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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
rsuffices ⟨g, hgm, hgle, hleg⟩ :
      ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ
  · exact ⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩
  -- Without loss of generality, `μ` is a finite measure.
  wlog h : IsFiniteMeasure μ generalizing μ
  · choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
    refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
    rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]
    exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)
  -- According to `exists_measurable_le_lintegral_eq`, for any natural `n`
  -- we can choose a measurable function $g_{n}$
  -- such that $g_{n}(x) ≤ \min (f(x), n)$ for all $x$
  -- and both sides have the same integral over the whole space w.r.t. $μ$.
  have (n : ℕ) : ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ g ≤ n ∧
      ∫⁻ a, min (f a) n ∂μ = ∫⁻ a, g a ∂μ := by
    simpa [and_assoc] using exists_measurable_le_lintegral_eq μ (f ⊓ n)
  choose g hgm hgf hgle hgint using this
  -- Let `φ` be the pointwise supremum of the functions $g_{n}$.
  -- Clearly, `φ` is a measurable function and `φ ≤ f`.
  set φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
  have hφm : Measurable φ := by fun_prop
  have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)
  refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩
  -- Now we show the inequality between set integrals.
  -- Choose a simple function `ψ ≤ f` with values in `ℝ≥0` and prove for `ψ`.
  rw [lintegral_eq_nnreal]
  refine iSup₂_le fun ψ hψ ↦ ?_
  -- Choose `n` such that `ψ x ≤ n` for all `x`.
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ x, ψ x ≤ n := by
    rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩
  calc
    (ψ.map (↑)).lintegral (μ.restrict s) = ∫⁻ a in s, ψ a ∂μ :=
      SimpleFunc.lintegral_eq_lintegral .. |>.symm
    _ ≤ ∫⁻ a in s, min (f a) n ∂μ :=
      lintegral_mono fun a ↦ le_min (hψ _) (ENNReal.coe_le_coe.2 (hn a))
    _ ≤ ∫⁻ a in s, g n a ∂μ := by
      have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)
    _ ≤ _ := lintegral_mono fun x ↦ le_iSup (g · x) n

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
⊢ c ≠ 0

Tactic:
intro hc

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
hc : c = 0
⊢ False
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s ≤ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp only [Measure.prod, ← map_apply measurable_prodMk_left hs]
  exact bind_apply_le _ hs

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : CocompactMap α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

Goal state after:
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 β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
x✝ : α
⊢ x✝ ∈ t' ↔ x✝ ∈ ⋃ c ∈ u, t ∩ g ⁻¹' {c}

Tactic:
simp [t']

Goal state after:
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 β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ g '' t' ⊆ u

Tactic:
simp [t']

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ ↑H.index * μ ↑H = μ univ

Tactic:
calc
    H.index * μ H = ∑' a : s, μ (a.val • H) := by simp [measure_smul, hs.encard_left]
    _ = μ univ := by
      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
      · simp [hs.mul_eq]
      · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

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✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
⊢ μ.inv.IsMulRightInvariant

Tactic:
by
  constructor
  intro g
  conv_rhs => rw [← map_mul_left_eq_self μ g⁻¹]
  simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
y : G
yins : y ∈ s
hy : f y = (fun x ↦ f g * x) x✝
⊢ f (g⁻¹ * y) = x✝

Tactic:
by simp [hy]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
y : G
yins : y ∈ s
hy : f y = (fun x ↦ x * f g) x✝
⊢ f (y * g⁻¹) = x✝

Tactic:
by simp [hy]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
· ext1 s hs
    rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs),
      Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ,
      univ_inter]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ

Tactic:
conv in f _ * (∫⁻ _, _ ∂μ) =>
    rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]

Goal state after:
G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : R1Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst✝³] K ∧ μ (A \ K) < ε

Tactic:
by
  rcases hA.exists_isCompact_isClosed_lt_add h'A hε with ⟨K, hKA, hKco, hKcl, hK⟩
  exact ⟨K, hKA, hKco, hKcl, measure_sdiff_lt_of_lt_add hKcl.nullMeasurableSet hKA
    (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩

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

Tactic:
rw [lintegral_indicator hA.inv] at h1

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEMeasurable (fun x ↦ ↑(f x) * g x) μ

Tactic:
by
  have t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f' := hf
  rcases t with ⟨f', hf'_m, hf'_ae⟩
  constructor
  · rintro ⟨g', g'meas, hg'⟩
    have A : MeasurableSet {x | f' x ≠ 0} := hf'_m (measurableSet_singleton _).compl
    refine ⟨fun x => f' x * g' x, hf'_m.coe_nnreal_ennreal.smul g'meas, ?_⟩
    apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
    · rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'
      rw [ae_restrict_iff' A]
      filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg
      have : (f' a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg
      rw [← h'a] at this ⊢
      rw [ha this]
    · rw [ae_restrict_iff' A.compl]
      filter_upwards [hf'_ae] with a ha ha_null
      have ha_null : f' a = 0 := Function.notMem_support.mp ha_null
      rw [ha_null] at ha ⊢
      rw [ha]
      simp only [ENNReal.coe_zero, zero_mul]
  · rintro ⟨g', g'meas, hg'⟩
    refine ⟨fun x => ((f' x)⁻¹ : ℝ≥0∞) * g' x, hf'_m.coe_nnreal_ennreal.inv.smul g'meas, ?_⟩
    rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]
    filter_upwards [hg', hf'_ae] with a hfga hff'a h'a
    rw [hff'a] at hfga h'a
    rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]

Goal state after:
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
⊢ b * b - 4 * a * c ≤ 0

Tactic:
obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0

Goal state after:
case inl
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
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0

case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0

case inr.inr
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
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

Tactic:
apply h_bound.mp ((ae_tendsto_enorm h_lim).mono _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ (x : α), Tendsto (fun n ↦ ‖F' n x‖ₑ) atTop (𝓝 ‖f' x‖ₑ) → (∀ (i : ℕ), ‖F' i x‖ₑ ≤ bound' x) → ‖f' x‖ₑ ≤ bound' x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

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

Goal state before:
pp: z : ℂ
⊢ |z.im| < ‖z‖ ↔ z.re ≠ 0

Tactic:
by
  simpa using @abs_re_lt_norm (z * I)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

Goal state after:
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))
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)

Tactic:
by
  have f_measurable : AEStronglyMeasurable f μ :=
    aestronglyMeasurable_of_tendsto_ae _ F_measurable h_lim
  let b a := 2 * ENNReal.ofReal (bound a)
  /- `‖F n a‖ ≤ bound a` and `F n a --> f a` implies `‖f a‖ ≤ bound a`, and thus by the
    triangle inequality, have `‖F n a - f a‖ ≤ 2 * (bound a)`. -/
  have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a := by
    intro n
    filter_upwards [all_ae_norm_ofReal_F_le_bound h_bound n,
      ae_norm_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
    calc
      ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]
  -- On the other hand, `F n a --> f a` implies that `‖F n a - f a‖ --> 0`
  have h : ∀ᵐ a ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0) := by
    rw [← ENNReal.ofReal_zero]
    refine h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp ?_
    rwa [← tendsto_iff_norm_sub_tendsto_zero]
  /- Therefore, by the dominated convergence theorem for nonnegative integration, have
    ` ∫ ‖f a - F n a‖ --> 0 ` -/
  suffices Tendsto (fun n => ∫⁻ a, ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ _ : α, 0 ∂μ)) by
    rwa [lintegral_zero] at this
  -- Using the dominated convergence theorem.
  refine tendsto_lintegral_of_dominated_convergence' _ ?_ hb ?_ ?_
  -- Show `fun a => ‖f a - F n a‖` is almost everywhere measurable for all `n`
  · exact fun n =>
      measurable_ofReal.comp_aemeasurable ((F_measurable n).sub f_measurable).norm.aemeasurable
  -- Show `2 * bound` `HasFiniteIntegral`
  · rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral
    · calc
        ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ := by
          rw [lintegral_const_mul']
          finiteness
        _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne
    filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h
  -- Show `‖f a - F n a‖ --> 0`
  · exact h

Goal state after:
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.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ ↑(normSq z) = (starRingEnd ℂ) z * z

Tactic:
ext <;> simp [normSq, mul_comm, ofReal]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
dsimp only [norm]
    simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
    rw [le_sup_iff]
    rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
⊢ ℑ.ker = selfAdjoint.submodule ℝ A

Tactic:
ext x
  simp [selfAdjoint.submodule, selfAdjoint.mem_iff, imaginaryPart, Subtype.ext_iff]
  grind

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ im a = 0

Tactic:
simpa only [mul_self_norm a, normSq_apply, left_eq_add, mul_self_eq_zero]
    using congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := K)

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
z : K
h : I = 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k

Tactic:
rw [tsub_eq_iff_eq_add_of_le ji] at hk

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =o[l] k₂
h₂ : f' =O[l] g'
⊢ (fun x ↦ k₁ x • f' x) =o[l] fun x ↦ k₂ x • g' x

Tactic:
simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
  exact ((h₁ (div_pos cpos c'pos)).smul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

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

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * ((↑(m.choose I))⁻¹ * ↑(m.choose I))))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
inv_mul_cancel₀ h₁

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h : x ≤ 0
⊢ 0 < rexp (- -x)

Tactic:
Real.exp_neg

Goal state after:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cosh ↑x).im = 0

Tactic:
rw [← ofReal_cosh_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cos x - (1 - x ^ 2 / 2)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖

Tactic:
simp [cos, field, Finset.sum_range_succ, Nat.factorial]

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (x * I) + cexp (-(x * I))) / 2 - (1 - x ^ 2 / 2)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + (x * I) ^ 2 / 2 + (-(x * I)) ^ 3 / 6)) / 2 +
        (cexp (x * I) - (1 + x * I + (x * I) ^ 2 / 2 + (x * I) ^ 3 / 6)) / 2‖