internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₃
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₂
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₀
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₂
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₁
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₀
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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₃
Proof state after:
no goals
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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)
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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))
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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'
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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'
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₂
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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₂