mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ∞
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun r ↦ μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s))

Tactic:
convert! tendsto_measure_thickening hs
  exact h's.closure_eq.symm

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

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
      rintro _ ⟨s, hs, rfl⟩

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
⊢ MeasurableSet (Prod.fst ⁻¹' s)

case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sSup (range fun x ↦ f (x + k))))

Tactic:
sSup_range

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨆ x, f (x + k)))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x

Tactic:
filter_upwards [h_tendsto] with x hx using hx.comp hv

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
⊢ r * s x ≠ 0

Tactic:
rwa [Ne, ← ENNReal.coe_eq_zero]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral μ ≤
    ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
by exact le_iSup₂ (α := ℝ≥0∞) φ hle

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

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
by
  filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
by
  rcases hf with ⟨g, hg, hfg⟩
  obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite
  refine ⟨t, ht, ?_, htμ⟩
  refine EventuallyEq.trans (ae_restrict_of_ae hfg) ?_
  rw [EventuallyEq, ae_restrict_iff' ht.compl]
  exact Eventually.of_forall hgt_zero

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ

Tactic:
have rinv' : r⁻¹ * r = 1 := by
    rw [mul_comm]
    exact rinv

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
ht : ¬↑t = 1
this : 1 - ↑s * ↑t ≠ 0
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    ↑x * (1 - ↑s * ↑t - ↑s * (1 - ↑t)) + ↑s * (1 - ↑t) * ↑y + ↑s * ↑t * ↑z

Tactic:
ring_nf

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 y : X ⊕ Y
⊢ Sum.dist x y = Sum.dist y x

Tactic:
cases x <;> cases y <;> simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ ↑y * (↑z - ↑x) = ↑x * (↑z - ↑x - (↑y - ↑x)) + (↑y - ↑x) * ↑z

Tactic:
ring_nf

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)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] (cylinder x n)

Tactic:
PiNat.cylinder_eq_pi

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] ((↑(Finset.range n)).pi fun i ↦ {x i})
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ Continuous toNNReal

Tactic:
by delta toNNReal; fun_prop

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

Goal state before:
pp: case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder y (Nat.find A - 1)
⊢ (s ∩ cylinder x (Nat.find A - 1)).Nonempty

Tactic:
refine ⟨y, ys, ?_⟩

Goal state after:
case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder y (Nat.find A - 1)
⊢ y ∈ cylinder x (Nat.find A - 1)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
⊢ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ

Tactic:
by (rw [h]; exact zero_left)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ μ sᶜ = 1 ↔ μ s = 0

Tactic:
rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : α → Prop
f✝ : β → α
f : α → β
⊢ IsZeroOrProbabilityMeasure (Measure.map f μ)

Tactic:
by_cases hf : AEMeasurable f μ
  · simpa [isZeroOrProbabilityMeasure_iff, hf] using IsZeroOrProbabilityMeasure.measure_univ
  · simp [isZeroOrProbabilityMeasure_iff, hf]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ

Tactic:
rw [biUnion_of_singleton]

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

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
⊢ ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f

Tactic:
by
    apply exists_retraction_subtype_of_isClosed s_closed
    simpa only [nonempty_coe_sort] using g_surj.nonempty

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

Goal state before:
pp: case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
obtain ⟨t, ht, ts, mlt, t_top⟩ :
      ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
      Measure.exists_subset_measure_lt_top hs this

Goal state after:
case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ (map join μ).join = μ.join.join

Tactic:
change bind μ join = join (join μ)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
⊢ μ.bind join = μ.join.join
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 β
hs : MeasurableSet s
⊢ (map Prod.snd (μ.prod ν)) s = (μ univ • ν) s

Tactic:
simp [Measure.map_apply measurable_snd hs, ← univ_prod]

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 β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᵐ[ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν

Tactic:
refine ⟨Prod.mk x ⁻¹' u, measurable_prodMk_left hum, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᵐ[ν] Prod.mk x ⁻¹' u
⊢ t =ᵐ[ν] Prod.mk x ⁻¹' u
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:
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: G : Type u_1
inst✝ : Group G
S : Set G
⊢ IsComplement S univ ↔ ∃ g, S = {g}

Tactic:
by
  refine
    ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨?_, fun a ha b hb => ?_⟩, ?_⟩
  · obtain ⟨a, _⟩ := h.2 1
    exact ⟨a.1.1, a.1.2⟩
  · have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
      h.1 ((mul_inv_cancel a).trans (mul_inv_cancel b).symm)
    exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1
  · rintro ⟨g, rfl⟩
    exact isComplement_singleton_univ

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ μ.withDensity f ≪ μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs₁ hs₂ => ?_
  rw [withDensity_apply _ hs₁]
  exact setLIntegral_measure_zero _ _ hs₂

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⁻¹ = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
← image_inv_eq_inv,

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 * ν' ((fun x ↦ x⁻¹) '' A) = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * ((fun x ↦ x⁻¹) '' A).indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
⊢ (μ.restrict A).Regular

Tactic:
by
  have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A
  constructor
  intro V hV r hr
  have R : restrict μ A V ≠ ∞ := by
    rw [restrict_apply hV.measurableSet]
    exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne
  exact MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

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
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
wlog hs : MeasurableSet s generalizing s

Goal state after:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Tactic:
have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
  rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]

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

Goal state before:
pp: case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
s : Set α
h_ms : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

Tactic:
simp [*, mul_comm _ c, ← indicator_mul_right]

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

Goal state before:
pp: x : ℝ≥0
⊢ sqrt (x ^ 2) = x

Tactic:
sqrt_sq

Goal state after:
x : ℝ≥0
⊢ x = x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ y ↔ x ≤ y ^ 2

Tactic:
← Real.le_toNNReal_iff_coe_le hy,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ NNReal.sqrt x.toNNReal ≤ y.toNNReal ↔ x ≤ y ^ 2
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
this : Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)

Tactic:
by
    rwa [lintegral_zero] at this

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
⊢ f x ≠ 0 → f x ≠ ∞ → (f * fun x ↦ (f x)⁻¹) x = 1 x

Tactic:
hf_ne_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
⊢ f x ≠ ∞ → (f * fun x ↦ (f x)⁻¹) x = 1 x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ (fun x ↦ ‖x‖) ((fun n ↦ (starRingEnd ℂ) (↑f n)) j - (fun n ↦ (starRingEnd ℂ) (↑f n)) i) < ε

Tactic:
simp_rw [← map_sub, norm_conj]

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖↑f j - ↑f i‖ < ε
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ ↑q * a < q • b

Tactic:
Rat.smul_def

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ ↑q * a < ↑q * b
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
⊢ ker 0 = ⊤

Tactic:
ext
  simp [mem_ker]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ (ψ.comp f₁).comp (ι f₁ g₁) = (ψ.comp g₁).comp (ι f₁ g₁)

Tactic:
simp only [comp_assoc, comp_ι_eq f₁ g₁]

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re x) * ↑(RCLike.re y) - ↑(RCLike.im x) * ↑(RCLike.im y) +
      (↑(RCLike.re x) * ↑(RCLike.im y) + ↑(RCLike.im x) * ↑(RCLike.re y)) * I =
    (↑(RCLike.re x) + ↑(RCLike.im x) * I) * (↑(RCLike.re y) + ↑(RCLike.im y) * I)

Tactic:
ring_nf

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I -
      ↑(RCLike.im x) * ↑(RCLike.im y) =
    ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I +
      ↑(RCLike.im x) * ↑(RCLike.im y) * I ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ √(normSq z) = ‖z‖

Tactic:
normSq_eq_def',

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ √(‖z‖ ^ 2) = ‖z‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = re z / normSq z

Tactic:
normSq_eq_def',

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = re z / ‖z‖ ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = -im z / normSq z

Tactic:
normSq_eq_def',

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = -im z / ‖z‖ ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ 1 = -I ^ 2

Tactic:
linear_combination I_mul_I_of_nonzero h

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ * ‖z‖ = normSq z

Tactic:
normSq_eq_def',

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ * ‖z‖ = ‖z‖ ^ 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]

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

Goal state before:
pp: x a p : ℂ
n : ℕ
⊢ cexp (a * ↑n * x / p) = cexp (n • (a * x / p))

Tactic:
ring_nf

Goal state after: