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
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • a) • f x • g x + (b • a) • f y • g x + ((a • f x) • b • g y + (b • f y) • b • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)

Tactic:
← smul_smul_smul_comm a b,

Goal state after:
𝕜 : 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 : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • a) • f x • g x + (b • a) • f y • g x + ((a • b) • f x • g y + (b • f y) • b • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : 0 = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ ∀ i ∈ s, 0 ≤ w i * z i

Tactic:
exact fun i hi => (mul_nonneg_iff_of_pos_left (hw i hi)).mpr (hz i hi)

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
h_rpow b,

Goal state after:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x ↦ f x ^ p) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0

Tactic:
filter_upwards [hf_zero] with x

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x ↦ f x ^ p) =ᵐ[μ] 0
x : α
⊢ f x ^ p = 0 x → f x = 0 x
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 : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x) =
    (a • a) • f x • g x + (b • a) • f y • g x + ((a • f x) • b • g y + (b • f y) • b • g y)

Tactic:
← smul_smul_smul_comm a b,

Goal state after:
𝕜 : 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 : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x) =
    (a • a) • f x • g x + (b • a) • f y • g x + ((a • b) • f x • g y + (b • f y) • b • g y)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
h_rpow b,

Goal state after:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

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

Tactic:
top_le_iff

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : q = ∞
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ q = ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p) ≤
    ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p)

Tactic:
gcongr
      simp_rw [ENNReal.rpow_mul]
      exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)

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

Goal state before:
pp: case inr.inr.inr.inl
α : 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 α
f : α → E
g : α → F
p r : ℝ≥0∞
hf : AEStronglyMeasurable 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
hpqr✝ : p.HolderTriple ∞ r
hpqr : 1 / r = 1 / p + 1 / ∞
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g ∞ μ

Tactic:
have : r = p := by simpa using hpqr
    exact this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top p hf g b c h

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
rcases eq_or_lt_of_le hp with (rfl | hp)

Goal state after:
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i ∈ s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i ∈ s, f i ^ 1) ^ (1 / 1) + (∑ i ∈ s, g i ^ 1) ^ (1 / 1)

case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a ↦ f a ^ p) (A ^ p)
hg_sum : HasSum (fun a ↦ g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i ↦ f i * g i) C
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i ↦ ↑(f i) * ↑(g i)) C

Tactic:
refine ⟨C, C.prop, hC, ?_⟩

Goal state after:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a ↦ f a ^ p) (A ^ p)
hg_sum : HasSum (fun a ↦ g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i ↦ f i * g i) C
⊢ HasSum (fun i ↦ ↑(f i) * ↑(g i)) ↑C
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
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
by_cases hμ : μ = 0
  · simp [hμ, nnnorm_def]
  rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]
  refine (eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_
  rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ

Tactic:
simp only [Lp.enorm_def]

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f + g)) p μ ≤ eLpNorm (↑↑f) p μ + eLpNorm (↑↑g) p μ
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
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ ‖(LpToLpOfMeasureLeSMulₗ hc h) f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ

Tactic:
simp only [Lp.enorm_def]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ eLpNorm (↑↑((LpToLpOfMeasureLeSMulₗ hc h) f)) p μ ≤ c ^ (1 / p).toReal * eLpNorm (↑↑f) p ν
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
hx : x ∈ nonunits R
h₁ : x ∈ Metric.ball 1 1
⊢ ‖1 - x‖ < 1

Tactic:
by rwa [mem_ball_iff_norm'] at h₁

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜₁ : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_8
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedSpace 𝕜₁ E
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜₁
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomIsometric σ₂₃
f : F →SL[σ₂₃] G
e : E ≃ₛₗᵢ[σ₁₂] F
⊢ ‖f ∘SL ↑↑e‖ = ‖f‖

Tactic:
by simp [← coe_nnnorm]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜₁ : Type u_2
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_8
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedSpace 𝕜₁ E
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₃₂ : 𝕜₃ →+* 𝕜₂
inst✝⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomIsometric σ₁₂
e : F ≃ₛₗᵢ[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖↑↑e ∘SL f‖ = ‖f‖

Tactic:
by simp [← coe_nnnorm]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T

Tactic:
by
  simpa [← toLinearMap_comp] using
    LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)

Tactic:
set Φ : range (g ∘ f) ≃ₜ range g := .setCongr <| f_quot.surjective.range_comp g

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : ↑(range (g ∘ f)) ≃ₜ ↑(range g) := Homeomorph.setCongr ⋯
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : μ s₂ ≠ ∞
H : μ s₁ < ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
· exact measureReal_sdiff_null' (measureReal_mono_null inter_subset_right h h') H.ne

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hμs_ne_zero : μ s ≠ 0
⊢ ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖

Tactic:
by
  rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
    eLpNorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.toReal_top,
    _root_.div_zero, ENNReal.rpow_zero, mul_one, toReal_enorm]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
⊢ Integrable f μ

Tactic:
by
  rw [← integrableOn_univ]
  apply hf.of_ae_sdiff_eq_zero nullMeasurableSet_univ
  filter_upwards [h't] with x hx h'x using hx h'x.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetrizableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
h's : IsSeparable s
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f (μ.restrict s) ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_1
𝕜 : 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

Tactic:
simp only [hasBasis_nhds_zero.mem_iff, Prod.exists]

Goal state after:
case refine_1
𝕜 : 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ r a b,
    (Bornology.IsVonNBounded 𝕜 a ∧ b ∈ 𝓝 0) ∧
      {f | Set.MapsTo (⇑f) a b} ⊆ (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict t)

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEMeasurable f (μ.restrict t) ∧ ∃ t_1, IsSeparable t_1 ∧ ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ t_1
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun n ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (fun x ↦ ‖G n x‖ₑ) μ
⊢ ?m.51 =ᵐ[?m.50] ?m.52

Tactic:
filter_upwards [hGf] with x hx using hx.enorm.liminf_eq

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ : E i →L[𝕜] E₁ i
⊢ ∀ (y : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update f i (f₁ + y)) =
      g.compContinuousLinearMap (update f i f₁) + g.compContinuousLinearMap (update f i y)

Tactic:
f₂

Goal state after:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
⊢ g.compContinuousLinearMap (update f i (f₁ + f₂)) =
    g.compContinuousLinearMap (update f i f₁) + g.compContinuousLinearMap (update f i f₂)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
hf' : MemLp (fun x ↦ ‖f x - y₀‖) p μ
x : β
⊢ ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
convert! norm_approxOn_y₀_le fmeas h₀ x n using 1

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
hf' : MemLp (fun x ↦ ‖f x - y₀‖) p μ
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x

Tactic:
rw [measureReal_add_apply, add_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
a0 : a = 0
⊢ g a * μ (⇑f ⁻¹' {a}) ≠ ∞

Tactic:
rw [a0, hg0, zero_mul]; exact WithTop.zero_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
a0 : ¬a = 0
⊢ g a * μ (⇑f ⁻¹' {a}) ≠ ∞

Tactic:
apply mul_ne_top (ht a) (hf'.meas_preimage_singleton_ne_zero a0).ne

Goal state after: