internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
lIneq : List.length tail < List.length ((a, x) :: tail)
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
rw [← c', add_zero] at lem
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
lIneq : List.length tail < List.length ((a, x) :: tail)
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
lIneq : List.length tail < List.length ((a, x) :: tail)
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
rw [← lem]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
lIneq : List.length tail < List.length ((a, x) :: tail)
⊢ ∃ ys, (a, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
lIneq : List.length tail < List.length ((a, x) :: tail)
⊢ ∃ ys, (a, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
exact ⟨tail, rfl, lIneq⟩
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : 0 = k
⊢ List.length tail < List.length ((a, x) :: tail)
Tactic:
simp [List.length_cons]
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
let ⟨ys, eqnStep, lIneqStep⟩ := hyp c'
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by
  apply Quot.sound
  apply ElementaryMove.addCoeffs
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by
  apply cons_equiv_of_equiv
  assumption
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
rw [← lem]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (a + k, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ ∃ ys, (a + k, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
have lIneq : ys.length < List.length ((a, x₀) :: tail) := by
  apply Nat.le_trans lIneqStep
  simp [List.length_cons, Nat.le_succ]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
lIneq : List.length ys < List.length ((a, x₀) :: tail)
⊢ ∃ ys, (a + k, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
lIneq : List.length ys < List.length ((a, x₀) :: tail)
⊢ ∃ ys, (a + k, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
exact ⟨ys, eqn, lIneq⟩
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
⊢ (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
Tactic:
apply Quot.sound
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
⊢ ElementaryMove R X ((a, x₀) :: (k, x₀) :: ys) ((a + k, x₀) :: ys)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
⊢ ElementaryMove R X ((a, x₀) :: (k, x₀) :: ys) ((a + k, x₀) :: ys)
Tactic:
apply ElementaryMove.addCoeffs
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
⊢ (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
Tactic:
apply cons_equiv_of_equiv
Proof state after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
⊢ (k, x₀) :: ys ≃ tail
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
⊢ (k, x₀) :: ys ≃ tail
Tactic:
assumption
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
apply Nat.le_trans lIneqStep
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ List.length tail ≤ List.length ((a, x₀) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
c' : ¬0 = k
ys : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys ≃ tail
lIneqStep : List.length ys < List.length tail
eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys
eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail
eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail
⊢ List.length tail ≤ List.length ((a, x₀) :: tail)
Tactic:
simp [List.length_cons, Nat.le_succ]
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = false
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
let k := coords tail x₀
Proof state after:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = false
k : R := coords tail x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = false
k : R := coords tail x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have lem : k = coords ((a, x) :: tail) x₀ := by
  simp [coords, monomCoeff, c, zero_add]
Proof state after:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = false
k : R := coords tail x₀
lem : k = coords ((a, x) :: tail) x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
c : (x == x₀) = false
k : R := coords tail x₀
lem : k = coords ((a, x) :: tail) x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
rw [← lem] at pos
Proof state after:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
c : (x == x₀) = false
k : R := coords tail x₀
pos : 0 ≠ k
lem : k = coords ((a, x) :: tail) x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
c : (x == x₀) = false
k : R := coords tail x₀
pos : 0 ≠ k
lem : k = coords ((a, x) :: tail) x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
let ⟨ys', eqnStep, lIneqStep⟩ := hyp pos
Proof state after:
case cons.false
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
c : (x == x₀) = false
k : R := coords tail x₀
pos : 0 ≠ k
lem : k = coords ((a, x) :: tail) x₀
ys' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)