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

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ {i} • dirac i, x ∈ s

Tactic:
;

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ {i} • dirac i, x ∈ s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ ↦ μ s) ∘ f) mβ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ ↦ μ s) ∘ f) mβ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ AEMeasurable (fun a ↦ a (f i)) m

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ AEMeasurable (fun a ↦ a (f i)) m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ b.join s

Tactic:
by
    simp only [join_apply hs, measurable_lintegral (measurable_coe hs)]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) ≤ ∑' (i : ?m.10), 2⁻¹ ^ encode i

Tactic:
;

Goal state after:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) ≤ ∑' (i : ?m.10), 2⁻¹ ^ encode i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
⊢ min (2⁻¹ ^ encode i) (edist (x i) (y i)) ≤ 2⁻¹ ^ encode i

Tactic:
;

Goal state after:
case h
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
⊢ min (2⁻¹ ^ encode i) (edist (x i) (y i)) ≤ 2⁻¹ ^ encode i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
x y z : (i : ι) → F i
n : ι
⊢ min (2⁻¹ ^ encode n) (edist (x n) (z n)) ≤
    min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n))

Tactic:
;

Goal state after:
case h
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
x y z : (i : ι) → F i
n : ι
⊢ min (2⁻¹ ^ encode n) (edist (x n) (z n)) ≤
    min (2⁻¹ ^ encode n) (edist (x n) (y n)) + min (2⁻¹ ^ encode n) (edist (y n) (z n))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h₁
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ ∑ _i ∈ K, δ ≤ ε / 2

Tactic:
;

Goal state after:
case h₁
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ ∑ _i ∈ K, δ ≤ ε / 2
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ 0 ≤ ∑' (i : ι), min (2⁻¹ ^ encode i) (dist (x i) (y i))

Tactic:
;

Goal state after:
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ 0 ≤ ∑' (i : ι), min (2⁻¹ ^ encode i) (dist (x i) (y i))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) =
    ENNReal.ofReal (∑' (i : ι), min (2⁻¹ ^ encode i) (dist (x i) (y i)))

Tactic:
ENNReal.ofReal_tsum_of_nonneg (fun _ ↦ by positivity) (dist_summable ..)

Goal state after:
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) =
    ∑' (n : ι), ENNReal.ofReal (min (2⁻¹ ^ encode n) (dist (x n) (y n)))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case toPiNat
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
y : PiNatEmbed X Y f
ofPiNat✝ : X
hxy : { ofPiNat := ofPiNat✝ }.ofPiNat = y.ofPiNat
⊢ { ofPiNat := ofPiNat✝ } = y

Tactic:
;

Goal state after:
case toPiNat
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
y : PiNatEmbed X Y f
ofPiNat✝ : X
hxy : { ofPiNat := ofPiNat✝ }.ofPiNat = y.ofPiNat
⊢ { ofPiNat := ofPiNat✝ } = y
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₁s : IsSigmaCompact s
h₂s : μ s = 0
⊢ IsMeagre s

Tactic:
rcases h₁s with ⟨K, hcompact, hcover⟩
  have h (n : ℕ) : IsNowhereDense (K n) := by
    have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
    exact .of_isClosed_null (hcompact n).isClosed this
  rw [isMeagre_iff_countable_union_isNowhereDense]
  exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (Prod.mk b) ν) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (Prod.mk b) ν) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν
x : α
| ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν
x : α
| ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone f →
    (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
      Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
h2f

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
⊢ (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
    Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν
this : ∀ (x : α), Monotone fun n y ↦ f n (x, y)
x : α
| ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν
this : ∀ (x : α), Monotone fun n y ↦ f n (x, y)
x : α
| ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
x✝ : M × M
⊢ (⇑L ∘ fun p ↦ p.1 * p.2) x✝ = ((fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L) x✝

Tactic:
;

Goal state after:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
x✝ : M × M
⊢ (⇑L ∘ fun p ↦ p.1 * p.2) x✝ = ((fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L) x✝
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

Tactic:
;

Goal state after:
case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet s

Tactic:
← image_preimage_eq s hsurj

Goal state after:
case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
;

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : T = ∅
⊢ ¬IsComplement S T
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U

Tactic:
;

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
⊢ ∃ K ⊆ U, p K ∧ r < μ K
Module: Mathlib.GroupTheory.Complement

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (g₂ * (↑(hSK.equiv g₂).2)⁻¹)⁻¹ * g₁ * (g₁⁻¹ * g₂) ∈ K
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₂).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.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.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.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: 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
h : ↥H
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ h • ↑h' • g • a = g • a

Tactic:
← mul_smul,

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
h : ↥H
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ h • (↑h' * g) • a = g • a
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 μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s = 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

Tactic:
;

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s = 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

case inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
ht : ν t = 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
ht : ν t ≠ 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
ht : ν t = 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0

case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
hs : μ s ≠ 0
ht : ν t ≠ 0
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0