internlm/Lean-Github huggingface dataset:
Theorem: Path.length_append
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p') + length q
Tactic:
rw [Nat.succ_add]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p' + length q)
Theorem: Path.length_append
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p' + length q)
Tactic:
apply congrArg
Proof state after:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ length (append p' q) = length p' + length q
Theorem: Path.length_append
Proof state before:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ length (append p' q) = length p' + length q
Tactic:
apply length_append
Proof state after:
no goals
Theorem: Path.last_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons' x✝³ x✝² x✝² a✝ nil) x✝) = x✝²
Tactic:
rw [snoc_cons]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (cons a✝ (snoc nil x✝)) = x✝²
Theorem: Path.last_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ : V
a✝ : x✝³ ⟶ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (cons a✝ (snoc nil x✝)) = x✝²
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.last_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons' x✝³ B✝¹ x✝² a✝² (cons a✝¹ a✝)) x✝) = x✝²
Tactic:
rw [snoc_cons, snoc, last, ← snoc_cons]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons a✝¹ a✝) x✝) = x✝²
Theorem: Path.last_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons a✝¹ a✝) x✝) = x✝²
Tactic:
apply last_snoc
Proof state after:
no goals
Theorem: Gardam.α_nonTrivial
Proof state before:
⊢ ¬trivialNonZeroElem α
Tactic:
intro ⟨g, _, (eqg : ∀ y, α.coordinates y ≠ 0 → y = g)⟩
Proof state after:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ False
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ False
Tactic:
have : z⁻¹ = g := by
  apply eqg; native_decide
Proof state after:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ False
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ False
Tactic:
have : x * y = g := by
  apply eqg; native_decide
Proof state after:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝ : z⁻¹ = g
this : x * y = g
⊢ False
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝ : z⁻¹ = g
this : x * y = g
⊢ False
Tactic:
have : z⁻¹ = x * y := by
  refine' Eq.trans _ (Eq.symm _) <;> assumption
Proof state after:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝¹ : z⁻¹ = g
this✝ : x * y = g
this : z⁻¹ = x * y
⊢ False
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝¹ : z⁻¹ = g
this✝ : x * y = g
this : z⁻¹ = x * y
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ z⁻¹ = g
Tactic:
apply eqg
Proof state after:
case a
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ FreeModule.coordinates z⁻¹ α ≠ 0
Theorem: Gardam.α_nonTrivial
Proof state before:
case a
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ FreeModule.coordinates z⁻¹ α ≠ 0
Tactic:
native_decide
Proof state after:
no goals
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ x * y = g
Tactic:
apply eqg
Proof state after:
case a
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ FreeModule.coordinates (x * y) α ≠ 0
Theorem: Gardam.α_nonTrivial
Proof state before:
case a
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ FreeModule.coordinates (x * y) α ≠ 0
Tactic:
native_decide
Proof state after:
no goals
Theorem: Gardam.α_nonTrivial
Proof state before:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝ : z⁻¹ = g
this : x * y = g
⊢ z⁻¹ = x * y
Tactic:
refine' Eq.trans _ (Eq.symm _) <;> assumption
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
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) ↔ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
Tactic:
apply Iff.intro
Proof 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)
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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]
Proof 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
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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⟩
Proof 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
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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
Proof 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
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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⟧
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
⊢ ∃ g,
    p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), g)] ∧
      FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0
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
⊢ ∃ 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
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
⊢ p ≈ [(FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p), x)] ∧
    FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0
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
⊢ 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
Proof 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
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
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₁
Proof 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₁
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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]
Proof 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
Theorem: trivialNonZeroElem_trivial_nonzeroAux
Proof 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₁
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₁
⊢ 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
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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
simp [h]
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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0
Tactic:
let hyp₃ := hyp₂ x₁
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₃ : 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
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₃ : 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₃
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₁
⊢ FormalSum.coords p x₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 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₁
⊢ 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
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₁ =
    match x == x₁ with
    | true => FormalSum.coords p x
    | false => 0