Theorem: Gardam.α_nonTrivial (UnitConjecture/GardamTheorem.lean)

State before:
⊢ ¬trivialNonZeroElem α
Tactic:
intro ⟨g, _, (eqg : ∀ y, α.coordinates y ≠ 0 → y = g)⟩
State after:
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
⊢ False

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

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

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

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

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

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

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

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

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