internlm/Lean-Github huggingface dataset:
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
let factorizes : (s : FormalSum R X) → g (s.sum) = sum ((a, x) :: s) := Quot.liftBeta f wit
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ (a, x) :: s₁ ≃ (a, x) :: s₂
Tactic:
rw [equiv]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ sum ((a, x) :: s₁) = sum ((a, x) :: s₂)
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ sum ((a, x) :: s₁) = sum ((a, x) :: s₂)
Tactic:
rw [← factorizes]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ g (sum s₁) = sum ((a, x) :: s₂)
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ g (sum s₁) = sum ((a, x) :: s₂)
Tactic:
rw [← factorizes]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ g (sum s₁) = g (sum s₂)
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
wit : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂ :=
  fun s₁ s₂ hyp => Quot.sound (ElementaryMove.cons a x s₁ s₂ hyp)
g : (Quot fun a b => ElementaryMove R X a b) → FreeModuleAux R X := Quot.lift f wit
factorizes : ∀ (s : FormalSum R X), g (sum s) = sum ((a, x) :: s) := Quot.liftBeta f wit
⊢ g (sum s₁) = g (sum s₂)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
a : R
x : X
h : s₁ ≃ s₂
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
⊢ ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
Tactic:
intro s₁ s₂ hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ f s₁ = f s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ f s₁ = f 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
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ ElementaryMove R X ((a, x) :: s₁) ((a, x) :: s₂)
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ ElementaryMove R X ((a, x) :: s₁) ((a, x) :: s₂)
Tactic:
apply ElementaryMove.cons
Proof state after:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ ElementaryMove R X s₁ s₂
Theorem: FormalSum.cons_equiv_of_equiv
Proof state before:
case a.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
h : s₁✝ ≃ s₂✝
f : FormalSum R X → FreeModuleAux R X := fun s => sum ((a, x) :: s)
s₁ s₂ : FormalSum R X
hyp : ElementaryMove R X s₁ s₂
⊢ ElementaryMove R X s₁ s₂
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
s : FormalSum R X
⊢ 0 ≠ coords s x₀ → ∃ ys, (coords s x₀, x₀) :: ys ≃ s ∧ List.length ys < List.length s
Tactic:
induction s with
| nil =>
  intro contra
  contradiction
| cons head tail hyp =>
  let (a, x) := head
  intro pos
  cases c : x == x₀ with
  | true =>
    let k := FormalSum.coords tail x₀
    have lem : a + k = coords ((a, x) :: tail) x₀ := by
      rw [coords, monomCoeff, c]
    have c'' : x = x₀ := of_decide_eq_true c
    rw [c'']
    rw [c''] at lem
    exact
      if c' : (0 = k) then by
        have lIneq : tail.length < List.length ((a, x) :: tail) := by
          simp [List.length_cons]
        rw [← c', add_zero] at lem
        rw [← lem]
        exact ⟨tail, rfl, lIneq⟩
      else by
        let ⟨ys, eqnStep, lIneqStep⟩ := hyp c'
        have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by
          apply Quot.sound
          apply ElementaryMove.addCoeffs
        have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by
          apply cons_equiv_of_equiv
          assumption
        have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂
        rw [← lem]
        have lIneq : ys.length < List.length ((a, x₀) :: tail) := by
          apply Nat.le_trans lIneqStep
          simp [List.length_cons, Nat.le_succ]
        exact ⟨ys, eqn, lIneq⟩
  | false =>
    let k := coords tail x₀
    have lem : k = coords ((a, x) :: tail) x₀ := by
      simp [coords, monomCoeff, c, zero_add]
    rw [← lem] at pos
    let ⟨ys', eqnStep, lIneqStep⟩ := hyp pos
    rw [← lem]
    let ys := (a, x) :: ys'
    have lIneq : ys.length < ((a, x) :: tail).length := by
      simp [List.length_cons]
      apply Nat.succ_lt_succ
      exact lIneqStep
    have eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys' := by
      apply Quot.sound
      apply ElementaryMove.swap
    have eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail := by
      apply cons_equiv_of_equiv
      assumption
    have eqn : (k, x₀) :: ys ≃ (a, x) :: tail := by
      exact Eq.trans eqn₁ eqn₂
    exact ⟨ys, eqn, lIneq⟩
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
⊢ 0 ≠ coords [] x₀ → ∃ ys, (coords [] x₀, x₀) :: ys ≃ [] ∧ List.length ys < List.length []
Tactic:
intro contra
Proof state after:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
contra : 0 ≠ coords [] x₀
⊢ ∃ ys, (coords [] x₀, x₀) :: ys ≃ [] ∧ List.length ys < List.length []
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
contra : 0 ≠ coords [] x₀
⊢ ∃ ys, (coords [] x₀, x₀) :: ys ≃ [] ∧ List.length ys < List.length []
Tactic:
contradiction
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons
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
⊢ 0 ≠ coords (head :: tail) x₀ →
    ∃ ys, (coords (head :: tail) x₀, x₀) :: ys ≃ head :: tail ∧ List.length ys < List.length (head :: tail)
Tactic:
let (a, x) := head
Proof state after:
case cons
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
⊢ 0 ≠ 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
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
⊢ 0 ≠ 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:
intro pos
Proof state after:
case cons
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₀
⊢ ∃ 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
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₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
cases c : x == x₀ with
| true =>
  let k := FormalSum.coords tail x₀
  have lem : a + k = coords ((a, x) :: tail) x₀ := by
    rw [coords, monomCoeff, c]
  have c'' : x = x₀ := of_decide_eq_true c
  rw [c'']
  rw [c''] at lem
  exact
    if c' : (0 = k) then by
      have lIneq : tail.length < List.length ((a, x) :: tail) := by
        simp [List.length_cons]
      rw [← c', add_zero] at lem
      rw [← lem]
      exact ⟨tail, rfl, lIneq⟩
    else by
      let ⟨ys, eqnStep, lIneqStep⟩ := hyp c'
      have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by
        apply Quot.sound
        apply ElementaryMove.addCoeffs
      have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by
        apply cons_equiv_of_equiv
        assumption
      have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂
      rw [← lem]
      have lIneq : ys.length < List.length ((a, x₀) :: tail) := by
        apply Nat.le_trans lIneqStep
        simp [List.length_cons, Nat.le_succ]
      exact ⟨ys, eqn, lIneq⟩
| false =>
  let k := coords tail x₀
  have lem : k = coords ((a, x) :: tail) x₀ := by
    simp [coords, monomCoeff, c, zero_add]
  rw [← lem] at pos
  let ⟨ys', eqnStep, lIneqStep⟩ := hyp pos
  rw [← lem]
  let ys := (a, x) :: ys'
  have lIneq : ys.length < ((a, x) :: tail).length := by
    simp [List.length_cons]
    apply Nat.succ_lt_succ
    exact lIneqStep
  have eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys' := by
    apply Quot.sound
    apply ElementaryMove.swap
  have eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail := by
    apply cons_equiv_of_equiv
    assumption
  have eqn : (k, x₀) :: ys ≃ (a, x) :: tail := by
    exact Eq.trans eqn₁ eqn₂
  exact ⟨ys, eqn, lIneq⟩
Proof state after:
no goals
Theorem: FormalSum.nonzero_coeff_has_complement
Proof state before:
case cons.true
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
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
let k := FormalSum.coords tail x₀
Proof state after:
case cons.true
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₀
⊢ ∃ 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.true
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₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have lem : a + k = coords ((a, x) :: tail) x₀ := by
  rw [coords, monomCoeff, c]
Proof state after:
case cons.true
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₀
⊢ ∃ 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.true
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₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
have c'' : x = x₀ := of_decide_eq_true c
Proof state after:
case cons.true
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₀
⊢ ∃ 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.true
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₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
Tactic:
rw [c'']
Proof state after:
case cons.true
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₀
⊢ ∃ 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.true
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₀
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
rw [c''] at lem
Proof state after:
case cons.true
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₀
⊢ ∃ 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.true
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₀
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
Tactic:
exact
  if c' : (0 = k) then by
    have lIneq : tail.length < List.length ((a, x) :: tail) := by
      simp [List.length_cons]
    rw [← c', add_zero] at lem
    rw [← lem]
    exact ⟨tail, rfl, lIneq⟩
  else by
    let ⟨ys, eqnStep, lIneqStep⟩ := hyp c'
    have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by
      apply Quot.sound
      apply ElementaryMove.addCoeffs
    have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by
      apply cons_equiv_of_equiv
      assumption
    have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂
    rw [← lem]
    have lIneq : ys.length < List.length ((a, x₀) :: tail) := by
      apply Nat.le_trans lIneqStep
      simp [List.length_cons, Nat.le_succ]
    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₀
⊢ a + k = coords ((a, x) :: tail) x₀
Tactic:
rw [coords, monomCoeff, c]
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:
have lIneq : tail.length < List.length ((a, x) :: tail) := by
  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
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)