-- 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
mH : Quotient.out ↑y * h ∈ H
⊢ ↑1 = ↑y

Tactic:
rw [← QuotientGroup.out_eq' y.1, QuotientGroup.eq]

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⁻¹ * Quotient.out ↑y ∈ 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
⊢ x ∈ ⋃ i, Quotient.out ↑i • ↑H

Tactic:
simp only [ne_eq, Set.mem_iUnion]

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
⊢ ∃ i, x ∈ Quotient.out ↑i • ↑H

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

Tactic:
simp only [← hS] at 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
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
mem : x ∈ Quotient.out ↑y • ↑H
⊢ x ∈ (↑H)ᶜ

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 ∧ (fun x_1 => Quotient.out ↑⟨↑x, ⋯⟩ • x_1) ((Quotient.out ↑x)⁻¹ * x) = x

Tactic:
simp only [SetLike.mem_coe, smul_eq_mul, mul_inv_cancel_left, and_true]

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

Proof state:
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
y : { x // x ≠ ↑1 }
hS : (fun i => Quotient.out ↑i • ↑H) y = S
mem : x ∈ Quotient.out ↑y • ↑H
⊢ x ∈ (↑H)ᶜ

Tactic:
rcases mem with ⟨h,hh,eq⟩

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

Tactic:
simp only [← eq, ne_eq, smul_eq_mul] at 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 : Quotient.out ↑y * h ∈ H
⊢ False

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 ∉ H

Tactic:
simpa only [inv_one, one_mul, ne_eq]

Result:
no goals