mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ⨆ b, ∫⁻ (a : α), f b a ∂μ = ⨆ b, ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
congr 1
    ext1 b
    rw [lintegral_congr_ae]
    apply EventuallyEq.symm
    exact aeSeq.aeSeq_n_eq_fun_n_ae hf hp _

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
⊢ IsSeparable (range f)

Tactic:
have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
    .closure <| .iUnion fun n => (hf.approx n).finite_range.isSeparable

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure[inst✝] (⋃ n, range ⇑(hf.approx n)))
⊢ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : (μ.trim hm) s = μ s
⊢ c * (μ.trim hm) s = c * μ s

Tactic:
h_trim_s

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : (μ.trim hm) s = μ s
⊢ c * μ s = c * μ s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩
  rw [SimpleFunc.coe_smul]
  exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h✝ : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∉ V
⊢ y ∈ E ∩ D ∪ V ∩ C

Tactic:
· exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_

Goal state after:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ n ≥ N, dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
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
ε : ℝ
p : Z
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε

Tactic:
have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 := by
    have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
    refine le_antisymm ?_ (le_ciInf A)
    have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
    rw [this]
    exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p
  simp only [glueDist, this, zero_add]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : a ≤ b
δ : α
⊢ ↑(addNSMul h δ 0) = a

Tactic:
addNSMul,

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : a ≤ b
δ : α
⊢ ↑(projIcc a b h (a + 0 • δ)) = a
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ ↑(addNSMul h δ n) = b

Tactic:
addNSMul,

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ ↑(projIcc a b h (a + n • δ)) = b
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) →
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

pp: case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Tactic:
· rintro ⟨⟨δX, δX0, hX⟩, δY, δY0, hY⟩
    refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
    rintro (a | a) (b | b) h <;> simp only [lt_min_iff] at h
    · exact hX h.1.1
    · exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt
    · exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt
    · exact hY h.1.2

Goal state after:
case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)

Tactic:
grw [Sum.dist, ← le_add_of_nonneg_right dist_nonneg, ← le_add_of_nonneg_left dist_nonneg]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)

Tactic:
rw [Sum.dist_comm]; exact Sum.one_le_dist_inl_inr

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ t,
    t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
simp_rw [Subtype.ext_iff]

Goal state after:
ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ t,
    ↑(t 0) = ↑0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_4.refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
⊢ t ∈ 𝓝 x

Tactic:
rcases h x hx with ⟨ε, ε0, hε⟩
      simp only [dist_eq, one_div] at hε
      have : Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|)
          (𝓝 x) (𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) := by
        refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs
        refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
        rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
        exact x.2
      simp only [dist_self, sub_self, abs_zero, zero_add] at this
      exact mem_of_superset (this <| gt_mem_nhds ε0) hε

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

Goal state before:
pp: case refine_2
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = Sigma.dist ⟨j, y⟩ ⟨i, x⟩

Tactic:
rcases eq_or_ne i j with (rfl | h)

Goal state after:
case refine_2.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist ⟨i, x⟩ ⟨i, y⟩ = Sigma.dist ⟨i, y⟩ ⟨i, x⟩

case refine_2.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = Sigma.dist ⟨j, y⟩ ⟨i, x⟩
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this : PolishSpace ↑s
⊢ IsClopenable s

Tactic:
let t : Set α := sᶜ

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this : PolishSpace ↑s
t : Set α := sᶜ
⊢ IsClopenable s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : IsEmpty β
⊢ AnalyticSet ∅

Tactic:
exact analyticSet_empty

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen[inst✝¹] s
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
⊢ AnalyticSet (f '' s)

Tactic:
rw [image_eq_range]

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen[inst✝¹] s
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
⊢ AnalyticSet (range fun x ↦ f ↑x)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
exact Or.inr ⟨h⟩

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

Goal state before:
pp: 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
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y)

Tactic:
eq_comm,

Goal state after:
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
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ cylinder Ay.some (firstDiff x y) = cylinder y (firstDiff x y)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:

Tactic:
(∑' x : α, s.indicator (fun x => μ {x}) x) =
      Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
      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]
    _ = μ s := by rw [μ.sum_smul_dirac]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂dirac a = f a

Tactic:
simp [lintegral_congr_ae (ae_eq_dirac f)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
by
  induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp
  | basic s hs =>
    obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs
  | compl s hs ihs =>
    simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
    exact ihs.const_sub _
  | iUnion f hfd hfm ihf =>
    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ S.ncard = H.index

Tactic:
by
  rw [← Nat.card_coe_set_eq, h.card_left]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst✝¹] U), μ U
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r

Tactic:
simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using! hr

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
⊢ Tendsto (fun n ↦ 2 * u n) atTop (𝓝 0)

Tactic:
simpa only [mul_zero] using u_lim.const_mul 2

Goal state after:
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
⊢ g = ↑(hST.equiv g).2 ↔ g ∈ T

Tactic:
eq_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).2 = g ↔ g ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (Quotient (QuotientGroup.rightRel H)) ↔ H.FiniteIndex

Tactic:
(QuotientGroup.quotientRightRelEquivQuotientLeftRel H).finite_iff

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ c • s ∈ ae μ ↔ s ∈ ae μ

Tactic:
simp only [mem_ae_iff, ← smul_set_compl, measure_smul_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ r < μ (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
apply hr.trans_le

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ (μ.restrict A) s ≤ μ (toMeasurable μ (s ∩ A) ∩ s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
rw [image_eq_range]

Goal state after:
γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (range fun x ↦ f ↑x)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
⊢ (bind 0 fun x ↦ map (Prod.mk x) ν) = 0

Tactic:
exact bind_zero_left _

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
h : H
⊢ Measure.map ((fun x ↦ h * x) ∘ ⇑f) μ = Measure.map (⇑f) μ

Tactic:
obtain ⟨g, rfl⟩ := h_surj h

Goal state after:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
⊢ Measure.map ((fun x ↦ f g * x) ∘ ⇑f) μ = Measure.map (⇑f) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
← image_union

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t' ∪ t')
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (r • μ).withDensity f = r • μ.withDensity f

Tactic:
by
  ext s hs
  simp [withDensity_apply, hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t

Tactic:
rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
    withDensity_apply _ ht]

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)) Sᶜ = 0

Tactic:
rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.fun_neg.ennreal_ofReal, EventuallyEq]
    exact
      (ae_restrict_mem hS.compl).mono fun x hx =>
        ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
withDensity_apply _ (hm s hs)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∫⁻ (a : α) in toMeasurable (μ.withDensity f) s, f a ∂μ = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
lintegral_eq_zero_iff' (AEMeasurable.restrict hf),

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : f =ᵐ[μ.restrict (toMeasurable (μ.withDensity f) s)] 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0