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

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
⊢ ∀ (x : X), coords s₂ x = 0
Tactic:
intro x
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
⊢ coords s₂ x = 0

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
⊢ coords s₂ x = 0
Tactic:
let h := hyp x
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
h : coords [] x = coords s₂ x := hyp x
⊢ coords s₂ x = 0

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
h : coords [] x = coords s₂ x := hyp x
⊢ coords s₂ x = 0
Tactic:
rw [← h]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
h : coords [] x = coords s₂ x := hyp x
⊢ coords [] x = 0

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
h : coords [] x = coords s₂ x := hyp x
⊢ coords [] x = 0
Tactic:
rfl
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
exact
  if p : 0 = a₀ then by
    have eq₁ : (a₀, x₀) :: t ≃ t := by
      apply Quot.sound
      apply ElementaryMove.zeroCoeff
      apply Eq.symm
      assumption
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    have eq₂ : t ≃ s₂ := by
      apply equiv_of_equal_coeffs t s₂
      intro x
      let ceq := coords_well_defined x ((a₀, x₀) :: t) t eq₁
      simp [← ceq, hyp]
    exact Eq.trans eq₁ eq₂
  else by
    let a₁ := coords t x₀
    exact
      if p₁ : 0 = a₁ then by
        have cf₂ : s₂.coords x₀ = a₀ := by
          rw [← hyp]
          simp [coords, ← p₁, Nat.add_zero, monomCoeff]
        let ⟨ys, eqn, _⟩ :=
          nonzero_coeff_has_complement x₀ s₂
            (by
              rw [cf₂]
              assumption)
        let cfs := fun x => coords_well_defined x _ _ eqn
        rw [cf₂] at cfs
        let cfs' := fun (x : X) => Eq.trans (hyp x) (Eq.symm (cfs x))
        simp [coords] at cfs'
        have _ : t.length < (h :: t).length := by
          simp [List.length_cons]
        let step := equiv_of_equal_coeffs t ys cfs'
        let _step' := cons_equiv_of_equiv t ys a₀ x₀ step
        rw [cf₂] at eqn
        exact Eq.trans _step' eqn
      else by
        let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁
        let s₃ := (a₀ + a₁, x₀) :: ys
        have eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃ := by
          apply Quot.sound
          let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
          exact lem
        have eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t := by
          apply cons_equiv_of_equiv
          assumption
        have eq₃ : s₃ ≃ s₂ := by
          have _ : ys.length + 1 < t.length + 1 := by
            apply Nat.succ_lt_succ
            exact ineqn
          apply equiv_of_equal_coeffs
          intro x
          rw [← hyp x]
          simp [coords]
          let d := coords_well_defined x _ _ eqn
          rw [coords] at d
          rw [← d]
          simp [monom_coords_hom, coords, add_assoc]
        apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have eq₁ : (a₀, x₀) :: t ≃ t := by
  apply Quot.sound
  apply ElementaryMove.zeroCoeff
  apply Eq.symm
  assumption
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
⊢ (a₀, x₀) :: t ≃ s₂
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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have eq₂ : t ≃ s₂ := by
  apply equiv_of_equal_coeffs t s₂
  intro x
  let ceq := coords_well_defined x ((a₀, x₀) :: t) t eq₁
  simp [← ceq, hyp]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
eq₂ : t ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
eq₂ : t ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
exact Eq.trans eq₁ eq₂
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ (a₀, 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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ ElementaryMove R X ((a₀, x₀) :: t) t

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ ElementaryMove R X ((a₀, 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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ a₀ = 0

State before:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ a₀ = 0
Tactic:
apply Eq.symm
State after:
case a.h.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ 0 = a₀

State before:
case a.h.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
⊢ 0 = a₀
Tactic:
assumption
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
⊢ 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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
⊢ t ≃ s₂
Tactic:
apply equiv_of_equal_coeffs t s₂
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
⊢ ∀ (x : X), coords t x = coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
⊢ ∀ (x : X), coords t x = coords s₂ x
Tactic:
intro x
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
⊢ coords t x = coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
⊢ coords t x = coords s₂ x
Tactic:
let ceq := coords_well_defined x ((a₀, x₀) :: t) t eq₁
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
ceq : coords ((a₀, x₀) :: t) x = coords t x := coords_well_defined x ((a₀, x₀) :: t) t eq₁
⊢ coords t x = coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
ceq : coords ((a₀, x₀) :: t) x = coords t x := coords_well_defined x ((a₀, x₀) :: t) t eq₁
⊢ coords t x = coords s₂ x
Tactic:
simp [← ceq, hyp]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let a₁ := coords t x₀
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
exact
  if p₁ : 0 = a₁ then by
    have cf₂ : s₂.coords x₀ = a₀ := by
      rw [← hyp]
      simp [coords, ← p₁, Nat.add_zero, monomCoeff]
    let ⟨ys, eqn, _⟩ :=
      nonzero_coeff_has_complement x₀ s₂
        (by
          rw [cf₂]
          assumption)
    let cfs := fun x => coords_well_defined x _ _ eqn
    rw [cf₂] at cfs
    let cfs' := fun (x : X) => Eq.trans (hyp x) (Eq.symm (cfs x))
    simp [coords] at cfs'
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    let step := equiv_of_equal_coeffs t ys cfs'
    let _step' := cons_equiv_of_equiv t ys a₀ x₀ step
    rw [cf₂] at eqn
    exact Eq.trans _step' eqn
  else by
    let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁
    let s₃ := (a₀ + a₁, x₀) :: ys
    have eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃ := by
      apply Quot.sound
      let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
      exact lem
    have eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t := by
      apply cons_equiv_of_equiv
      assumption
    have eq₃ : s₃ ≃ s₂ := by
      have _ : ys.length + 1 < t.length + 1 := by
        apply Nat.succ_lt_succ
        exact ineqn
      apply equiv_of_equal_coeffs
      intro x
      rw [← hyp x]
      simp [coords]
      let d := coords_well_defined x _ _ eqn
      rw [coords] at d
      rw [← d]
      simp [monom_coords_hom, coords, add_assoc]
    apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have cf₂ : s₂.coords x₀ = a₀ := by
  rw [← hyp]
  simp [coords, ← p₁, Nat.add_zero, monomCoeff]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let ⟨ys, eqn, _⟩ :=
  nonzero_coeff_has_complement x₀ s₂
    (by
      rw [cf₂]
      assumption)
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let cfs := fun x => coords_well_defined x _ _ eqn
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((coords s₂ x₀, x₀) :: ys) x = coords s₂ x :=
  fun x => coords_well_defined x ((coords s₂ x₀, x₀) :: ys) s₂ eqn
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((coords s₂ x₀, x₀) :: ys) x = coords s₂ x :=
  fun x => coords_well_defined x ((coords s₂ x₀, x₀) :: ys) s₂ eqn
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
rw [cf₂] at cfs
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let cfs' := fun (x : X) => Eq.trans (hyp x) (Eq.symm (cfs x))
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords ((a₀, x₀) :: ys) x := fun x => (hyp x).trans (cfs x).symm
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords ((a₀, x₀) :: ys) x := fun x => (hyp x).trans (cfs x).symm
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
simp [coords] at cfs'
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
⊢ (a₀, x₀) :: t ≃ s₂
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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let step := equiv_of_equal_coeffs t ys cfs'
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let _step' := cons_equiv_of_equiv t ys a₀ x₀ step
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
_step' : (a₀, x₀) :: t ≃ (a₀, x₀) :: ys := cons_equiv_of_equiv t ys a₀ x₀ step
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
_step' : (a₀, x₀) :: t ≃ (a₀, x₀) :: ys := cons_equiv_of_equiv t ys a₀ x₀ step
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
rw [cf₂] at eqn
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (a₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
_step' : (a₀, x₀) :: t ≃ (a₀, x₀) :: ys := cons_equiv_of_equiv t ys a₀ x₀ step
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (a₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
x✝ : List.length t < List.length (h :: t)
step : t ≃ ys := equiv_of_equal_coeffs t ys cfs'
_step' : (a₀, x₀) :: t ≃ (a₀, x₀) :: ys := cons_equiv_of_equiv t ys a₀ x₀ step
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
exact Eq.trans _step' eqn
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
⊢ coords s₂ x₀ = a₀
Tactic:
rw [← hyp]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
⊢ coords ((a₀, x₀) :: t) x₀ = a₀

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
⊢ coords ((a₀, x₀) :: t) x₀ = a₀
Tactic:
simp [coords, ← p₁, Nat.add_zero, monomCoeff]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
⊢ 0 ≠ coords s₂ x₀
Tactic:
rw [cf₂]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
⊢ 0 ≠ a₀

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
⊢ 0 ≠ a₀
Tactic:
assumption
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
cf₂ : coords s₂ x₀ = a₀
ys : FormalSum R X
eqn : (coords s₂ x₀, x₀) :: ys ≃ s₂
right✝ : List.length ys < List.length s₂
cfs : ∀ (x : X), coords ((a₀, x₀) :: ys) x = coords s₂ x
cfs' : ∀ (x : X), coords t x = coords ys x
⊢ 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₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
let s₃ := (a₀ + a₁, x₀) :: ys
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃ := by
  apply Quot.sound
  let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
  exact lem
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t := by
  apply cons_equiv_of_equiv
  assumption
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
have eq₃ : s₃ ≃ s₂ := by
  have _ : ys.length + 1 < t.length + 1 := by
    apply Nat.succ_lt_succ
    exact ineqn
  apply equiv_of_equal_coeffs
  intro x
  rw [← hyp x]
  simp [coords]
  let d := coords_well_defined x _ _ eqn
  rw [coords] at d
  rw [← d]
  simp [monom_coords_hom, coords, add_assoc]
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
eq₃ : s₃ ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
eq₃ : s₃ ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂
Tactic:
apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
⊢ (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
Tactic:
apply Quot.sound
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
⊢ ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) s₃

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
⊢ ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) s₃
Tactic:
let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
lem : ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) ((a₀ + a₁, x₀) :: ys) := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
⊢ ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) s₃

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
lem : ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) ((a₀ + a₁, x₀) :: ys) := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
⊢ ElementaryMove R X ((a₀, x₀) :: (a₁, x₀) :: ys) s₃
Tactic:
exact lem
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
⊢ (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
Tactic:
apply cons_equiv_of_equiv
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
⊢ (a₁, x₀) :: ys ≃ t

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
⊢ (a₁, x₀) :: ys ≃ t
Tactic:
assumption
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ s₃ ≃ s₂
Tactic:
have _ : ys.length + 1 < t.length + 1 := by
  apply Nat.succ_lt_succ
  exact ineqn
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ s₃ ≃ s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ s₃ ≃ s₂
Tactic:
apply equiv_of_equal_coeffs
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ ∀ (x : X), coords s₃ x = coords s₂ x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ ∀ (x : X), coords s₃ x = coords s₂ x
Tactic:
intro x
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ coords s₃ x = coords s₂ x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ coords s₃ x = coords s₂ x
Tactic:
rw [← hyp x]
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ coords s₃ x = coords ((a₀, x₀) :: t) x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ coords s₃ x = coords ((a₀, x₀) :: t) x
Tactic:
simp [coords]
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x
Tactic:
let d := coords_well_defined x _ _ eqn
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : coords ((coords t x₀, x₀) :: ys) x = coords t x := coords_well_defined x ((coords t x₀, x₀) :: ys) t eqn
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : coords ((coords t x₀, x₀) :: ys) x = coords t x := coords_well_defined x ((coords t x₀, x₀) :: ys) t eqn
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x
Tactic:
rw [coords] at d
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : monomCoeff R X x (coords t x₀, x₀) + coords ys x = coords t x
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : monomCoeff R X x (coords t x₀, x₀) + coords ys x = coords t x
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x = monomCoeff R X x (a₀, x₀) + coords t x
Tactic:
rw [← d]
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : monomCoeff R X x (coords t x₀, x₀) + coords ys x = coords t x
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x =
    monomCoeff R X x (a₀, x₀) + (monomCoeff R X x (coords t x₀, x₀) + coords ys x)

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
x : X
d : monomCoeff R X x (coords t x₀, x₀) + coords ys x = coords t x
⊢ monomCoeff R X x (a₀ + coords t x₀, x₀) + coords ys x =
    monomCoeff R X x (a₀, x₀) + (monomCoeff R X x (coords t x₀, x₀) + coords ys x)
Tactic:
simp [monom_coords_hom, coords, add_assoc]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys + 1 < List.length t + 1
Tactic:
apply Nat.succ_lt_succ
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys < List.length t

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ List.length ys < List.length t
Tactic:
exact ineqn
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
_x✝ : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x
a✝² :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y _x✝ →
      y.1 ≃ y.2.1
s₁ : FormalSum R X
s₂✝ : (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x
a✝¹ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := s₁, snd := s₂✝ } →
      y.1 ≃ y.2.1
s₂ : FormalSum R X
hyp✝¹ : ∀ (x : X), coords s₁ x = coords s₂ x
a✝ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := s₁, snd := { fst := s₂, snd := hyp✝¹ } } →
      y.1 ≃ y.2.1
h : R × X
t : List (R × X)
hyp✝ : ∀ (x : X), coords (h :: t) x = coords s₂ x
x✝¹ :
  ∀ (y : (s₁ : FormalSum R X) ×' (s₂ : FormalSum R X) ×' ∀ (x : X), coords s₁ x = coords s₂ x),
    (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
            instWellFoundedRelation).1
        y { fst := h :: t, snd := { fst := s₂, snd := hyp✝ } } →
      y.1 ≃ y.2.1
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
x✝ : List.length ys + 1 < List.length t + 1
⊢ (invImage (fun a => PSigma.casesOn a fun s snd => PSigma.casesOn snd fun s₂ snd => List.length s)
        instWellFoundedRelation).1
    { fst := s₃, snd := { fst := s₂, snd := (_ : ∀ (x : X), coords s₃ x = coords s₂ x) } }
    { fst := h :: t, snd := { fst := s₂, snd := hyp✝ } }
Tactic:
assumption
State after:
no goals