Theorem: FreeModule.zero_addn (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ zero + x = x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => zero + x = x)
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), zero + Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ ∀ (a : FormalSum R X), zero + Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) a
Tactic:
intro x
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ zero + Quotient.mk (formalSumSetoid R X) x = Quotient.mk (formalSumSetoid R X) x

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ zero + Quotient.mk (formalSumSetoid R X) x = Quotient.mk (formalSumSetoid R X) x
Tactic:
apply Quotient.sound
State after:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ [] ++ x ≈ x

State before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ [] ++ x ≈ x
Tactic:
apply funext
State after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords ([] ++ x) x_1 = coords x x_1

State before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
⊢ ∀ (x_1 : X), coords ([] ++ x) x_1 = coords x x_1
Tactic:
intro x₀
State after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords ([] ++ x) x₀ = coords x x₀

State before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords ([] ++ x) x₀ = coords x x₀
Tactic:
rw [← append_coords]
State after:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords x x₀ = coords x x₀

State before:
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords x x₀ = coords x x₀
Tactic:
simp [add_zero, coords]
State after:
no goals