mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (c : (ℕ × ℕ) × ℕ),
      ((sfiniteSeq μ ((Equiv.prodAssoc ℕ ℕ ℕ) c).1).prod
          ((sfiniteSeq ν ((Equiv.prodAssoc ℕ ℕ ℕ) c).2.1).prod (sfiniteSeq τ ((Equiv.prodAssoc ℕ ℕ ℕ) c).2.2)))
        s =
    ∑' (i : (ℕ × ℕ) × ℕ), ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))) s

Tactic:
simp only [Equiv.prodAssoc_apply]

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
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 < δ
a : γ
ha : a ∈ ↑(s n)
⊢ dist a (y n) + dist (y n) z ≤ u n + dist (y n) z

Tactic:
dist_le_diam_of_mem (hs n).1 ha (hy n),

Goal state after:
γ : 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 < δ
a : γ
ha : a ∈ ↑(s n)
⊢ diam ↑(s n) + dist (y n) z ≤ u n + dist (y n) z
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : DivInvMonoid G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun x ↦ x / g) μ = μ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : DivInvMonoid G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun x ↦ x * g⁻¹) μ = μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x ↦ x / g) μ μ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x ↦ x * g⁻¹) μ μ
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
⊢ μ (⋃ i, ↑i • ↑H) = μ univ

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
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)

Tactic:
· simp [hs.mul_eq]

Goal state after:
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
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ

Tactic:
obtain ⟨g, hg, hfg⟩ := hf
  refine ⟨fun x ↦ ∫⁻ y, g (x, y) ∂ν, by fun_prop, ?_⟩
  exact (ae_ae_of_ae_prod hfg).mono fun x hfg' ↦ lintegral_congr_ae hfg'

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

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet
    {x | ∃ i, True ∧ ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}

Tactic:
simp_rw [Set.ofPred_exists, true_and]

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet (⋃ i, {x | ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}})
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
by
  rw [lintegral_prod _ (by fun_prop)]
  simp [lintegral_lintegral_mul hf hg]

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 α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ

Tactic:
ext1 s hs
    rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs),
      Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ,
      inter_univ]

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : BorelSpace G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

Tactic:
lintegral_eq_zero_iff hf.measurable,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : BorelSpace G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
⊢ f =ᵐ[μ] 0 ↔ f = 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
⊢ IsClosed[inst✝⁷] (L n)

Tactic:
induction n with
    | zero => exact Kclosed
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))

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

Tactic:
let b a := 2 * ENNReal.ofReal (bound a)

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

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

Tactic:
have hy := x.sqrt_nonneg.trans_lt h

Goal state after:
x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < y ^ 2
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ (f x)⁻¹ * i x ≤ g x

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

Tactic:
by
  rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]

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

Goal state before:
pp: ⊢ ↑0⁻¹ = ↑0

Tactic:
inv_zero

Goal state after:
⊢ ↑0 = ↑0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (a : α × β), ((fun z ↦ f z.1) * φ) a ∂μ.prod ν

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
lintegral_prod

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp +contextual [expect, sum_eq_zero_iff_of_nonneg hf]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (a : α × β), ((fun z ↦ g z.2) * φ) a ∂μ.prod ν

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

Tactic:
lintegral_prod

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν ∂μ

case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ g z.2) * φ) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x * x‖ = ‖x‖ ^ 2

Tactic:
simpa [sq, hx.star_eq] using CStarRing.norm_star_mul_self (x := x)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑r * ↑(re z) - ↑r * ↑(im z) * I = ↑r * (↑(re z) - ↑(im z) * I)

Tactic:
mul_sub,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑r * ↑(re z) - ↑r * ↑(im z) * I = ↑r * ↑(re z) - ↑r * (↑(im z) * I)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = I * (z - (starRingEnd K) z) / 2

Tactic:
mul_sub,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = (I * z - I * (starRingEnd K) z) / 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ I⁻¹ = -I

Tactic:
by
  by_cases h : (I : K) = 0
  · simp [h]
  · field_simp
    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 / I = -(z * I)

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z * I⁻¹ = -(z * I)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
obtain ⟨c₁, hc₁⟩ := h₁.isBigOWith

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
c₁ : ℝ
hc₁ : IsBigOWith c₁ l f₁ g₁
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case cons
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ (fun H ↦ ∑ i ∈ Finset.cons i s his, A i H) =o[l] fun H ↦ ∑ i ∈ Finset.cons i s his, ‖B i H‖

Tactic:
| cons i s his h =>

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
⊢ ∀ᶠ (x : α) in l, ‖∑ j ∈ i x, A j x‖ ≤ C * ‖∑ j ∈ i x, ‖B j x‖‖

Tactic:
obtain ⟨s₁, hs₁, s₂, hs₂, hbound⟩ := Filter.eventually_prod_iff.mp hAB

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
⊢ ∀ᶠ (x : α) in l, ‖∑ j ∈ i x, A j x‖ ≤ C * ‖∑ j ∈ i x, ‖B j x‖‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
⊢ ∀ᶠ (x : α) in l, ‖∑ j ∈ i x, A j x‖ ≤ C * ‖∑ j ∈ i x, ‖B j x‖‖

Tactic:
filter_upwards [hs₂] with H hH

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ‖∑ j ∈ i H, A j H‖ ≤ C * ‖∑ j ∈ i H, ‖B j H‖‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (∑ m_1 ∈ range (m + 1), x ^ m_1 * y ^ (m - m_1) * ↑(m.choose m_1)) / ↑m.factorial =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
div_eq_mul_inv,

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (∑ m_1 ∈ range (m + 1), x ^ m_1 * y ^ (m - m_1) * ↑(m.choose m_1)) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by rw [← ofReal_tanh_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℂ
⊢ 2 * (cosh x - sinh x) = 2 * cexp (-x)

Tactic:
mul_sub,

Goal state after:
x : ℂ
⊢ 2 * cosh x - 2 * sinh x = 2 * cexp (-x)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ IsBigOWith C l f g

Tactic:
simp only [IsBigOWith]
  apply (((continuous_norm.tendsto _).comp h).eventually_const_le ha).mono
  intro x hx
  simp only [Function.comp_apply, norm_div] at hx
  by_cases hf : f x = 0
  · simp [hf] at hx
    linarith
  rw [le_div_iff₀ (by positivity)] at hx
  field_simp at hx
  exact hx

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ * (1 - c) ≤ ‖f₂ x - f₁ x‖

pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
mul_sub,

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ * 1 - ‖f₂ x‖ * c ≤ ‖f₂ x - f₁ x‖

α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c