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