-- Mathlib/Topology/Algebra/UniformField.lean
theorem coe_inv (x : K) : (x : hat K)⁻¹ = ((x⁻¹ : K) : hat K)

Proof state:
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 (↑0).hatInv) = ↑0

Tactic:
norm_cast

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

Proof state:
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

Tactic:
simp

Result:
no goals

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

Tactic:
dsimp [Inv.inv]

Result:
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 (↑0).hatInv) = ↑0

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

Tactic:
conv_lhs => dsimp [Inv.inv]

Result:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑x = 0 then 0 else (↑x).hatInv) = ↑x⁻¹

Proof state:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑x = 0 then 0 else (↑x).hatInv) = ↑x⁻¹

Tactic:
rw [if_neg]

Result:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑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
⊢ ¬↑x = 0

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

Tactic:
rw [h, inv_zero]

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

Proof state:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹

Tactic:
exact hatInv_extends h

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
⊢ (↑x)⁻¹ = ↑x⁻¹

Tactic:
by_cases h : x = 0

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

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

Proof state:
case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0

Tactic:
exact fun H => h (isDenseEmbedding_coe.injective H)

Result:
no goals