internlm/Lean-Github huggingface dataset:
Theorem: eqlCoords.symm
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : eqlCoords R X s₁ s₂
x : X
⊢ FormalSum.coords s₂ x = FormalSum.coords s₁ x
Tactic:
apply Eq.symm
Proof state after:
case h.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : eqlCoords R X s₁ s₂
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Theorem: eqlCoords.symm
Proof state before:
case h.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : eqlCoords R X s₁ s₂
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₂ x
Tactic:
exact congrFun hyp x
Proof state after:
no goals
Theorem: eqlCoords.trans
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
⊢ eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₃ → eqlCoords R X s₁ s₃
Tactic:
intro hyp₁ hyp₂
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
⊢ eqlCoords R X s₁ s₃
Theorem: eqlCoords.trans
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
⊢ eqlCoords R X s₁ s₃
Tactic:
apply funext
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₃ x
Theorem: eqlCoords.trans
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
⊢ ∀ (x : X), FormalSum.coords s₁ x = FormalSum.coords s₃ x
Tactic:
intro x
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Theorem: eqlCoords.trans
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Tactic:
have l₁ := congrFun hyp₁ x
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
l₁ : FormalSum.coords s₁ x = FormalSum.coords s₂ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Theorem: eqlCoords.trans
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
l₁ : FormalSum.coords s₁ x = FormalSum.coords s₂ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Tactic:
have l₂ := congrFun hyp₂ x
Proof state after:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
l₁ : FormalSum.coords s₁ x = FormalSum.coords s₂ x
l₂ : FormalSum.coords s₂ x = FormalSum.coords s₃ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Theorem: eqlCoords.trans
Proof state before:
case h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ s₃ : FormalSum R X
hyp₁ : eqlCoords R X s₁ s₂
hyp₂ : eqlCoords R X s₂ s₃
x : X
l₁ : FormalSum.coords s₁ x = FormalSum.coords s₂ x
l₂ : FormalSum.coords s₂ x = FormalSum.coords s₃ x
⊢ FormalSum.coords s₁ x = FormalSum.coords s₃ x
Tactic:
exact Eq.trans l₁ l₂
Proof state after:
no goals
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
⊢ beqOnSupport l f g = true → equalOnList l f g
Tactic:
intro hyp
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
hyp : beqOnSupport l f g = true
⊢ equalOnList l f g
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
l : List X
f g : X → R
hyp : beqOnSupport l f g = true
⊢ equalOnList l f g
Tactic:
induction l with
| nil =>
  simp [equalOnList]
| cons h t step =>
  simp [equalOnList]
  simp [beqOnSupport, List.all] at hyp
  let p₂ := step hyp.right
  exact And.intro hyp.left p₂
Proof state after:
no goals
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
case nil
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
hyp : beqOnSupport [] f g = true
⊢ equalOnList [] f g
Tactic:
simp [equalOnList]
Proof state after:
no goals
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ equalOnList (h :: t) f g
Tactic:
simp [equalOnList]
Proof state after:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ f h = g h ∧ equalOnList t f g
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : beqOnSupport (h :: t) f g = true
⊢ f h = g h ∧ equalOnList t f g
Tactic:
simp [beqOnSupport, List.all] at hyp
Proof state after:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
⊢ f h = g h ∧ equalOnList t f g
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
⊢ f h = g h ∧ equalOnList t f g
Tactic:
let p₂ := step hyp.right
Proof state after:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
p₂ : equalOnList t f g := step hyp.right
⊢ f h = g h ∧ equalOnList t f g
Theorem: FreeModule.eql_on_support_of_true
Proof state before:
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
f g : X → R
h : X
t : List X
step : beqOnSupport t f g = true → equalOnList t f g
hyp : f h = g h ∧ List.foldr (fun a r => decide (f a = g a) && r) true t = true
p₂ : equalOnList t f g := step hyp.right
⊢ f h = g h ∧ equalOnList t f g
Tactic:
exact And.intro hyp.left p₂
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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₁
Proof 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₂
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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₂
Proof 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₂
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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₂
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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'
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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₂]
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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₂
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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'
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof state after:
no goals
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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
Proof 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
Theorem: FreeModule.eqlquot_of_beq_support
Proof 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₁
Proof 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