mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:

Tactic:
μ s * ν t ≤ μ s' * ν t := by gcongr
    _ = ∫⁻ _ in s', ν t ∂μ := by rw [setLIntegral_const, mul_comm]
    _ ≤ ∫⁻ x in s', f x ∂μ := setLIntegral_mono hfm fun x => id
    _ ≤ ∫⁻ x, f x ∂μ := lintegral_mono' restrict_le_self le_rfl
    _ = μ.prod ν ST := (prod_apply hSTm).symm
    _ = μ.prod ν (s ×ˢ t) := measure_toMeasurable _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.snd (μ.prod ν) ν

Tactic:
by
  refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply measurable_snd hs, ← univ_prod, ← nonpos_iff_eq_zero]
  refine (prod_prod_le _ _).trans_eq ?_
  rw [h2s, mul_zero]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝ : SFinite ν✝
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
⊢ ⋃ i, hμ.set (Nat.unpair i).1 ×ˢ hν.set (Nat.unpair i).2 = univ

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝ : SFinite ν✝
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
⊢ ⋃ i, hμ.set (Nat.unpair i).1 ×ˢ hν.set (Nat.unpair i).2 = univ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι' : Type u_4
inst✝¹ : Countable ι'
m : Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), (sum m') (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι' : Type u_4
inst✝¹ : Countable ι'
m : Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), (sum m') (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum m).prod (sum m') = sum fun p ↦ (m p.1).prod (m' p.2)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum m).prod (sum m') = sum fun p ↦ (m p.1).prod (m' p.2)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
this : μ.prod ν = sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (μ.prod ν)

Tactic:
this

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
this : μ.prod ν = sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))
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
this : range f = ⋂ n, F n
E_meas : ∀ (s : ↑b), MeasurableSet (E s)
F_meas : ∀ (n : ℕ), MeasurableSet (F n)
⊢ MeasurableSet (range f)

Tactic:
this

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
this : range f = ⋂ n, F n
E_meas : ∀ (s : ↑b), MeasurableSet (E s)
F_meas : ∀ (n : ℕ), MeasurableSet (F n)
⊢ MeasurableSet (⋂ n, F n)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h✝ : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ tᶜ = ν tᶜ

Tactic:
[

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h✝ : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ tᶜ = ν tᶜ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
[

Goal state after:
case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ S, IsComplement S ↑H ∧ g ∈ S

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
    QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
  by_cases hq : q = Quotient.mk'' g
  · exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
  · simp [Function.update, dif_neg hq, q.out_eq']

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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ μ univ = ν univ

Tactic:
[

Goal state after:
α : 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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ μ univ = ν univ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
this

Goal state after:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Tactic:
this

Goal state after:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, ↑(map H.subtype H'') * S = ↑H ∧ Nat.card ↥(map H.subtype H'') * Nat.card ↑S = Nat.card ↥H
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 * ↑k)).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

Tactic:
this

Goal state after:
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
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 * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Tactic:
rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]

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 (↑h * g)).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Tactic:
this

Goal state after:
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
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_4
α : 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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ tᶜ = ν tᶜ

Tactic:
[

Goal state after:
case refine_4
α : 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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ tᶜ = ν tᶜ
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
⊢ S.encard = ↑H.index

Tactic:
by
  rw [← h.finite_left.cast_ncard_eq, h.ncard_left]

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

Goal state before:
pp: case refine_5
α : 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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
[

Goal state after:
case refine_5
α : 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 γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
γ : 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)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
⊢ x ∈ range f

Tactic:
have : Nonempty γ := ⟨y 0⟩

Goal state after:
case h₂
γ : 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)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
⊢ x ∈ range f
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ ((fun x ↦ c • x) ⁻¹' toMeasurable μ s)

Tactic:
exact measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

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)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
⊢ ∃ δ > 0, ball z δ ⊆ f ⁻¹' v

Tactic:
by
      apply Metric.mem_nhds_iff.1
      exact f_cont.continuousAt.preimage_mem_nhds (v_open.mem_nhds fzv)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun p ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) =
    sum fun p ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < μ F
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K

Tactic:
this

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ m • f x) ⁻¹' S) = μ ((fun x ↦ f (m • x)) ⁻¹' S)

Tactic:
[

Goal state after:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ m • f x) ⁻¹' S) = μ ((fun x ↦ f (m • x)) ⁻¹' S)