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

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
⊢ x + zero = x
Tactic:
apply @Quotient.ind (motive := fun x : R[X] => x + zero = 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), Quotient.mk (formalSumSetoid R X) a + zero = 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), Quotient.mk (formalSumSetoid R X) a + zero = 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
⊢ Quotient.mk (formalSumSetoid R X) x + zero = 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
⊢ Quotient.mk (formalSumSetoid R X) x + zero = 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 x₀ + coords [] 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₀ = coords x x₀
Tactic:
simp [add_zero, coords]
State after:
no goals