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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
⊢ ∃ K', ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑K' * edist x y

Tactic:
refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ edist (f x) (f y) ≤ ↑(NNReal.mk (max K' 0) ⋯) * edist x y
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ ↑(K ↑z ⋯) * edist x y + ↑(K' ↑z ⋯) * (edist x y + edist x y) = ↑(K ↑z ⋯ + 2 * K' ↑z ⋯) * edist x y

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ ↑(K ↑z ⋯) * edist x y + ↑(K' ↑z ⋯) * (edist x y + edist x y) = (↑(K ↑z ⋯) + 2 * ↑(K' ↑z ⋯)) * edist x y
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
hy : y ∈ Metric.ball x 1
⊢ y ∈ {x}

Tactic:
simp only [Metric.mem_ball, mem_singleton_iff] at *

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
hy : dist y x < 1
⊢ y = x
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α

Tactic:
exact f.symm.polishSpace_induced

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0

Tactic:
exact glueDist_glued_points Φ Ψ 0 _

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
⊢ ε > 0 → ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Tactic:
ε_pos

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
⊢ map f (c • μa) = c • μb

Tactic:
Measure.map_smul,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
⊢ c • map f μa = c • μb
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

Tactic:
by
  rcases eq_zero_or_isProbabilityMeasure μ with h | h <;> simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋂ n, t n)ᶜ ≤ 2 * ↑ε

Tactic:
· rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
      2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]
    refine (measure_iUnion_le _).trans ?_
    exact ENNReal.summable.tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ s = ∅ → count s = 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ count ∅ = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
⊢ dirac x ≠ dirac y

Tactic:
obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y
  exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ (∀ᵐ (b : β) ∂μ, f b ∈ s) ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a

Tactic:
rw [← ae_map_iff hf (by measurability), ae_mem_finset_iff]

Goal state after:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ map f μ = ∑ a ∈ s, (map f μ) {a} • dirac a ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case e_f
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun i ↦ ∫⁻ (a : α), f a ∂dirac i) = fun a ↦ f a

Tactic:
exact funext fun a => lintegral_dirac' a hf

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

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

Tactic:
← lintegral_count

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (sum m).join s = ∑' (i : ι), (m i).join s

Tactic:
join_apply hs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure α), μ s ∂sum m = ∑' (i : ι), ∫⁻ (μ : Measure α), μ s ∂m i
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rcases hf with ⟨g, hgm, hfg⟩
    rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]
    exact lintegral_congr_ae <| (ae_ae_of_ae_join hfg).mono fun μ hμ ↦
      .symm <| lintegral_congr_ae hμ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (map f m).join s = ∫⁻ (a : α), (f a) s ∂m

Tactic:
join_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ ∫⁻ (μ : Measure β), μ s ∂map f m = ∫⁻ (a : α), (f a) s ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (map f (c • m)).join = c • (map f m).join

Tactic:
Measure.map_smul,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • map f m).join = c • (map f m).join
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ (map (map f) μ).join s = (map f μ.join) s

Tactic:
join_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), μ s ∂map (map f) μ = (map f μ.join) s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ f x ∈ u ∧ g y ∈ v ∧ Disjoint u v

Tactic:
apply t2_separation

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := ⋯
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⋯
p : ℕ → A := ⋯
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := ⋯
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := ⋯
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
⊢ f x ≠ g y
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:
simp_rw [Measure.sum_apply _ (M _)]

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 : α), ∑' (i : ι'), (m' i) (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
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:
by
  classical
  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.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ μ U < ∞ ∧ μ (U \ A) < ε

Tactic:
rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen[inst✝¹] U
hU : μ U < μ A + ε
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ μ U < ∞ ∧ μ (U \ A) < ε
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 > (map (⇑f) μ) A
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (map (⇑f) μ) U < r

Tactic:
map_apply f.measurable hA,

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 ⁻¹' A)
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (map (⇑f) μ) U < r
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 μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet s μ

Tactic:
by
  refine .right_of_prod ?_ ht
  rw [← preimage_swap_prod]
  exact h.preimage measurePreserving_swap.quasiMeasurePreserving

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ g * x) (c • μ) = c • μ

Tactic:
Measure.map_smul,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ c • Measure.map (fun x ↦ g * x) μ = c • μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ x * g) (c • μ) = c • μ

Tactic:
Measure.map_smul,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ c • Measure.map (fun x ↦ x * g) μ = c • μ
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 ν
ρ : Measure (α × β)
inst✝ : SFinite ρ
⊢ SFinite ρ.fst

Tactic:
by
  rw [fst]
  infer_instance

Goal state after:
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 ν
ρ : Measure (α × β)
inst✝ : IsFiniteMeasure ρ
⊢ IsFiniteMeasure ρ.fst

Tactic:
by
  rw [fst]
  infer_instance

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
a : ι
s : Finset ι
ha : a ∉ s
ih : (∑ i ∈ s, μ i).InnerRegular
⊢ (∑ i ∈ insert a s, μ i).InnerRegular

Tactic:
| insert a s ha ih =>

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
⊢ μ (s * closure[inst✝³] {1}) ≤ μ s

Tactic:
conv_rhs => rw [measure_eq_iInf]

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
⊢ μ (s * closure[inst✝³] {1}) ≤ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case e'_2
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : ContinuousMul G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h ↦ g⁻¹ * h) ⁻¹' {1}

Tactic:
simp only [mul_one, preimage_mul_left_singleton, inv_inv]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 ∂ν' = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
setLIntegral_one,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
← lintegral_indicator hA,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ ∫⁻ (a : G), A.indicator (fun x ↦ ν' ((fun y ↦ y * x) ⁻¹' s)) a ∂μ' ≠ ∞
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0

Tactic:
rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Tactic:
rintro rfl

Goal state after:
case mp
x : ℝ
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0