import JaxLean.Stdlib import examples.tensor_puzzles.generated.PuzzlesPadToset_option maxRecDepth 4096set_option maxHeartbeats 2000000namespace JaxLean.Puzzles.PadTotheorem matches_loop (a : Tensor ℝ [3]) : Array.pad_to a = Loop.pad_to a := bya:Tensor ℝ [3]⊢ Array.pad_to a = Loop.pad_to a funext ⟨i, u⟩a:Tensor ℝ [3]i:Fin 5u:Index []⊢ Array.pad_to a (i, u) = Loop.pad_to a (i, u) cases uunita:Tensor ℝ [3]i:Fin 5⊢ Array.pad_to a (i, PUnit.unit) = Loop.pad_to a (i, PUnit.unit) fin_cases iunit.«0»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«3»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨3, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨3, ⋯⟩, PUnit.unit)unit.«4»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨4, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨4, ⋯⟩, PUnit.unit) <;>unit.«0»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨0, ⋯⟩, PUnit.unit)unit.«1»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨1, ⋯⟩, PUnit.unit)unit.«2»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨2, ⋯⟩, PUnit.unit)unit.«3»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨3, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨3, ⋯⟩, PUnit.unit)unit.«4»a:Tensor ℝ [3]⊢ Array.pad_to a ((fun i => i) ⟨4, ⋯⟩, PUnit.unit) = Loop.pad_to a ((fun i => i) ⟨4, ⋯⟩, PUnit.unit) rflAll goals completed! 🐙 theorem certificate (a : Tensor ℝ [3]) : Jaxpr.Program.eval (.cons a .nil) Array.pad_to_ir = Jaxpr.Program.eval (.cons a .nil) Loop.pad_to_ir := bya:Tensor ℝ [3]⊢ Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Array.pad_to_ir = Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Loop.pad_to_ir rw [Array.pad_to_translation_correct,a:Tensor ℝ [3]⊢ Array.pad_to a = Jaxpr.Program.eval (Jaxpr.Env.cons a Jaxpr.Env.nil) Loop.pad_to_ira:Tensor ℝ [3]⊢ Array.pad_to a = Loop.pad_to a Loop.pad_to_translation_correcta:Tensor ℝ [3]⊢ Array.pad_to a = Loop.pad_to aa:Tensor ℝ [3]⊢ Array.pad_to a = Loop.pad_to a]a:Tensor ℝ [3]⊢ Array.pad_to a = Loop.pad_to a exact matches_loop aAll goals completed! 🐙end JaxLean.Puzzles.PadTo