Theorem: FreeModule.eqlquot_of_beq_support (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let ch₁ := eql_on_support_of_true c₁
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let ch₂ := eql_on_support_of_true c₂
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
apply Quotient.sound
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ s₁ ≈ s₂

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ s₁ ≈ s₂
Tactic:
apply funext
State after:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
intro x
State after:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
case a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
exact
  if h₁ : (0 = s₁.coords x) then
    if h₂ : (0 = s₂.coords x) then by
      rw [← h₁, h₂]
    else by
      have lem : x ∈ s₂.support := by
        apply nonzero_coord_in_support
        assumption
      let lem' := eq_mem_of_equalOnList s₂.support s₁.coords s₂.coords x lem ch₂
      exact lem'
  else by
    have lem : x ∈ s₁.support := by
      apply nonzero_coord_in_support
      assumption
    let lem' := eq_mem_of_equalOnList s₁.support s₁.coords s₂.coords x lem ch₁
    exact lem'
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : 0 = FormalSum.coords s₂ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
rw [← h₁, h₂]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
have lem : x ∈ s₂.support := by
  apply nonzero_coord_in_support
  assumption
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
lem : x ∈ FormalSum.support s₂
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
lem : x ∈ FormalSum.support s₂
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
let lem' := eq_mem_of_equalOnList s₂.support s₁.coords s₂.coords x lem ch₂
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
lem : x ∈ FormalSum.support s₂
lem' : FormalSum.coords s₁ x = FormalSum.coords s₂ x :=
  eq_mem_of_equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) x lem ch₂
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
lem : x ∈ FormalSum.support s₂
lem' : FormalSum.coords s₁ x = FormalSum.coords s₂ x :=
  eq_mem_of_equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) x lem ch₂
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
exact lem'
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
⊢ x ∈ FormalSum.support s₂
Tactic:
apply nonzero_coord_in_support
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
⊢ 0 ≠ FormalSum.coords s₂ x

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : 0 = FormalSum.coords s₁ x
h₂ : ¬0 = FormalSum.coords s₂ x
⊢ 0 ≠ FormalSum.coords s₂ x
Tactic:
assumption
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
have lem : x ∈ s₁.support := by
  apply nonzero_coord_in_support
  assumption
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
lem : x ∈ FormalSum.support s₁
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
lem : x ∈ FormalSum.support s₁
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
let lem' := eq_mem_of_equalOnList s₁.support s₁.coords s₂.coords x lem ch₁
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
lem : x ∈ FormalSum.support s₁
lem' : FormalSum.coords s₁ x = FormalSum.coords s₂ x :=
  eq_mem_of_equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) x lem ch₁
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
lem : x ∈ FormalSum.support s₁
lem' : FormalSum.coords s₁ x = FormalSum.coords s₂ x :=
  eq_mem_of_equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) x lem ch₁
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
exact lem'
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ x ∈ FormalSum.support s₁
Tactic:
apply nonzero_coord_in_support
State after:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ 0 ≠ FormalSum.coords s₁ x

State before:
case a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
c₁ : beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
c₂ : beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true
ch₁ : equalOnList (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₁
ch₂ : equalOnList (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) := eql_on_support_of_true c₂
x : X
h₁ : ¬0 = FormalSum.coords s₁ x
⊢ 0 ≠ FormalSum.coords s₁ x
Tactic:
assumption
State after:
no goals