import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesOnesset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.Onestheorem matches_loop : Array.ones (R := ℝ) = Loop.ones (R := ℝ) := by⊢ Array.ones = Loop.ones funext ⟨i, u⟩i:Fin 3u:Index []⊢ Array.ones (i, u) = Loop.ones (i, u) cases uuniti:Fin 3⊢ Array.ones (i, PUnit.unit) = Loop.ones (i, PUnit.unit) fin_cases iunit.«0»⊢ Array.ones ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»⊢ Array.ones ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»⊢ Array.ones ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) <;>unit.«0»⊢ Array.ones ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»⊢ Array.ones ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»⊢ Array.ones ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.ones ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) rflAll goals completed! 🐙 theorem certificate : Jaxpr.Program.eval .nil Array.ones_ir = Jaxpr.Program.eval .nil Loop.ones_ir := by⊢ Jaxpr.Program.eval Jaxpr.Env.nil Array.ones_ir = Jaxpr.Program.eval Jaxpr.Env.nil Loop.ones_ir rw [Array.ones_translation_correct,⊢ Array.ones = Jaxpr.Program.eval Jaxpr.Env.nil Loop.ones_ir⊢ Array.ones = Loop.ones Loop.ones_translation_correct⊢ Array.ones = Loop.ones⊢ Array.ones = Loop.ones]⊢ Array.ones = Loop.ones exact matches_loopAll goals completed! 🐙end JaxLean.Puzzles.Ones