Theorem: FormalSum.equiv_e_of_zero_coeffs (UnitConjecture/FreeModule.lean)

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)
hyp : ∀ (x : X), coords (h :: t) x = 0
mt : s = h :: t
⊢ h :: t ≃ []
Tactic:
let (a₀, x₀) := h
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
⊢ (a₀, x₀) :: t ≃ []

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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let hyp₀ := hyp x₀
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₀ : coords ((a₀, x₀) :: t) x₀ = 0 := hyp x₀
⊢ (a₀, x₀) :: t ≃ []

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₀ : coords ((a₀, x₀) :: t) x₀ = 0 := hyp x₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [coords] at hyp₀
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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
⊢ (a₀, x₀) :: t ≃ []

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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀ := by
  simp [monomCoeff]
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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (a₀, x₀) :: t ≃ []

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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [c₀] at hyp₀
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₀
⊢ (a₀, x₀) :: t ≃ []

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₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
exact
  if hz : a₀ = 0 then by
    rw [hz] at hyp₀
    rw [zero_add] at hyp₀
    have tail_coeffs : ∀ x : X, coords t x = 0 := by
      intro x
      exact
        if c : (x₀ = x) then by
          rw [← c]
          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
          assumption
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    let step : t ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    rw [hz]
    have ls : (0, x₀) :: t ≃ t := by
      apply Quot.sound
      apply ElementaryMove.zeroCoeff
      rfl
    exact Eq.trans ls step
  else by
    have non_zero : 0 ≠ coords t x₀ := by
      intro contra'
      let contra := Eq.symm contra'
      rw [contra, add_zero] at hyp₀
      contradiction
    let ⟨ys, eqnStep, lIneqStep⟩ := nonzero_coeff_has_complement x₀ t non_zero
    have tail_coeffs : ∀ x : X, coords ys x = 0 := by
      intro x
      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
    have _ : ys.length < (h :: t).length := by
      simp [List.length_cons]
      apply Nat.le_trans lIneqStep
      apply Nat.le_succ
    let step : ys ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    let eqn₁ := cons_equiv_of_equiv _ _ (coords t x₀) x₀ step
    let eqn₂ : t ≃ (coords t x₀, x₀) :: [] := Eq.trans (Eq.symm eqnStep) eqn₁
    let eqn₃ := cons_equiv_of_equiv _ _ a₀ x₀ eqn₂
    apply Eq.trans eqn₃
    have eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)] := by
      apply Quot.sound
      apply ElementaryMove.addCoeffs
    apply Eq.trans eqn₄
    rw [hyp₀]
    apply Quot.sound
    apply ElementaryMove.zeroCoeff
    rfl
State after:
no goals

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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
⊢ monomCoeff R X x₀ (a₀, x₀) = a₀
Tactic:
simp [monomCoeff]
State after:
no goals

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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [hz] at hyp₀
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₀ : 0 + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
⊢ (a₀, x₀) :: t ≃ []

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₀ : 0 + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [zero_add] at hyp₀
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
⊢ (a₀, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have tail_coeffs : ∀ x : X, coords t x = 0 := by
  intro x
  exact
    if c : (x₀ = x) then by
      rw [← c]
      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
      assumption
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
⊢ (a₀, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have _ : t.length < (h :: t).length := by
  simp [List.length_cons]
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let step : t ≃ [] := by
  apply equiv_e_of_zero_coeffs
  exact tail_coeffs
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ (a₀, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [hz]
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ (0, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ (0, x₀) :: t ≃ []
Tactic:
have ls : (0, x₀) :: t ≃ t := by
  apply Quot.sound
  apply ElementaryMove.zeroCoeff
  rfl
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
ls : (0, x₀) :: t ≃ t
⊢ (0, x₀) :: t ≃ []

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
ls : (0, x₀) :: t ≃ t
⊢ (0, x₀) :: t ≃ []
Tactic:
exact Eq.trans ls step
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
⊢ ∀ (x : X), coords t x = 0
Tactic:
intro x
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
⊢ coords t x = 0
Tactic:
exact
  if c : (x₀ = x) then by
    rw [← c]
    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
    assumption
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : x₀ = x
⊢ coords t x = 0
Tactic:
rw [← c]
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : x₀ = x
⊢ coords t x₀ = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : x₀ = x
⊢ coords t x₀ = 0
Tactic:
assumption
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
⊢ coords t x = 0
Tactic:
let hx := hyp x
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : coords ((a₀, x₀) :: t) x = 0 := hyp x
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : coords ((a₀, x₀) :: t) x = 0 := hyp x
⊢ coords t x = 0
Tactic:
simp [coords, monomCoeff] at hx
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
⊢ coords t x = 0
Tactic:
have lf : (x₀ == x) = false := decide_eq_false c
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
lf : (x₀ == x) = false
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
lf : (x₀ == x) = false
⊢ coords t x = 0
Tactic:
rw [lf] at hx
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx :
  (match false with
      | true => a₀
      | false => 0) +
      coords t x =
    0
lf : (x₀ == x) = false
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
hx :
  (match false with
      | true => a₀
      | false => 0) +
      coords t x =
    0
lf : (x₀ == x) = false
⊢ coords t x = 0
Tactic:
simp [zero_add] at hx
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
lf : (x₀ == x) = false
hx : coords t x = 0
⊢ coords t x = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
x : X
c : ¬x₀ = x
lf : (x₀ == x) = false
hx : coords t x = 0
⊢ coords t x = 0
Tactic:
assumption
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
⊢ List.length t < List.length (h :: t)
Tactic:
simp [List.length_cons]
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
⊢ t ≃ []
Tactic:
apply equiv_e_of_zero_coeffs
State after:
case hyp
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
⊢ ∀ (x : X), coords t x = 0

State before:
case hyp
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
⊢ ∀ (x : X), coords t x = 0
Tactic:
exact tail_coeffs
State after:
no goals

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ (0, x₀) :: t ≃ t
Tactic:
apply Quot.sound
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ ElementaryMove R X ((0, x₀) :: t) t

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ ElementaryMove R X ((0, x₀) :: t) t
Tactic:
apply ElementaryMove.zeroCoeff
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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ 0 = 0

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₀ : coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : a₀ = 0
tail_coeffs : ∀ (x : X), coords t x = 0
x✝ : List.length t < List.length (h :: t)
step : t ≃ [] := equiv_e_of_zero_coeffs t tail_coeffs
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have non_zero : 0 ≠ coords t x₀ := by
  intro contra'
  let contra := Eq.symm contra'
  rw [contra, add_zero] at hyp₀
  contradiction
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₀
⊢ (a₀, x₀) :: t ≃ []

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₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let ⟨ys, eqnStep, lIneqStep⟩ := nonzero_coeff_has_complement x₀ t non_zero
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
⊢ (a₀, x₀) :: t ≃ []

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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have tail_coeffs : ∀ x : X, coords ys x = 0 := by
  intro x
  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
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
⊢ (a₀, x₀) :: t ≃ []

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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have _ : ys.length < (h :: t).length := by
  simp [List.length_cons]
  apply Nat.le_trans lIneqStep
  apply Nat.le_succ
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)
⊢ (a₀, x₀) :: t ≃ []

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
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 ≃ []

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
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 ≃ []

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₁
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 ≃ []

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₂
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 ≃ []

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₃
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 []

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
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 []

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₄
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 []

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₀]
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 []

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
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₀)] []

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
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

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
State after:
no goals

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'
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

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'
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

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₀
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

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
State after:
no goals

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
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

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
State after:
no goals

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]
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

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:
let ceq := coords_well_defined x₀ _ _ eqnStep
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
ceq : coords ((coords t x₀, x₀) :: ys) x₀ = coords t x₀ := coords_well_defined x₀ ((coords t x₀, x₀) :: ys) t eqnStep
⊢ coords ys x₀ = 0

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
ceq : coords ((coords t x₀, x₀) :: ys) x₀ = coords t x₀ := coords_well_defined x₀ ((coords t x₀, x₀) :: ys) t eqnStep
⊢ coords ys x₀ = 0
Tactic:
simp [coords, monomCoeff] at ceq
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
ceq : coords ys x₀ = 0
⊢ coords ys x₀ = 0

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
ceq : coords ys x₀ = 0
⊢ coords ys x₀ = 0
Tactic:
assumption
State after:
no goals

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:
let hx := hyp x
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
hx : coords ((a₀, x₀) :: t) x = 0 := hyp x
⊢ coords ys x = 0

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
hx : coords ((a₀, x₀) :: t) x = 0 := hyp x
⊢ coords ys x = 0
Tactic:
simp [coords, monomCoeff] at hx
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
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
⊢ coords ys x = 0

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
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
⊢ coords ys x = 0
Tactic:
have lf : (x₀ == x) = false := decide_eq_false c
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
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
lf : (x₀ == x) = false
⊢ coords ys x = 0

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
hx : (match x₀ == x with
    | true => a₀
    | false => 0) +
    coords t x =
  0 :=
  hyp x
lf : (x₀ == x) = false
⊢ coords ys x = 0
Tactic:
rw [lf] at hx
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
hx :
  (match false with
      | true => a₀
      | false => 0) +
      coords t x =
    0
lf : (x₀ == x) = false
⊢ coords ys x = 0

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
hx :
  (match false with
      | true => a₀
      | false => 0) +
      coords t x =
    0
lf : (x₀ == x) = false
⊢ coords ys x = 0
Tactic:
simp [zero_add] at hx
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
lf : (x₀ == x) = false
hx : coords t x = 0
⊢ coords ys x = 0

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
lf : (x₀ == x) = false
hx : coords t x = 0
⊢ coords ys x = 0
Tactic:
let ceq := coords_well_defined x _ _ eqnStep
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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ((coords t x₀, x₀) :: ys) x = coords t x := coords_well_defined x ((coords t x₀, x₀) :: ys) t eqnStep
⊢ coords ys x = 0

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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ((coords t x₀, x₀) :: ys) x = coords t x := coords_well_defined x ((coords t x₀, x₀) :: ys) t eqnStep
⊢ coords ys x = 0
Tactic:
simp [coords, monomCoeff, lf] at ceq
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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ys x = coords t x
⊢ coords ys x = 0

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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ys x = coords t x
⊢ coords ys x = 0
Tactic:
rw [hx] at ceq
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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ys x = 0
⊢ coords ys x = 0

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
lf : (x₀ == x) = false
hx : coords t x = 0
ceq : coords ys x = 0
⊢ coords ys x = 0
Tactic:
exact ceq
State after:
no goals

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
⊢ List.length ys < List.length (h :: t)
Tactic:
simp [List.length_cons]
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
⊢ List.length ys < Nat.succ (List.length t)

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
⊢ List.length ys < Nat.succ (List.length t)
Tactic:
apply Nat.le_trans lIneqStep
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
⊢ List.length t ≤ Nat.succ (List.length t)

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
⊢ List.length t ≤ Nat.succ (List.length t)
Tactic:
apply Nat.le_succ
State after:
no goals

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)
⊢ ys ≃ []
Tactic:
apply equiv_e_of_zero_coeffs
State after:
case hyp
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)
⊢ ∀ (x : X), coords ys x = 0

State before:
case hyp
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)
⊢ ∀ (x : X), coords ys x = 0
Tactic:
exact tail_coeffs
State after:
no goals

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 [(a₀ + coords t x₀, x₀)]
Tactic:
apply Quot.sound
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₂
⊢ ElementaryMove R X [(a₀, x₀), (coords t x₀, x₀)] [(a₀ + coords t x₀, x₀)]

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₂
⊢ ElementaryMove R X [(a₀, x₀), (coords t x₀, x₀)] [(a₀ + coords t x₀, x₀)]
Tactic:
apply ElementaryMove.addCoeffs
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
_x✝ : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0
a✝¹ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y _x✝ → y.1 ≃ []
s : FormalSum R X
hyp✝¹ : ∀ (x : X), coords s x = 0
a✝ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y
        { fst := s, snd := hyp✝¹ } →
      y.1 ≃ []
h : R × X
t : List (R × X)
hyp✝ : ∀ (x : X), coords (h :: t) x = 0
mt✝ : s = h :: t
x✝¹ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y
        { fst := h :: t, snd := hyp✝ } →
      y.1 ≃ []
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : coords ((a₀, x₀) :: t) x₀ = 0 := hyp x₀
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)
⊢ (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1
    { fst := ys, snd := tail_coeffs } { fst := h :: t, snd := hyp✝ }
Tactic:
assumption
State after:
no goals