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
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
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₁
⊢ coords s₂ x₀ = a₀
Tactic:
rw [← 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₀
a₁ : R := coords t x₀
p₁ : 0 = a₁
⊢ coords ((a₀, x₀) :: t) x₀ = a₀
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₁
⊢ coords ((a₀, x₀) :: t) x₀ = a₀
Tactic:
simp [coords, ← p₁, Nat.add_zero, monomCoeff]
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₁
cf₂ : coords s₂ x₀ = a₀
⊢ 0 ≠ coords s₂ x₀
Tactic:
rw [cf₂]
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₀
⊢ 0 ≠ a₀
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₀
⊢ 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₀
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]
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:
let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁
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₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length 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₁
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
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₁
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₂
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₁
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
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₁
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₂
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₁
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
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₁
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₂
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₁
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]
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₁
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₂
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₁
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₃
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₁
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
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₀
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₃
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₀
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
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₀
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₃
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₀
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
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₁
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
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₀
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
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₀
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
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₁
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
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₁
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₂
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₁
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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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
Proof 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
Theorem: FormalSum.equiv_of_equal_coeffs
Proof 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]
Proof 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)