mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
n : ℕ
⊢ ↑(s n) ≠ ∅

Tactic:
]

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
n : ℕ
⊢ ↑(s n) ≠ ∅
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * ((↑(hHT.equiv g₁).1)⁻¹ * g₁)⁻¹ ∈ ↑H

Tactic:
]

Goal state after:
case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * ((↑(hHT.equiv g₁).1)⁻¹ * g₁)⁻¹ ∈ ↑H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * g₁⁻¹ * (g₁ * (↑(hHT.equiv g₂).2)⁻¹) ∈ H

Tactic:
]

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * g₁⁻¹ * (g₁ * (↑(hHT.equiv g₂).2)⁻¹) ∈ H
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (⇑f.symm '' A)
U : Set α
hAU : U ⊇ ⇑f.symm '' A
hUo : IsOpen[inst✝⁵] U
hU : μ U < r
this : IsOpen[inst✝²] (⇑f.symm ⁻¹' U)
⊢ μ U < r

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (⇑f.symm '' A)
U : Set α
hAU : U ⊇ ⇑f.symm '' A
hUo : IsOpen[inst✝⁵] U
hU : μ U < r
this : IsOpen[inst✝²] (⇑f.symm ⁻¹' U)
⊢ μ U < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * (g₁⁻¹ * (g₁ * ((↑(hHT.equiv g₂).1)⁻¹ * g₂)⁻¹)) ∈ H

Tactic:
]

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * (g₁⁻¹ * (g₁ * ((↑(hHT.equiv g₂).1)⁻¹ * g₂)⁻¹)) ∈ H
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (comap f μ) U < r

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (comap f μ) U < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ (↑(hHT.equiv g).1)⁻¹ * g * g⁻¹ ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ (↑(hHT.equiv g).1)⁻¹ * g * g⁻¹ ∈ H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ { toFun := fun x ↦ ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨g, hg⟩, ⟨1, h1⟩) = g

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ { toFun := fun x ↦ ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ f '' A ⊆ U

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ f '' A ⊆ U
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ { toFun := fun x ↦ ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨1, h1⟩, ⟨g, hg⟩) = g

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ { toFun := fun x ↦ ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ μ (f '' f ⁻¹' U) < r

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ μ (f '' f ⁻¹' U) < r
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ∞
⊢ OuterRegular 0

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
hx : 0 ≠ ∞
⊢ OuterRegular 0
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ 1 = ↑⟨1, h1⟩

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ 1 = ↑⟨1, h1⟩

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ ↑(hST.equiv g).1 = ↑⟨1, h1⟩

Tactic:
rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
m n : ℕ
⊢ ¬Disjoint ↑(s m) ↑(s n)

Tactic:
]

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
m n : ℕ
⊢ ¬Disjoint ↑(s m) ↑(s n)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst✝¹] U), μ U
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst✝¹] U), μ U
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case fst
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv g).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ (↑(hSK.equiv g).1)⁻¹ * (g * ↑k) = (↑(hSK.equiv g).1)⁻¹ * (g * ↑k)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ A = A

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.fst
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑h * (g * (↑(hHT.equiv g).2)⁻¹) = ↑h * (g * (↑(hHT.equiv g).2)⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.snd
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv g).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ 1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ 1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : ↑(hST.equiv g).1 = g
⊢ ↑(hST.equiv g).1 ∈ S

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : ↑(hST.equiv g).1 = g
⊢ ↑(hST.equiv g).1 ∈ S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
h : g ∈ S
⊢ ↑⟨g, h⟩ = g

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
⊢ ∃ U ⊇ ⋃ n, A n, IsOpen[inst✝¹] U ∧ μ U < r

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
⊢ ∃ U ⊇ ⋃ n, A n, IsOpen[inst✝¹] U ∧ μ U < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ ↑(hST.equiv g).2 ∈ T

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : ↑(hST.equiv g).2 = g
⊢ ↑(hST.equiv g).2 ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ ↑⟨g, h⟩ = g

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g ∈ T ↔ g ∈ T

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ g ∈ S ↔ g ∈ S

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
⊢ μ (A n ∩ s n) ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
⊢ μ (A n ∩ s n) ≠ ∞
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ g⁻¹ * ↑(hS.toLeftFun g) = g⁻¹ * ↑(hS.toLeftFun g)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ ↑(hT.toRightFun g) * g⁻¹ = ↑(hT.toRightFun g) * g⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
S : Set G
inst✝ : H.FiniteIndex
h : IsComplement S ↑H
⊢ ↑H.index = ↑H.index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
T : Set G
inst✝ : H.FiniteIndex
h : IsComplement (↑H) T
⊢ ↑H.index = ↑H.index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv q)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h : μ = ν
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ ν (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
Ht : (μ.restrict (s n)) (A n) ≠ ∞
U : Set α
hAU : U ⊇ A n
hUo : IsOpen[inst✝¹] U
hU : μ (U ∩ s n) < μ (A n) + δ n
⊢ ∃ U ⊇ A n, IsOpen[inst✝¹] U ∧ μ U < μ (A n) + δ n

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
Ht : (μ.restrict (s n)) (A n) ≠ ∞
U : Set α
hAU : U ⊇ A n
hUo : IsOpen[inst✝¹] U
hU : μ (U ∩ s n) < μ (A n) + δ n
⊢ ∃ U ⊇ A n, IsOpen[inst✝¹] U ∧ μ U < μ (A n) + δ n
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
⊢ ↑h • g • a = a

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
⊢ ↑h • g • a = a