Theorem: FormalSum.nonzero_coeff_has_complement (UnitConjecture/FreeModule.lean)

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⟩
State after:
no goals

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
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 []

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
State after:
no goals

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
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)

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
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)

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⟩
State after:
no goals

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₀
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)

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]
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)

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
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)

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'']
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)

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
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)

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⟩
State after:
no goals

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]
State after:
no goals

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]
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)

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
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)

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]
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)

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⟩
State after:
no goals

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]
State after:
no goals

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'
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)

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
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)

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
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)

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₂
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)

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]
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)

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]
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)

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⟩
State after:
no goals

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
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)

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
State after:
no goals

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
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

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
State after:
no goals

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
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)

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]
State after:
no goals

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₀
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)

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]
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)

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
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)

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
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)

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]
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)

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'
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)

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
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)

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
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)

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
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)

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₂
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)

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⟩
State after:
no goals

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]
State after:
no goals

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]
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)

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
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

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
State after:
no goals

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
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')

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
State after:
no goals

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
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

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
State after:
no goals

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₂
State after:
no goals