-- Mathlib/Topology/Algebra/Group/Basic.lean
/-- Let `A` and `B` be topological groups, and let `φ : A → B` be a continuous surjective group
homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map. -/
@[to_additive "Let `A` and `B` be topological additive groups, and let `φ : A → B` be a continuous
surjective additive group homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map."]
lemma MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A]
    [TopologicalSpace A] [IsTopologicalGroup A] {B : Type*} [Group B] [TopologicalSpace B]
    {F : Type*} [FunLike F A B] [MonoidHomClass F A B] {φ : F}
    (hφ : IsQuotientMap φ) : IsOpenQuotientMap φ where
    surjective := hφ.surjective
    continuous := hφ.continuous
    isOpenMap

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ IsOpen (⇑φ '' U)

Tactic:
rw [← hφ.isOpen_preimage]

Result:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ IsOpen (⇑φ ⁻¹' (⇑φ '' U))

Proof state:
case right
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x k : A
hk : φ k = 1
hx : x ∈ (fun h => (fun x => x * k) ⁻¹' U) hk
⊢ φ (x * k) = φ x

Tactic:
rw [map_mul, hk, mul_one]

Result:
no goals

Proof state:
case h.mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U) → x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Tactic:
rintro ⟨y, hyU, hyx⟩

Result:
case h.mp.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x y : A
hyU : y ∈ U
hyx : φ y = φ x
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
this : ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U
k : A
x✝ : k ∈ ↑(↑φ).ker
⊢ Continuous fun x => x * k

Tactic:
fun_prop

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ IsOpen (⇑φ ⁻¹' (⇑φ '' U))

Tactic:
suffices ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
  exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)

Result:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Proof state:
case h.mp.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x y : A
hyU : y ∈ U
hyx : φ y = φ x
⊢ x ∈ ⋃ (_ : x⁻¹ * y ∈ (↑φ).ker), (fun x_1 => x_1 * (x⁻¹ * y)) ⁻¹' U

Tactic:
simp_all

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Tactic:
ext x

Result:
case h
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U) ↔ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
this : ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U
⊢ IsOpen (⇑φ ⁻¹' (⇑φ '' U))

Tactic:
exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)

Result:
no goals

Proof state:
case h.mp.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x y : A
hyU : y ∈ U
hyx : φ y = φ x
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Tactic:
apply Set.mem_iUnion_of_mem (x⁻¹ * y)

Result:
case h.mp.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x y : A
hyU : y ∈ U
hyx : φ y = φ x
⊢ x ∈ ⋃ (_ : x⁻¹ * y ∈ (↑φ).ker), (fun x_1 => x_1 * (x⁻¹ * y)) ⁻¹' U

Proof state:
case h
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U) ↔ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

Tactic:
constructor

Result:
case h.mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U) → x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U

case h.mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' (⇑φ '' U)