case pos
x : ℝ*
h0 : x = 0
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
x : ℝ*
⊢ st x⁻¹ = (st x)⁻¹
by_cases h0 : x = 0
case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
case pos
x : ℝ*
h0 : x = 0
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
by_cases h1 : Infinitesimal x
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
case pos
x : ℝ*
h0 : ¬x = 0
h1 : Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : Infinite x
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
by_cases h2 : Infinite x
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : Infinite x
⊢ st x⁻¹ = (st x)⁻¹

case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
no goals
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
exact ((isSt_st' h2).inv h1).st_eq