-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_self_pos [ExistsAddOfLE α] [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftStrictMono α] [AddLeftReflectLT α]
    {a : α} : 0 < a * a ↔ a ≠ 0

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
⊢ 0 < a * a ↔ a ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
⊢ 0 < a * a → a ≠ 0

case mpr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
⊢ a ≠ 0 → 0 < a * a

Proof state:
case mpr.inl
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

case mpr.inr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a

Tactic:
exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

Result:
no goals

Proof state:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
⊢ 0 < a * a → a ≠ 0

Tactic:
rintro h rfl

Result:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
h : 0 < 0 * 0
⊢ False

Proof state:
case mpr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
⊢ a ≠ 0 → 0 < a * a

Tactic:
intro h

Result:
case mpr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h : a ≠ 0
⊢ 0 < a * a

Proof state:
case mpr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h : a ≠ 0
⊢ 0 < a * a

Tactic:
rcases h.lt_or_lt with h | h

Result:
case mpr.inl
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

case mpr.inr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
a : α
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a

Proof state:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
h : 0 < 0 * 0
⊢ False

Tactic:
rw [mul_zero] at h

Result:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
h : 0 < 0
⊢ False

Proof state:
case mp
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddLeftReflectLT α
h : 0 < 0
⊢ False

Tactic:
exact h.false

Result:
no goals