-- Mathlib/Topology/Algebra/ClosedSubgroup.lean
@[to_additive]
lemma isOpen_of_isClosed_of_finiteIndex (H : Subgroup G) [H.FiniteIndex]
    (h : IsClosed (H : Set G)) : IsOpen (H : Set G)

Proof state:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
⊢ x ∈ (↑H)ᶜ

Tactic:
simp only [Set.mem_compl_iff, SetLike.mem_coe]

Result:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
⊢ x ∉ H

Proof state:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsClosed (↑H)ᶜ

Tactic:
convert isClosed_iUnion_of_finite <| fun (x : {x : (G ⧸ H) // x ≠ QuotientGroup.mk 1})
  ↦ IsClosed.smul h (Quotient.out x.1)

Result:
case h.e'_3
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ (↑H)ᶜ = ⋃ i, Quotient.out ↑i • ↑H

Proof state:
case h.e'_3.h.refine_1
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
this : ↑1 ≠ ↑x
⊢ ∃ i, x ∈ Quotient.out ↑i • ↑H

Tactic:
use ⟨QuotientGroup.mk (s := H) x, this.symm⟩,
  (Quotient.out (QuotientGroup.mk (s := H) x))⁻¹ * x

Result:
case h
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
this : ↑1 ≠ ↑x
⊢ (Quotient.out ↑x)⁻¹ * x ∈ ↑H ∧ (fun x_1 => Quotient.out ↑⟨↑x, ⋯⟩ • x_1) ((Quotient.out ↑x)⁻¹ * x) = x

Proof state:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
⊢ ↑1 ≠ ↑x

Tactic:
apply QuotientGroup.eq.not.mpr

Result:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
⊢ 1⁻¹ * x ∉ H

Proof state:
case h.e'_3.h
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
x : G
⊢ x ∈ (↑H)ᶜ ↔ x ∈ ⋃ i, Quotient.out ↑i • ↑H

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.e'_3.h.refine_1
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
⊢ x ∈ ⋃ i, Quotient.out ↑i • ↑H

case h.e'_3.h.refine_2
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ ⋃ i, Quotient.out ↑i • ↑H
⊢ x ∈ (↑H)ᶜ

Proof state:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
mH : Quotient.out ↑y * h ∈ H
⊢ 1⁻¹ * Quotient.out ↑y ∈ H

Tactic:
simp only [inv_one, ne_eq, one_mul, (Subgroup.mul_mem_cancel_right H hh).mp mH]

Result:
no goals

Proof state:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
mH : Quotient.out ↑y * h ∈ H
⊢ False

Tactic:
absurd y.2.symm

Result:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
mH : Quotient.out ↑y * h ∈ H
⊢ ↑1 = ↑y

Proof state:
case h
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
this : ↑1 ≠ ↑x
⊢ (Quotient.out ↑x)⁻¹ * x ∈ H

Tactic:
exact QuotientGroup.eq.mp <| QuotientGroup.out_eq' (QuotientGroup.mk (s := H) x)

Result:
no goals

Proof state:
case h.e'_3.h.refine_2
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ ⋃ i, Quotient.out ↑i • ↑H
⊢ x ∈ (↑H)ᶜ

Tactic:
rcases h with ⟨S,⟨y,hS⟩,mem⟩

Result:
case h.e'_3.h.refine_2.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
x : G
S : Set G
mem : x ∈ S
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
⊢ x ∈ (↑H)ᶜ

Proof state:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsOpen ↑H

Tactic:
apply isClosed_compl_iff.mp

Result:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsClosed (↑H)ᶜ

Proof state:
case h.e'_3.h.refine_1
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
⊢ x ∈ ⋃ i, Quotient.out ↑i • ↑H

Tactic:
have : QuotientGroup.mk 1 ≠ QuotientGroup.mk (s := H) x := by
  apply QuotientGroup.eq.not.mpr
  simpa only [inv_one, one_mul, ne_eq]

Result:
case h.e'_3.h.refine_1
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
h : x ∈ (↑H)ᶜ
this : ↑1 ≠ ↑x
⊢ x ∈ ⋃ i, Quotient.out ↑i • ↑H

Proof state:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
⊢ x ∉ H

Tactic:
by_contra mH

Result:
case h.e'_3.h.refine_2.intro.intro.intro.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h✝ : IsClosed ↑H
x : G
S : Set G
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
h : G
hh : h ∈ ↑H
eq : (fun x => Quotient.out ↑y • x) h = x
mH : x ∈ H
⊢ False

Proof state:
case h.e'_3
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ (↑H)ᶜ = ⋃ i, Quotient.out ↑i • ↑H

Tactic:
ext x

Result:
case h.e'_3.h
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
x : G
⊢ x ∈ (↑H)ᶜ ↔ x ∈ ⋃ i, Quotient.out ↑i • ↑H