mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case refine_2
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
⊢ LipschitzWith 1 f

Tactic:
refine LipschitzWith.mk_one fun x y => ?_

Goal state after:
case refine_2
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
⊢ μ ≪ ν₁

Tactic:
by
  refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
  let t := h_ms.nullSet
  have ht : MeasurableSet t := h_ms.measurableSet_nullSet
  have htμ : μ t = 0 := h_ms.measure_nullSet
  have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet
  have : μ s = μ (s ∩ tᶜ) := by
    conv_lhs => rw [← inter_union_compl s t]
    rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
    · exact (disjoint_compl_right.inter_right' _).inter_left' _
    · exact hs.inter ht.compl
  rw [this]
  refine h ?_
  simp only [Measure.coe_add, Pi.add_apply, add_eq_zero]
  exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
h : μ univ = 0
⊢ μ univ ≤ 1

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
h : μ univ = 1
⊢ μ univ ≤ 1

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
h : μ univ = 0
⊢ μ univ ≤ 1

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
h : μ univ = 1
⊢ μ univ ≤ 1
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ ¬μ univ = 0

Tactic:
simp [measure_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : p
⊢ IsProbabilityMeasure (μ h✝)

pp: case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : ¬p
⊢ IsProbabilityMeasure (ν h✝)

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : p
⊢ IsProbabilityMeasure (μ h✝)

case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : ¬p
⊢ IsProbabilityMeasure (ν h✝)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : p
⊢ IsProbabilityMeasure μ

pp: case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : ¬p
⊢ IsProbabilityMeasure ν

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : p
⊢ IsProbabilityMeasure μ

case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : ¬p
⊢ IsProbabilityMeasure ν
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ = 0
⊢ (μ univ)⁻¹ • μ = μ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ (μ univ)⁻¹ • μ = μ

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ = 0
⊢ (μ univ)⁻¹ • μ = μ

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ (μ univ)⁻¹ • μ = μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = (sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x) (measurableAtom x)

Tactic:
sum_apply _ (MeasurableSet.measurableAtom_of_countable x)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = ∑' (i : ↑(range points)), (μ (measurableAtom ↑i) • dirac ↑i) (measurableAtom x)
Module: Mathlib.SetTheory.Cardinal.ENNReal

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

pp: case inr
α : Type u_1
h✝ : Infinite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

case inr
α : Type u_1
h✝ : Infinite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∉ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∈ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
h✝ : a ∉ s
⊢ s ∈ ae (dirac a) ↔ a ∈ s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ a ∈ s

pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ MeasurableSet {x | x ∈ s}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ a ∈ s

case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ MeasurableSet {x | x ∈ s}
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∈ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t

pp: case neg
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∉ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t

Tactic:
<;>

Goal state after:
case pos
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∈ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t

case neg
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∉ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case e'_1.e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
x✝ : α
⊢ x✝ = a₁ ∨ x✝ = a₂ ↔ x✝ ∈ Finset.cons a₁ {a₂} ⋯

pp: case e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ μ {a₁} • dirac a₁ + μ {a₂} • dirac a₂ = ∑ a ∈ Finset.cons a₁ {a₂} ⋯, μ {a} • dirac a

Tactic:
<;>

Goal state after:
case e'_1.e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
x✝ : α
⊢ x✝ = a₁ ∨ x✝ = a₂ ↔ x✝ ∈ Finset.cons a₁ {a₂} ⋯

case e'_2
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ μ {a₁} • dirac a₁ + μ {a₂} • dirac a₂ = ∑ a ∈ Finset.cons a₁ {a₂} ⋯, μ {a} • dirac a
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case e'_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
x✝ : β
⊢ f x✝ = a₁ ∨ f x✝ = a₂ ↔ f x✝ ∈ Finset.cons a₁ {a₂} ⋯

pp: case e'_2
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
⊢ μ (f ⁻¹' {a₁}) • dirac a₁ + μ (f ⁻¹' {a₂}) • dirac a₂ = ∑ a ∈ Finset.cons a₁ {a₂} ⋯, μ (f ⁻¹' {a}) • dirac a

Tactic:
<;>

Goal state after:
case e'_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
x✝ : β
⊢ f x✝ = a₁ ∨ f x✝ = a₂ ↔ f x✝ ∈ Finset.cons a₁ {a₂} ⋯

case e'_2
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
⊢ μ (f ⁻¹' {a₁}) • dirac a₁ + μ (f ⁻¹' {a₂}) • dirac a₂ = ∑ a ∈ Finset.cons a₁ {a₂} ⋯, μ (f ⁻¹' {a}) • dirac a
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
⊢ Measurable μ

Tactic:
rw [measurable_measure]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
⊢ ∀ (s : Set β), MeasurableSet s → Measurable fun b ↦ (μ b) s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ count {i | ε ≤ a i} ≤ ↑c / ↑ε

Tactic:
rw [show (fun i => ε ≤ a i) = fun i => (ε : ℝ≥0∞) ≤ ((↑) ∘ a) i by
      simp only [ENNReal.coe_le_coe, Function.comp]]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ count {i | ↑ε ≤ (ofNNReal ∘ a) i} ≤ ↑c / ↑ε
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (m.bind fun x ↦ dirac (f x)) = map f m

Tactic:
by
  rw [← bind_dirac (m := m.map f), bind, bind, map_map, Function.comp_def]
  exacts [measurable_dirac, hf]

Goal state after:
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 ≤ dist x y

Tactic:
rw [dist_eq_tsum]

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: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ofPiNat

Tactic:
refine continuous_iff_continuousAt.mpr fun x s hs ↦ ?_

Goal state after:
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : PiNatEmbed X (fun x ↦ ↑I) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 x.ofPiNat
⊢ s ∈ map ofPiNat (𝓝 x)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs

Goal state after:
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x ↦ x.1 * x.2) ((dirac x).prod μ) = map (fun y ↦ x * y) μ

Tactic:
dirac_prod,

Goal state after:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x ↦ x.1 * x.2) (map (Prod.mk x) μ) = map (fun y ↦ x * y) μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : 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∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

pp: case refine_3
α : 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 : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (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:
· rintro f g - hf - h2f h2g
    simp only [Pi.add_apply]
    conv => enter [1, x]; erw [lintegral_add_left (hf.comp m)]
    exact h2f.add h2g

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∞⦄,
    (∀ (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) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ s ⊆ S

pp: case ht
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ t ⊆ T

Tactic:
<;>

Goal state after:
case hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ s ⊆ S

case ht
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ t ⊆ T
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
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
by
  have d := hf.mono le_rfl OpensMeasurableSpace.borel_le
  let := borel Y; have : BorelSpace Y := ⟨rfl⟩
  exact d.map_measurableSpace_eq hsurj

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! s, (↑s)⁻¹ * g ∈ T) → ∃! x, ↑x.1 * ↑x.2 = g

pp: case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! x, ↑x.1 * ↑x.2 = g) → ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
<;>

Goal state after:
case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! s, (↑s)⁻¹ * g ∈ T) → ∃! x, ↑x.1 * ↑x.2 = g

case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! x, ↑x.1 * ↑x.2 = g) → ∃! s, (↑s)⁻¹ * g ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! t, g * (↑t)⁻¹ ∈ S) → ∃! x, ↑x.1 * ↑x.2 = g

pp: case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! x, ↑x.1 * ↑x.2 = g) → ∃! t, g * (↑t)⁻¹ ∈ S

Tactic:
<;>

Goal state after:
case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! t, g * (↑t)⁻¹ ∈ S) → ∃! x, ↑x.1 * ↑x.2 = g

case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! x, ↑x.1 * ↑x.2 = g) → ∃! t, g * (↑t)⁻¹ ∈ S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_1
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 : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

pp: case refine_2.refine_2
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 : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↑↑H''

Tactic:
<;>

Goal state after:
case refine_2.refine_1
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 : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

case refine_2.refine_2
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 : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↑↑H''
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_1
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 : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↥H''

pp: case refine_2.refine_2
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 : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

Tactic:
<;>

Goal state after:
case refine_2.refine_1
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 : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↥H''

case refine_2.refine_2
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 : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ ↑H

Tactic:
obtain ⟨t, ht1, ht2⟩ := isComplement_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)

Goal state after:
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s ↦ (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
⊢ ∃! s, (↑s)⁻¹ * g ∈ ↑H