case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹

case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
⊢ (↑K x)⁻¹ = ↑K x⁻¹
by_cases h : x = 0
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K 0)⁻¹ = ↑K 0
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
rw [h, inv_zero]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if ↑K 0 = 0 then 0 else hatInv (↑K 0)) = ↑K 0
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K 0)⁻¹ = ↑K 0
dsimp [Inv.inv]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if 0 = 0 then 0 else hatInv 0) = 0
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if ↑K 0 = 0 then 0 else hatInv (↑K 0)) = ↑K 0
norm_cast
no goals
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if 0 = 0 then 0 else hatInv 0) = 0
simp
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑K x = 0 then 0 else hatInv (↑K x)) = ↑K x⁻¹
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
conv_lhs => dsimp [Inv.inv]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ hatInv (↑K x) = ↑K x⁻¹

case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑K x = 0
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑K x = 0 then 0 else hatInv (↑K x)) = ↑K x⁻¹
rw [if_neg]
no goals
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ hatInv (↑K x) = ↑K x⁻¹
exact hatInv_extends h
no goals
case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑K x = 0
exact fun H => h (denseEmbedding_coe.inj H)