Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: case func.add
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.add a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.add a))

pp: case func.mul
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.mul a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.mul a))

pp: case func.neg
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 1 → ring.Term α
ih : ∀ (a_1 : Fin 1), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.neg a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.neg a))

pp: case func.zero
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.zero a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.zero a))

pp: case func.one
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.one a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.one a))

Tactic:
<;>

Goal state after:
case func.add
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.add a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.add a))

case func.mul
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih : ∀ (a_1 : Fin 2), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.mul a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.mul a))

case func.neg
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 1 → ring.Term α
ih : ∀ (a_1 : Fin 1), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.neg a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.neg a))

case func.zero
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.zero a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.zero a))

case func.one
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih : ∀ (a_1 : Fin 0), Term.realize v (a a_1) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (a a_1))
⊢ Term.realize v (func ringFunc.one a) = (FreeCommRing.lift v) (Term.realize FreeCommRing.of (func ringFunc.one a))