internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let step : ys ≃ [] := by
  apply equiv_e_of_zero_coeffs
  exact tail_coeffs
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
⊢ (a₀, x₀) :: t ≃ []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let eqn₁ := cons_equiv_of_equiv _ _ (coords t x₀) x₀ step
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
⊢ (a₀, x₀) :: t ≃ []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let eqn₂ : t ≃ (coords t x₀, x₀) :: [] := Eq.trans (Eq.symm eqnStep) eqn₁
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
⊢ (a₀, x₀) :: t ≃ []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let eqn₃ := cons_equiv_of_equiv _ _ a₀ x₀ eqn₂
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
⊢ (a₀, x₀) :: t ≃ []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
⊢ (a₀, x₀) :: t ≃ []
Tactic:
apply Eq.trans eqn₃
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
⊢ sum [(a₀, x₀), (coords t x₀, x₀)] = sum []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
⊢ sum [(a₀, x₀), (coords t x₀, x₀)] = sum []
Tactic:
have eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)] := by
  apply Quot.sound
  apply ElementaryMove.addCoeffs
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀, x₀), (coords t x₀, x₀)] = sum []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀, x₀), (coords t x₀, x₀)] = sum []
Tactic:
apply Eq.trans eqn₄
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀ + coords t x₀, x₀)] = sum []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(a₀ + coords t x₀, x₀)] = sum []
Tactic:
rw [hyp₀]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(0, x₀)] = sum []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ sum [(0, x₀)] = sum []
Tactic:
apply Quot.sound
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ ElementaryMove R X [(0, x₀)] []
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ ElementaryMove R X [(0, x₀)] []
Tactic:
apply ElementaryMove.zeroCoeff
Proof state after:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ 0 = 0
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
step : ys ≃ [] := equiv_e_of_zero_coeffs ys tail_coeffs
eqn₁ : (coords t x₀, x₀) :: ys ≃ [(coords t x₀, x₀)] := cons_equiv_of_equiv ys [] (coords t x₀) x₀ step
eqn₂ : t ≃ [(coords t x₀, x₀)] := eqnStep.symm.trans eqn₁
eqn₃ : (a₀, x₀) :: t ≃ [(a₀, x₀), (coords t x₀, x₀)] := cons_equiv_of_equiv t [(coords t x₀, x₀)] a₀ x₀ eqn₂
eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)]
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
⊢ 0 ≠ coords t x₀
Tactic:
intro contra'
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
⊢ False
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
⊢ False
Tactic:
let contra := Eq.symm contra'
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
contra : coords t x₀ = 0 := contra'.symm
⊢ False
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
contra : coords t x₀ = 0 := contra'.symm
⊢ False
Tactic:
rw [contra, add_zero] at hyp₀
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
contra : coords t x₀ = 0 := contra'.symm
⊢ False
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
contra' : 0 = coords t x₀
contra : coords t x₀ = 0 := contra'.symm
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
⊢ ∀ (x : X), coords ys x = 0
Tactic:
intro x
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
⊢ coords ys x = 0
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
⊢ coords ys x = 0
Tactic:
exact
  if c : (x₀ = x) then by
    rw [← c]
    let ceq := coords_well_defined x₀ _ _ eqnStep
    simp [coords, monomCoeff] at ceq
    assumption
  else by
    let hx := hyp x
    simp [coords, monomCoeff] at hx
    have lf : (x₀ == x) = false := decide_eq_false c
    rw [lf] at hx
    simp [zero_add] at hx
    let ceq := coords_well_defined x _ _ eqnStep
    simp [coords, monomCoeff, lf] at ceq
    rw [hx] at ceq
    exact ceq
Proof state after:
no goals
Theorem: FormalSum.equiv_e_of_zero_coeffs
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
c : x₀ = x
⊢ coords ys x = 0
Tactic:
rw [← c]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
c : x₀ = x
⊢ coords ys x₀ = 0