Theorem: trivialNonZeroElem_trivial_nonzeroAux (UnitConjecture/GardamTheorem.lean)

State before:
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) ↔ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
apply Iff.intro
State after:
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0

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)

State before:
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
rw [trivialNonZeroElem]
State after:
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ (∃! x, FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0

State before:
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ (∃! x, FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
intro ⟨x, hyp⟩
State after:
case mp
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
⊢ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0

State before:
case mp
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
⊢ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
let ⟨hyp₁, hyp₂⟩ := hyp
State after:
case mp
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
⊢ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0

State before:
case mp
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
⊢ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
use FreeModule.coordinates x ⟦p⟧
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
⊢ ∃ g,
    p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), g)] ∧
      FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0

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
⊢ ∃ g,
    p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), g)] ∧
      FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0
Tactic:
use x
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
⊢ p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)] ∧
    FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0

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
⊢ p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)] ∧
    FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0
Tactic:
apply And.intro
State after:
case h.left
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
⊢ p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)]

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

State before:
case h.left
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
⊢ p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)]
Tactic:
funext x₁
State after:
case h.left.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
⊢ FormalSum.coords p x₁ = FormalSum.coords [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)] x₁

State before:
case h.left.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
⊢ FormalSum.coords p x₁ = FormalSum.coords [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)] x₁
Tactic:
simp only [FormalSum.coords, monomCoeff, FreeModule.coordinates, Quotient.lift_mk, add_zero]
State after:
case h.left.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
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0

State before:
case h.left.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
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
by_cases x = x₁
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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0

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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
simp [h]
State after:
no goals

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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
let hyp₃ := hyp₂ x₁
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₃ : FreeModule.coordinates x₁ (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → x₁ = x := hyp₂ x₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0

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₃ : FreeModule.coordinates x₁ (Quotient.mk (formalSumSetoid R G) p) ≠ 0 → x₁ = x := hyp₂ x₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
simp only [h, FreeModule.coordinates, Quot.lift_mk, ne_eq] at hyp₃
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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0

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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
let neqLem : ((x == x₁) = false) := 
  by apply beq_false_of_ne; assumption
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₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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