internlm/Lean-Github huggingface dataset:
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
simp only [neqLem]
Proof state after:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h
⊢ FormalSum.coords p x₁ = 0
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h
⊢ FormalSum.coords p x₁ = 0
Tactic:
by_cases FormalSum.coords p x₁ = 0
Proof state after:
case pos
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : FormalSum.coords p x₁ = 0
⊢ FormalSum.coords p x₁ = 0

case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
⊢ FormalSum.coords p x₁ = 0
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
⊢ (x == x₁) = false
Tactic:
apply beq_false_of_ne
Proof state after:
case h
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
⊢ x ≠ x₁
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
⊢ x ≠ x₁
Tactic:
assumption
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case pos
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : FormalSum.coords p x₁ = 0
⊢ FormalSum.coords p x₁ = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
hyp₃ : ¬Quotient.lift (fun s => FormalSum.coords s x₁)
        (_ : ∀ (a b : FormalSum R G), a ≈ b → FormalSum.coords a x₁ = FormalSum.coords b x₁)
        (Quotient.mk (formalSumSetoid R G) p) =
      0 →
  x₁ = x :=
  hyp₂ x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
⊢ FormalSum.coords p x₁ = 0
Tactic:
simp only [Quotient.lift_mk, h, not_false_iff, forall_true_left] at hyp₃
Proof state after:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
hyp₃ : x₁ = x
⊢ FormalSum.coords p x₁ = 0
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
hyp₃ : x₁ = x
⊢ FormalSum.coords p x₁ = 0
Tactic:
have := Eq.symm hyp₃
Proof state after:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
hyp₃ : x₁ = x
this : x = x₁
⊢ FormalSum.coords p x₁ = 0
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
x₁ : G
h✝ : ¬x = x₁
neqLem : (x == x₁) = false := beq_false_of_ne h✝
h : ¬FormalSum.coords p x₁ = 0
hyp₃ : x₁ = x
this : x = x₁
⊢ FormalSum.coords p x₁ = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
hyp₁ : (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x
hyp₂ : ∀ (y : G), FreeModule.coordinates y (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → y = x
⊢ FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ (∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0) → trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p)
Tactic:
intro ⟨a, g, hyp⟩
Proof state after:
case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p)
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p)
Tactic:
simp only [trivialNonZeroElem, ne_eq]
Proof state after:
case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ ∃! x, ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ ∃! x, ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0
Tactic:
use g
Proof state after:
case h
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g ∧
    ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g ∧
    ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g
Tactic:
apply And.intro
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g

case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g
Tactic:
intro h
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FreeModule.coordinates g (Quotient.mk (formalSumSetoid R G) p) = 0
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FreeModule.coordinates g (Quotient.mk (formalSumSetoid R G) p) = 0
⊢ False
Tactic:
simp only [FreeModule.coordinates, Quotient.lift_mk] at h
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords p g = 0
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords p g = 0
⊢ False
Tactic:
have : p.coords = FormalSum.coords [(a, g)] := hyp.left
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords p g = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords p g = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ False
Tactic:
rw [this] at h
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords [(a, g)] g = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
h : FormalSum.coords [(a, g)] g = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ False
Tactic:
simp only [FormalSum.coords, monomCoeff, beq_self_eq_true, add_zero] at h
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h : a = 0
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h : a = 0
⊢ False
Tactic:
have := hyp.right
Proof state after:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
this✝ : FormalSum.coords p = FormalSum.coords [(a, g)]
h : a = 0
this : a ≠ 0
⊢ False
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
this✝ : FormalSum.coords p = FormalSum.coords [(a, g)]
h : a = 0
this : a ≠ 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
⊢ ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g
Tactic:
intro x h
Proof state after:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0
⊢ x = g
Tactic:
simp only [FreeModule.coordinates, Quotient.lift_mk] at h
Proof state after:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords p x = 0
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords p x = 0
⊢ x = g
Tactic:
have : p.coords = FormalSum.coords [(a, g)] := hyp.left
Proof state after:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords p x = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords p x = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ x = g
Tactic:
rw [this] at h
Proof state after:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords [(a, g)] x = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
h : ¬FormalSum.coords [(a, g)] x = 0
this : FormalSum.coords p = FormalSum.coords [(a, g)]
⊢ x = g
Tactic:
simp only [FormalSum.coords, monomCoeff, add_zero] at h
Proof state after:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case h.right
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
⊢ x = g
Tactic:
by_cases c:x = g
Proof state after:
case pos
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : x = g
⊢ x = g

case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case pos
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : x = g
⊢ x = g
Tactic:
assumption
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
⊢ x = g
Tactic:
have neq : (g == x) = false := by aesop
Proof state after:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
neq : (g == x) = false
⊢ x = g
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
neq : (g == x) = false
⊢ x = g
Tactic:
simp only [neq, not_true] at h
Proof state after:
no goals
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof state before:
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
⊢ (g == x) = false
Tactic:
aesop
Proof state after:
no goals