awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ ∀ (x : Fin 2 → R), funMap addFunc x = x 0 + x 1
have simp : ∀ (a a_1 : R),
  funMap addFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
    HAdd.hAdd (β := R) a
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1 :
        R)
Tactic: simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ ∀ (x : Fin 2 → R), funMap mulFunc x = x 0 * x 1
have simp : ∀ (a a_1 : R),
  funMap mulFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
        (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R)))) =
    HMul.hMul (β := R) a
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ R) a
          (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a_1 (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1 :
        R)
Tactic: simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ ∀ (x : Fin 1 → R), funMap negFunc x = -x 0
have simp : ∀ (a : R),
  funMap negFunc
      (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ R) a (finZeroElim (α := fun (i : Fin 0) ↦ R))) =
    -a
Tactic: simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ ∀ (x : Fin 0 → R), funMap zeroFunc x = 0
have simp : Eq.{u_2 + 1} (α := R) (funMap zeroFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 0
Tactic: simp only [Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : ring.Structure R
⊢ ∀ (x : Fin 0 → R), funMap oneFunc x = 1
have simp : Eq.{u_2 + 1} (α := R) (funMap oneFunc (finZeroElim (α := fun (i : Fin 0) ↦ R))) 1
Tactic: simp only [Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Definability (goal)
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ Set.Definable (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) ring
    (zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))))
have rw : ∃ (φ :
  ring.Formula
    (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
  zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))) =
    {v : ι → K |
      φ.Realize
        (Sum.elim
          (Subtype.val (p := fun (x : K) ↦
            Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
          v)}
Tactic: rw [Set.definable_iff_exists_formula_sum]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Definability (goal)
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    zeroLocus K (Ideal.span (↑S : Set (MvPolynomial ι K))) =
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}
have rw : ∃ (φ :
  ring.Formula
    (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
  Eq (α := Set (ι → K))
    {x : ι → K |
      ∀ p ∈ (↑S : Set (MvPolynomial ι K)), Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
    {v : ι → K |
      φ.Realize
        (Sum.elim
          (Subtype.val (p := fun (x : K) ↦
            Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
          v)}
Tactic: rw [MvPolynomial.zeroLocus_span]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Definability (goal)
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support
⊢ Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ)))
    (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
      (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
have simp : ∃ (i : MvPolynomial ι K) (_ : i ∈ S),
  Membership.mem (γ := Set K) ((fun (m : ι →₀ ℕ) ↦ coeff m i) '' (↑i.support : Set (ι →₀ ℕ)))
    (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
      (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
Tactic: simp only [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Definability (goal)
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    Eq (α := Set (ι → K))
      {x : ι → K |
        ∀ p ∈ (↑S : Set (MvPolynomial ι K)),
          Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}
have refine : Eq (α := Set (ι → K))
  {x : ι → K |
    ∀ p ∈ (↑S : Set (MvPolynomial ι K)), Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
  {v : ι → K |
    Formula.Realize (L := ring) (α :=
      Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)
      (BoundedFormula.iInf fun (i : ↥S) ↦
        Term.equal
          (Term.relabel
            (Sum.map
              (fun (p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ)))
                    x)
                  (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
                    (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
                  sorry)
              id)
            (termOfFreeCommRing (p' i)))
          0)
      (Sum.elim
        (Subtype.val (p := fun (x : K) ↦
          Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
        v)}
Tactic: refine ⟨BoundedFormula.iInf
      (fun i : S => Term.equal
        ((termOfFreeCommRing (p' i)).relabel
          (Sum.map (fun p => ⟨p.1.1.coeff p.2.1, by
            simp only [Set.mem_iUnion]
            exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩⟩) id)) 0), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
| ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      p :
    R)
have rw : ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
      (a : FreeCommRing α) → R)
    (Term.realize FreeCommRing.of
      (Classical.choose (p := fun (x : ring.Term α) ↦ Term.realize FreeCommRing.of x = p) sorry)) :
  R)
Tactic: rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      p
have conv_rhs : Term.realize (L := ring) v (sorry p) =
  (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
      (a : FreeCommRing α) → R)
    (Term.realize FreeCommRing.of
      (Classical.choose (p := fun (x : ring.Term α) ↦ Term.realize FreeCommRing.of x = p) sorry))
Tactic: conv_rhs => rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : α
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize (L := ring) FreeCommRing.of (var a))
have var : Term.realize (L := ring) v (sorry p) = v a
Tactic: simp
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
l : ℕ
f : ring.Functions l
a : Fin l → ring.Term α
ih :
  ∀ (a_1 : Fin l),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func f a))
have func : ∀ (a : Fin 2 → ring.Term α)
  (ih :
    ∀ (a_1 : Fin 2),
      Term.realize (L := ring) v (sorry p) =
        (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a a_1))),
  Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.add a))
Tactic: cases f
Cleared hypotheses: l, f, a, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
l : ℕ
f : ring.Functions l
a : Fin l → ring.Term α
ih :
  ∀ (a_1 : Fin l),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
func :
  ∀ (a : Fin 2 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 2),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.add a))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func f a))
have func₁ : ∀ (a : Fin 2 → ring.Term α)
  (ih :
    ∀ (a_1 : Fin 2),
      Term.realize (L := ring) v (sorry p) =
        (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a a_1))),
  Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func ringFunc.mul a))
Tactic: cases f
Cleared hypotheses: l, f, a, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
l : ℕ
f : ring.Functions l
a : Fin l → ring.Term α
ih :
  ∀ (a_1 : Fin l),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
func :
  ∀ (a : Fin 2 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 2),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.add a))
func₁ :
  ∀ (a : Fin 2 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 2),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.mul a))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func f a))
have func₂ : ∀ (a : Fin 1 → ring.Term α)
  (ih :
    ∀ (a_1 : Fin 1),
      Term.realize (L := ring) v (sorry p) =
        (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a a_1))),
  Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func ringFunc.neg a))
Tactic: cases f
Cleared hypotheses: l, f, a, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
l : ℕ
f : ring.Functions l
a : Fin l → ring.Term α
ih :
  ∀ (a_1 : Fin l),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
func :
  ∀ (a : Fin 2 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 2),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.add a))
func₁ :
  ∀ (a : Fin 2 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 2),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.mul a))
func₂ :
  ∀ (a : Fin 1 → ring.Term α)
    (ih :
      ∀ (a_1 : Fin 1),
        Term.realize (L := ring) v (sorry p) =
          (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
              (a : FreeCommRing α) → R)
            (Term.realize FreeCommRing.of (a a_1))),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (Language.func ringFunc.neg a))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func f a))
have func₃ : ∀ (a : Fin 0 → ring.Term α)
  (ih :
    ∀ (a_1 : Fin 0),
      Term.realize (L := ring) v (sorry p) =
        (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a a_1))),
  Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (Language.func ringFunc.zero a))
Tactic: cases f
Cleared hypotheses: l, f, a, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih :
  ∀ (a_1 : Fin 2),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.add a))
have func : Term.realize (L := ring) v (sorry p) =
  HAdd.hAdd (α := R) (β := R)
    ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a 0)) :
      R)
    ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a 1)) :
      R)
Tactic: simp [ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih :
  ∀ (a_1 : Fin 2),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.mul a))
have func : Term.realize (L := ring) v (sorry p) =
  HMul.hMul (α := R) (β := R)
    ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a 0)) :
      R)
    ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a 1)) :
      R)
Tactic: simp [ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 1 → ring.Term α
ih :
  ∀ (a_1 : Fin 1),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.neg a))
have func : Term.realize (L := ring) v (sorry p) =
  -(((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (a 0))
Tactic: simp [ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih :
  ∀ (a_1 : Fin 0),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.zero a))
have func : Term.realize (L := ring) v (sorry p) = 0
Tactic: simp [ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih :
  ∀ (a_1 : Fin 0),
    Term.realize (L := ring) v (sorry p) =
      (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of (func ringFunc.one a))
have func : Term.realize (L := ring) v (sorry p) = 1
Tactic: simp [ih]