internlm/Lean-Github huggingface dataset:
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' : 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:
rw [← lem]
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, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
⊢ ∃ ys, (k, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
let ys := (a, x) :: ys'
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 : List (R × X) := (a, x) :: ys'
⊢ ∃ ys, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
⊢ ∃ ys, (k, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have lIneq : ys.length < ((a, x) :: tail).length := by
  simp [List.length_cons]
  apply Nat.succ_lt_succ
  exact lIneqStep
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
⊢ ∃ ys, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
⊢ ∃ ys, (k, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys' := by
  apply Quot.sound
  apply ElementaryMove.swap
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
⊢ ∃ ys, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
⊢ ∃ ys, (k, 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:
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail
⊢ ∃ ys, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail
⊢ ∃ ys, (k, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have eqn : (k, x₀) :: ys ≃ (a, x) :: tail := by
  exact Eq.trans eqn₁ eqn₂
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail
eqn : (k, x₀) :: ys ≃ (a, x) :: tail
⊢ ∃ ys, (k, 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' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail
eqn : (k, x₀) :: ys ≃ (a, x) :: tail
⊢ ∃ ys, (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₀) = false
k : R := coords tail x₀
⊢ k = coords ((a, x) :: tail) x₀
Tactic:
simp [coords, monomCoeff, c, zero_add]
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
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 : List (R × X) := (a, x) :: ys'
⊢ List.length ys < List.length ((a, x) :: tail)
Tactic:
simp [List.length_cons]
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
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 : List (R × X) := (a, x) :: ys'
⊢ Nat.succ (List.length ys') < Nat.succ (List.length 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
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 : List (R × X) := (a, x) :: ys'
⊢ Nat.succ (List.length ys') < Nat.succ (List.length tail)
Tactic:
apply Nat.succ_lt_succ
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
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 : List (R × X) := (a, x) :: ys'
⊢ List.length ys' < List.length 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
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 : List (R × X) := (a, x) :: ys'
⊢ List.length ys' < List.length tail
Tactic:
exact lIneqStep
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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
⊢ (k, x₀) :: ys ≃ (a, x) :: (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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
⊢ ElementaryMove R X ((k, x₀) :: ys) ((a, x) :: (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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
⊢ ElementaryMove R X ((k, x₀) :: ys) ((a, x) :: (k, x₀) :: ys')
Tactic:
apply ElementaryMove.swap
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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (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
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 : List (R × X) := (a, x) :: ys'
lIneq : List.length ys < List.length ((a, x) :: tail)
eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys'
eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail
⊢ (k, x₀) :: ys ≃ (a, x) :: tail
Tactic:
exact Eq.trans eqn₁ eqn₂
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)
hyp : ∀ (x : X), coords (h :: t) x = 0
mt : s = h :: t
⊢ h :: t ≃ []
Tactic:
let (a₀, x₀) := h
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
⊢ (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
⊢ (a₀, x₀) :: t ≃ []
Tactic:
let hyp₀ := 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 ((a₀, x₀) :: t) x₀ = 0 := hyp 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₀ : coords ((a₀, x₀) :: t) x₀ = 0 := hyp x₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [coords] 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₀ : monomCoeff R X x₀ (a₀, 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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
⊢ (a₀, x₀) :: t ≃ []
Tactic:
have c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀ := by
  simp [monomCoeff]
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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
rw [c₀] 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₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (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₀
⊢ (a₀, x₀) :: t ≃ []
Tactic:
exact
  if hz : a₀ = 0 then by
    rw [hz] at hyp₀
    rw [zero_add] at hyp₀
    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
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    let step : t ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    rw [hz]
    have ls : (0, x₀) :: t ≃ t := by
      apply Quot.sound
      apply ElementaryMove.zeroCoeff
      rfl
    exact Eq.trans ls step
  else by
    have non_zero : 0 ≠ coords t x₀ := by
      intro contra'
      let contra := Eq.symm contra'
      rw [contra, add_zero] at hyp₀
      contradiction
    let ⟨ys, eqnStep, lIneqStep⟩ := nonzero_coeff_has_complement x₀ t non_zero
    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
    have _ : ys.length < (h :: t).length := by
      simp [List.length_cons]
      apply Nat.le_trans lIneqStep
      apply Nat.le_succ
    let step : ys ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    let eqn₁ := cons_equiv_of_equiv _ _ (coords t x₀) x₀ step
    let eqn₂ : t ≃ (coords t x₀, x₀) :: [] := Eq.trans (Eq.symm eqnStep) eqn₁
    let eqn₃ := cons_equiv_of_equiv _ _ a₀ x₀ eqn₂
    apply Eq.trans eqn₃
    have eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)] := by
      apply Quot.sound
      apply ElementaryMove.addCoeffs
    apply Eq.trans eqn₄
    rw [hyp₀]
    apply Quot.sound
    apply ElementaryMove.zeroCoeff
    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₀ : monomCoeff R X x₀ (a₀, x₀) + coords t x₀ = 0
⊢ monomCoeff R X x₀ (a₀, x₀) = a₀
Tactic:
simp [monomCoeff]
Proof state after:
no goals