mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
· rcases hx with ⟨y, rfl⟩
    simpa only [SimpleFunc.extend_apply, hg.injective, Injective.extend_apply] using
      hf.tendsto_approx y

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x ↦ ∑' (n : α), f n x) s

Tactic:
by
  refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)
  intro t
  exact continuousOn_finsetSum _ fun i _ => hf i

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inl
x : ℝ
h₀ : x ≤ 0
⊢ ↑(σ (projIcc 0 1 ⋯ x)) = ↑(projIcc 0 1 ⋯ (1 - x))

pp: case inr
x : ℝ
h₀ : 0 ≤ x
⊢ ↑(σ (projIcc 0 1 ⋯ x)) = ↑(projIcc 0 1 ⋯ (1 - x))

Tactic:
· simp [projIcc_of_le_left, projIcc_of_right_le, h₀]

Goal state after:
case inr
x : ℝ
h₀ : 0 ≤ x
⊢ ↑(σ (projIcc 0 1 ⋯ x)) = ↑(projIcc 0 1 ⋯ (1 - x))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ i < σ j ↔ j < i

Tactic:
by
  simp only [symm, Subtype.mk_lt_mk, sub_lt_sub_iff_left, Subtype.coe_lt_coe]

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))

Tactic:
add_left_comm,

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ p, dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + dist y (Ψ p) + (ε + ε))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)

Tactic:
by
  by_cases h : (z - x : ℝ) = 0
  · simp_all
  · replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
    replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
    apply div_nonneg <;> grind

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

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist ⟨i, x⟩ ⟨j, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨j, z⟩

Tactic:
simp only [Sigma.dist_ne hij, Sigma.dist_same]

Goal state after:
case inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + dist y z
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
⊢ res ↑x = res ↑y

Tactic:
ext n : 1

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
⊢ res (↑x) n = res (↑y) n
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < ε → y ∈ s

Tactic:
refine ⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩

Goal state after:
case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < min ε 1 → y ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
leRecOn_succ xm,

Goal state after:
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (f m (leRecOn xm (fun {k} ↦ f k) x.snd)) (leRecOn hy (fun {k} ↦ f k) y.snd)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

Tactic:
l_eq,

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
l_eq : longestPrefix y s = longestPrefix x s
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix x s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
⊢ IsZeroOrProbabilityMeasure ((0 univ)⁻¹ • 0)

Tactic:
simp; infer_instance

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

Goal state before:
pp: case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ y ∈ range F

Tactic:
have xt : x ∈ t := by
        refine mem_iInter.2 fun n => ?_
        simp [γ, hx]

Goal state after:
case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ y ∈ range F
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ (μ1 {x}).toReal = μ2.real {x}
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ (μ1 {x}).toReal = μ2.real {x}

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ (μ1 {x}).toReal = (μ2 {x}).toReal
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 1 → 2
  | h => h.disjoint
  tfae_have 2 → 1
  | h => mutuallySingular_of_disjoint h
  tfae_have 1 → 3
  | h => h.disjoint_ae
  tfae_have 3 → 2
  | h => disjoint_of_disjoint_ae h
  tfae_finish

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (fun x ↦ μ {x}) x = (sum fun a ↦ μ {a} • dirac a) s

Tactic:
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ count.real {a} = 1

Tactic:
measureReal_def,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ (count {a}).toReal = 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.refine_2
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C

Tactic:
intro y hy
    replace hy : dist y (denseSeq X n) < ε / 2 := by
      simpa [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, not_lt_of_ge, ε, div_le_iff₀] using hy
    have : dist x y < infDist x (closure Cᶜ) :=
      ((dist_triangle_right x y (denseSeq X n)).trans_lt (add_lt_add hn hy)).trans_le (by simp [ε])
    simpa using notMem_of_notMem_closure (mt infDist_le_dist_of_mem this.not_ge)

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
filter_upwards [Classical.choose_spec
      (exists_eventually_forall_measure_closedBall_le_mul μ K)] with r hr x
  grw [hr x K le_rfl, scalingConstantOf, ← le_max_left]

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 ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
set s' : Set α := { x | ν t ≤ f x }

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x | ν t ≤ f x}
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ 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
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s ↦ (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
exact ⟨(x, ⟨_, hx⟩), by simp, by aesop⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

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

Tactic:
rw [equiv_snd_eq_inv_mul, mul_assoc]

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

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

Tactic:
rw [H₁]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
⊢ μ (A n ∩ s n) ≠ ∞
Module: Mathlib.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
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
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
fsnv : f '' ↑(s n) ⊆ v
⊢ False

Tactic:
have : x ∈ closure v := closure_mono fsnv (hxs n).1

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 γ
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
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
fsnv : f '' ↑(s n) ⊆ v
this : x ∈ closure[inst✝³] v
⊢ False
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
x : α
y : β
⊢ (dirac x).prod (dirac y) = dirac (x, y)

Tactic:
by
  rw [prod_dirac, map_dirac' measurable_prodMk_right]

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 γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc (Prod.mk a ⁻¹' (fun p ↦ (f p.1, g p.1 p.2)) ⁻¹' s) = μd (Prod.mk (f a) ⁻¹' s)

Tactic:
rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]

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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y ↦ f (x, y)) ν τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
by
  refine ⟨hf, ?_⟩
  refine AbsolutelyContinuous.mk fun s hs h2s => ?_
  rw [map_apply hf hs, Measure.prod_apply (hf hs)]; simp_rw [preimage_preimage]
  rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]

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✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
⊢ (map (fun x ↦ a • x) μ) K < ∞

Tactic:
by
    let F := (Homeomorph.smul a (α := G)).toMeasurableEquiv
    change map F μ K < ∞
    rw [F.map_apply K]
    exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
μ : Measure β
inst✝ : μ.Regular
f : α → β
hf : IsOpenEmbedding f
⊢ (comap f μ).Regular

Tactic:
have := OuterRegular.comap' μ hf.continuous hf.measurableEmbedding

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
μ : Measure β
inst✝ : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this : (comap f μ).OuterRegular
⊢ (comap f μ).Regular
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
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c ≤ 0

Tactic:
rw [discrim, sq]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ≠ 0 ↔ 0 < x

Tactic:
rw [← not_le, not_iff_not, sqrt_eq_zero']

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

Goal state before:
pp: x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < y ^ 2

Tactic:
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq ((starRingEnd ℂ) w) + 2 * (z * (starRingEnd ℂ) w).re ≤
    normSq z + normSq ((starRingEnd ℂ) w) + 2 * √(normSq z * normSq ((starRingEnd ℂ) w))

Tactic:
← map_mul

Goal state after:
z w : ℂ
⊢ normSq z + normSq ((starRingEnd ℂ) w) + 2 * (z * (starRingEnd ℂ) w).re ≤
    normSq z + normSq ((starRingEnd ℂ) w) + 2 * √(normSq (z * (starRingEnd ℂ) w))
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
simp_rw [_root_.abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]

Goal state after: