mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_3_to_5 :
  UniformEquicontinuous (DFunLike.coe ∘ f) →
    BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
        Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_3_to_5 :
  UniformEquicontinuous (DFunLike.coe ∘ f) →
    BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))
tfae_5_to_4 :
  BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k))) →
    ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
        Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ (-f x) y = -(f x) y

Tactic:
neg_apply

Goal state after:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ -(f x) y = -(f x) y
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup (p ∘ ⇑e)

Tactic:
use {e.symm i}, 1

Goal state after:
case h
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {e.symm i}.sup (p ∘ ⇑e)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : ι → TopologicalSpace E
ht : ∀ (i : ι), PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
let _ : TopologicalSpace E := ⨅ i, t i

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : ι → TopologicalSpace E
ht : ∀ (i : ι), PolynormableSpace 𝕜 E
x✝ : TopologicalSpace E := ⨅ i, t i
⊢ PolynormableSpace 𝕜 E
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ 0 < (μ s)⁻¹ * μ (s ∩ t)

Tactic:
refine ENNReal.mul_pos ?_ hci

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ (μ s)⁻¹ ≠ 0
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
exact limsup_const_mul_of_ne_top ha_top

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
have hau : (a * u ·) =ᶠ[f] 0 := hu.mono fun x hx => by simp [hx]

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : (fun x ↦ a * u x) =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ (∑ x, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = ∑ x, μ (X ⁻¹' {x} ∩ E)

Tactic:
simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]
      simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]

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

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
comap_generateFrom

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ generateFrom ((preimage fun b ↦ b i) '' C i) ≤ generateFrom (univ.pi '' univ.pi C)
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (↑(#s))⁻¹ * ↑(#(s ∩ t)) = ↑(#(s ∩ t)) / ↑(#s)

Tactic:
rw [div_eq_mul_inv, mul_comm]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x ↦ rexp (f x)
⊢ Measurable f

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x ↦ rexp (f x)
this : f = fun x ↦ log (rexp (f x))
⊢ Measurable f
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x ↦ rexp (f x)) μ
⊢ AEMeasurable f μ

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x ↦ rexp (f x)) μ
this : f = fun x ↦ log (rexp (f x))
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ε = ∞
this : 0 ^ p.toReal = 0
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
simp [h, this, hmeas_top]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), (μ i).IsInvInvariant
⊢ (Measure.pi μ).IsInvInvariant

Tactic:
by
  refine ⟨(Measure.pi_eq fun s hs => ?_).symm⟩
  have A : Inv.inv ⁻¹' pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i := by ext; simp
  simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq_neg : q < 0
⊢ eLpNorm' 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hμ, hq_neg]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ

Tactic:
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul]
    using eLpNorm_const_smul_le (c := c⁻¹) (f := c • f)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ) ((μ 0).prod (μ 1))

Tactic:
refine ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => ?_).symm⟩
  rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod,
    Measure.pi_pi, Fin.prod_univ_two]
  rfl

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
⊢ y⁻¹ * (y - x) < log y - log x

Tactic:
have hxy'' : x / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
hxy' : 0 < x / y
hxy'' : x / y ≠ 1
⊢ y⁻¹ * (y - x) < log y - log x
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
eLpNorm_eq_eLpNorm' hp0 hp_top,

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' f p.toReal (μ.restrict s) = eLpNorm' f p.toReal μ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
hp : 1 < p
⊢ p.HolderConjugate q ↔ q = p / (p - 1)

Tactic:
rw [← holderConjugate_coe_iff, Real.holderConjugate_iff_eq_conjExponent (by exact_mod_cast hp),
    ← coe_one, ← NNReal.coe_sub hp.le]
  exact_mod_cast Iff.rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ c ^ (1 / p).toReal • eLpNorm f p μ < ∞

Tactic:
exact ENNReal.mul_lt_top (Ne.lt_top (by simp [hc])) hf.2

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
hq : 0 < q.toReal
⊢ p.toReal.HolderConjugate q.toReal

Tactic:
simpa using HolderTriple.toReal 1 (zero_lt_one.trans hp) hq

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ liminf (fun n ↦ 1) atTop < ∞

Tactic:
rw [liminf_const (1 : ℝ≥0∞)]

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ 1 < ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case insert
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ ≤ ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
| insert i₀ s hi₀ ih =>

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
have hq0 : q ≠ 0 := by
    by_contra hq_eq_zero
    obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
    rw [ENNReal.toReal_zero] at hp_pos
    exact (lt_irrefl _) hp_pos

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
⊢ eLpNorm f p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ eLpNorm (fun i ↦ ‖f i‖ * ‖g i‖) p μ ≤ eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
eLpNorm_eq_lintegral_rpow_enorm_toReal hp₁.ne' hp₂.ne,

Goal state after:
case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ (∫⁻ (x : α), ‖‖f x‖ * ‖g x‖‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    eLpNorm f ∞ μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i ↦ f i * g i) (∑' (i : ι), f i * g i)

Tactic:
· simpa only [rpow_self_rpow_inv hpq.ne_zero] using H₁.hasSum

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
⊢ (fun x ↦ 0) ≤ fun i ↦ μ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) i x) (s.indicator g x)}

pp: case refine_2
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
⊢ (fun i ↦ μ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) i x) (s.indicator g x)}) ≤ fun i ↦
    μ {x | ε ≤ edist (f i x) (g x)}

Tactic:
· intro; simp

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
⊢ (fun i ↦ μ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) i x) (s.indicator g x)}) ≤ fun i ↦
    μ {x | ε ≤ edist (f i x) (g x)}
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
have : ∀ i, ∃ c : 𝕜, c ≠ 0 ∧ ∀ c' : 𝕜, ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i := fun i ↦ by
      rw [isVonNBounded_pi_iff] at hs
      have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ i))
      rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩
      rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, hc⟩
      refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
      exact hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
this : ∀ (i : ι), ∃ c, c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ Absorbs 𝕜 V (⇑f '' s)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
let _ : NontriviallyNormedField 𝕜 := ⟨by simpa using h₁⟩
    obtain ⟨I, t, ht₀, hft⟩ :
        ∃ (I : Finset ι) (t : ∀ i, Set (E i)), (∀ i, t i ∈ 𝓝 0) ∧ Set.pi I t ⊆ f ⁻¹' V := by
      have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV
      rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV
    have : ∀ i, ∃ c : 𝕜, c ≠ 0 ∧ ∀ c' : 𝕜, ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i := fun i ↦ by
      rw [isVonNBounded_pi_iff] at hs
      have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ i))
      rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩
      rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, hc⟩
      refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
      exact hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩
    choose c hc₀ hc using this
    rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
    have hc₀' : ∏ i ∈ I, c i ≠ 0 := Finset.prod_ne_zero_iff.2 fun i _ ↦ hc₀ i
    refine ⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩
    let ⟨i₀⟩ := ‹Nonempty ι›
    set y := I.piecewise (fun i ↦ c i • x i) x
    calc
      f (update y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) ∈ V := hft fun i hi => by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx
      _ = a • f x := by
        rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : ∀ (i : β), μ (f i) ≠ ∞
⊢ μ.real (⋃ b, f b) = ∑ p, μ.real (f p)

Tactic:
simp_rw [measureReal_def, measure_iUnion hn h, tsum_fintype,
    ENNReal.toReal_sum (fun i _hi ↦ h' i)]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ.real sᶜ = 1 - μ.real s

Tactic:
measureReal_compl₀ h,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ.real univ - μ.real s = 1 - μ.real s