-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem isInvertible_zero_iff :
    IsInvertible (0 : M →L[R] M₂) ↔ Subsingleton M ∧ Subsingleton M₂

Proof state:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ ↑e = 0

Tactic:
ext x

Result:
case refine_2.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
x : M
⊢ ↑e x = 0 x

Proof state:
case refine_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
A : Subsingleton M
⊢ Subsingleton M ∧ Subsingleton M₂

Tactic:
exact ⟨A, e.toEquiv.symm.subsingleton⟩

Result:
no goals

Proof state:
case refine_2.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
x : M
⊢ ↑e x = 0 x

Tactic:
exact Subsingleton.elim _ _

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
x y : M
⊢ e x = e y

Tactic:
simp [he, ← ContinuousLinearEquiv.coe_coe]

Result:
no goals

Proof state:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ IsInvertible 0

Tactic:
refine ⟨e, ?_⟩

Result:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ ↑e = 0

Proof state:
case refine_2
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
rintro ⟨hM, hM₂⟩

Result:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ IsInvertible 0

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂

Tactic:
refine ⟨fun ⟨e, he⟩ ↦ ?_, ?_⟩

Result:
case refine_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

case refine_2
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M

Tactic:
refine ⟨fun x y ↦ e.injective ?_⟩

Result:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
x y : M
⊢ e x = e y

Proof state:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ IsInvertible 0

Tactic:
let e : M ≃L[R] M₂ :=
{ toFun := 0
  invFun := 0
  left_inv x := Subsingleton.elim _ _
  right_inv x := Subsingleton.elim _ _
  map_add' x y := Subsingleton.elim _ _
  map_smul' c x := Subsingleton.elim _ _ }

Result:
case refine_2.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ IsInvertible 0

Proof state:
case refine_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

Tactic:
have A : Subsingleton M := by
  refine ⟨fun x y ↦ e.injective ?_⟩
  simp [he, ← ContinuousLinearEquiv.coe_coe]

Result:
case refine_1
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
A : Subsingleton M
⊢ Subsingleton M ∧ Subsingleton M₂