mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
by
  rw [← neg_smul_neg]
  exact hf.neg.smul' hg.neg (fun x hx ↦ neg_nonneg.2 <| hf₀ hx) (fun x hx ↦ neg_nonneg.2 <| hg₀ hx)
    hfg.neg

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ ((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ ∑ a ∈ s, (w a * z a ^ p).toNNReal

Tactic:
toNNReal_rpow,

Goal state after:
case refine_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ (∑ i ∈ s, w i * z i).toNNReal ^ p ≤ ∑ a ∈ s, (w a * z a ^ p).toNNReal
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
by
  rw [← neg_smul_neg]
  exact hf.neg.smul' hg.neg (fun x hx ↦ neg_nonneg.2 <| hf₀ hx) (fun x hx ↦ neg_nonneg.2 <| hg₀ hx)
    hfg.neg

Goal state after:
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
by
  rw [← neg_concaveOn_iff, ← smul_neg]
  exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ z k ^ ∑ x ∈ s, w x = ∑ i ∈ s, w i * z k

Tactic:
← sum_mul,

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
⊢ z k ^ ∑ x ∈ s, w x = (∑ i ∈ s, w i) * z k
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
this : DecidableEq ι
⊢ MemLp (fun a ↦ ∑ i ∈ s, f i a) p μ

Tactic:
revert hf

Goal state after:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst✝ : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
⊢ (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a ↦ ∑ i ∈ s, f i a) p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ 0 ≤ q⁻¹

Tactic:
simp [hq_pos.le]

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q)

Tactic:
by
  have h_le : (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ≤ ∫⁻ _ : α, eLpNormEssSup f μ ^ q ∂μ := by
    refine lintegral_mono_ae ?_
    have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ
    exact h_nnnorm_le_eLpNorm_ess_sup.mono fun x hx => by gcongr
  rw [eLpNorm', ← ENNReal.rpow_one (eLpNormEssSup f μ)]
  nth_rw 2 [← mul_inv_cancel₀ (ne_of_lt hq_pos).symm]
  rw [ENNReal.rpow_mul, one_div, ← ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ q⁻¹)]
  gcongr
  rwa [lintegral_const] at h_le

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ x ∈ s, f x ^ p / p.toNNReal + ∑ x ∈ s, g x ^ q / q.toNNReal =
    ∑ i ∈ s, f i ^ p / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal

Tactic:
sum_div

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ x ∈ s, f x ^ p / p.toNNReal + ∑ x ∈ s, g x ^ q / q.toNNReal =
    ∑ i ∈ s, f i ^ p / p.toNNReal + ∑ i ∈ s, g i ^ q / q.toNNReal
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
suffices h :
    1 ≤
      (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) by
    rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
by
  rcases eq_or_lt_of_le hp with hp | hp
  · simp [← hp]
  let q : ℝ := p / (p - 1)
  have hpq : p.HolderConjugate q := .conjExponent hp
  have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
  have hq : 1 / q * p = p - 1 := by
    rw [← hpq.div_conj_eq_sub_one]
    ring
  simpa only [NNReal.mul_rpow, ← NNReal.rpow_mul, hp₁, hq, one_mul, one_rpow, rpow_one,
    Pi.one_apply, sum_const, Nat.smul_one_eq_cast] using
    NNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f - g)) p μ = ENNReal.ofReal (eLpNorm (↑↑(f - g)) p μ).toReal

Tactic:
ENNReal.ofReal_toReal (eLpNorm_ne_top (f - g))

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f - g)) p μ = eLpNorm (↑↑(f - g)) p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ), (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i
⊢ eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
rw [hgf_norm_diff]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ), (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i
⊢ eLpNorm' (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
⊢ Function.Injective fun x ↦
    match x with
    | Sum.inl a => f a
    | Sum.inr b => g b

Tactic:
rintro (a₁ | b₁) (a₂ | b₂) f_eq <;>
        simp only at f_eq
      · rw [f.injective f_eq]
      · exfalso
        exact disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp⟩⟩
      · exfalso
        exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩
      · rw [g.injective f_eq]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
⊢ Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)

Tactic:
refine tendsto_zero_iff_norm_tendsto_zero.mpr ?_

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
⊢ Tendsto (fun x_1 ↦ ‖x_1 - ↑x‖) (𝓝 ↑x) (𝓝 0)
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hf : Filter.comap (⇑f) (𝓝 (f x)) ≤ 𝓝 0
hx : f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖

Tactic:
obtain rfl : x = 0 := Specializes.eq (specializes_iff_pure.2 <|
      ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)

Goal state after:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
hf : Filter.comap (⇑f) (𝓝 (f 0)) ≤ 𝓝 0
hx : f 0 = 0
⊢ ‖0‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f 0‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (fun x ↦ (f x).coprod (g x)) s x

Tactic:
simp only [← comp_fst_add_comp_snd]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s x
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ (f x).coprod (g x)) x

Tactic:
simp only [← comp_fst_add_comp_snd]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) x
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ (f x).coprod (g x)) s

Tactic:
simp only [← comp_fst_add_comp_snd]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝ : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Tactic:
by
  rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (eLpNorm (fun x ↦ c) p μ).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
eLpNorm_const'

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

case h_top
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case neg
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0✝ : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : 0 < ∏ i, ‖δ i‖
⊢ ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
simpa [map_smul_univ, norm_smul, prod_mul_distrib, mul_left_comm C, hδ0] using
    hf (fun i => δ i • m i) hle_δm hδm_lt

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ μ {x | ε ≤ ‖f x‖} < ∞

Tactic:
by
  convert! Integrable.measure_enorm_ge_lt_top hf (ofReal_pos.mpr hε) ofReal_ne_top with x
  rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝⁴ : TopologicalSpace ε
inst✝³ : ContinuousENorm ε
inst✝² : Preorder α
inst✝¹ : IsCodirectedOrder α
inst✝ : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
by
  refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩
  obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
  exact ⟨t, hi.mono_set fun _ hx ↦ ht _ hx⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter (-f) l μ
⊢ IntegrableAtFilter f l μ

Tactic:
convert! h.neg

Goal state after:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter (-f) l μ
⊢ f = - -f
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable f μ

Tactic:
rw [← indicator_add_eq_left h]; exact hfg.indicator hf.measurableSet_support

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x = 0
⊢ f x • ↑↑(u + v) x = f x • ↑↑u x + f x • ↑↑v x

Tactic:
simp only [hx, zero_smul, add_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι

Tactic:
have := (norm_nonneg x).trans hx; gcongr

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ ‖f x‖ ≤ r

Tactic:
calc
      ‖f x‖ ≤ ‖f‖ * ε ^ Fintype.card ι := le_opNorm_mul_pow_card_of_le f hx
      _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
      _ ≤ r := (mul_comm _ _).trans_le hδ.le

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ‖f - g‖ = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal

Tactic:
rw [norm_def]
  congr 1
  rw [lintegral_congr_ae]
  filter_upwards [Lp.coeFn_sub f g] with _ ha
  simp only [ha, Pi.sub_apply]

Goal state after: