mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inr.inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ limsup (fun a ↦ (u a).toReal) f ≤ r

pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ limsup u f ≠ ∞

Tactic:
limsup_le_iff

Goal state after:
case inr.inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y

α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
⊢ limsup u f ≠ ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

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

Tactic:
apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    rw [univ_pi_eq_iInter]; apply MeasurableSet.iInter; intro i
    apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
    exact measurableSet_generateFrom (hs i (mem_univ i))

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = 0 * (uniformOn s) t

Tactic:
zero_mul,

Goal state after:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = 0
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : f ≤ f'
hg : g ≤ f'
⊢ f ⊔ g ≤ f'

Tactic:
by
  rw [← coeFn_le] at hf hg ⊢
  filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup
  rw [ha_sup]
  exact sup_le haf hag

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)

Tactic:
intro h s hs; refine (h _ hs).trans_eq (piPremeasure_pi hs)

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
⊢ (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod

Tactic:
by
  induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    simp only [foldr_cons, prod_cons, map_cons]
    rw [prod_prod, ih]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ∞

Tactic:
by_cases h : ε = ∞
  · simp [h]
  exact hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top hε (by simp)

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✝ : ESeminormedAddMonoid ε
⊢ 0 < ∞

Tactic:
exact ENNReal.coe_lt_top

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (-f y - -f x) / (y - x) ≤ (-f z - -f y) / (z - y)
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
linear_combination this

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (-f y - -f x) / (y - x) < (-f z - -f y) / (z - y)
⊢ (f z - f y) / (z - y) < (f y - f x) / (y - x)

Tactic:
linear_combination this

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✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C
⊢ eLpNorm f p 0 ≤ C • 0 Set.univ ^ p.toReal⁻¹

case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ p ≠ ∞

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConcaveOn 𝕜 s f

Tactic:
← neg_convexOn_iff

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConvexOn 𝕜 s (-f)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case refine_1
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑q ↑r
⊢ p.HolderTriple q r

Tactic:
rw [NNReal.holderTriple_iff]

Goal state after:
case refine_1
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑q ↑r
⊢ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
rw [← neg_div_neg_eq]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : a < y
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : 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
⊢ z i ^ w i = 0

Tactic:
· rw [hzi]
      exact zero_rpow hwi

Goal state after:
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 μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

pp: case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ∞

Tactic:
hpq.inv_add_inv_ennreal

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ 1 = 1

case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ∞
Module: Mathlib.Analysis.MeanInequalitiesPow

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
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)

Tactic:
← rpow_le_rpow_iff _ _ this,

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
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ((∑ i ∈ s, w i * z i ^ p) ^ (1 / p)) ^ p

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i ∈ s, w i * z i

ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ 0 * z i = 0 * x

Tactic:
zero_mul,

Goal state after:
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i ∈ s, w i = 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ 0 = 0 * x
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
have hb : b ≤ 1 := (self_le_add_left b a).trans hab

Goal state after:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p

Tactic:
nth_rw 4 [← mul_one ((a + b) ^ p)]

Goal state after:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : 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
⊢ z i ^ w i = 0

Tactic:
· rw [hzi]
      exact zero_rpow hwi

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
by
  rw [← @lintegral_zero_fun α _ μ]
  refine lintegral_congr_ae ?_
  suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero
  have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero
  exact hf_eq_zero.mul (ae_eq_refl g)

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

Goal state before:
pp: case ha
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ eLpNorm (↑↑f) p μ ≠ ∞

pp: case hb
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ c • eLpNorm (↑↑g) p μ ≠ ∞

Tactic:
· finiteness

Goal state after:
case hb
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ≥0
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊
this : eLpNorm (↑↑f) p μ ≤ c • eLpNorm (↑↑g) p μ
⊢ c • eLpNorm (↑↑g) p μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ edist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
specialize hfg ((2⁻¹ : ℝ≥0∞) ^ n) (ENNReal.pow_pos (by simp) _)
  rw [ENNReal.tendsto_atTop_zero] at hfg
  exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr <| pow_ne_zero _ <| by simp)

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

Goal state before:
pp: E : Type u_4
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
⊢ compMeasurePreserving id ⋯ = AddMonoidHom.id ↥(Lp E p μb)

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (L + L').compLp f = L.compLp f + L'.compLp f

Tactic:
by
  ext1
  grw [Lp.coeFn_add, coeFn_compLp', coeFn_compLp', coeFn_compLp']
  rfl

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
g✝ : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
⊢ L.compLp (f + g) = L.compLp f + L.compLp g

Tactic:
by
    ext1
    filter_upwards [Lp.coeFn_add f g, coeFn_compLp L (f + g), coeFn_compLp L f,
      coeFn_compLp L g, Lp.coeFn_add (L.compLp f) (L.compLp g)]
    intro a ha1 ha2 ha3 ha4 ha5
    simp only [ha1, ha2, ha3, ha4, ha5, map_add, Pi.add_apply]

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
g : E → F
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
a✝ : α
ha1 : ↑↑(c • f) a✝ = (c • ↑↑f) a✝
ha2 : ↑↑(L.compLp (c • f)) a✝ = L (↑↑(c • f) a✝)
ha3 : ↑↑(σ c • L.compLp f) a✝ = (σ c • ↑↑(L.compLp f)) a✝
ha4 : ↑↑(L.compLp f) a✝ = L (↑↑f a✝)
⊢ ↑↑(L.compLp (c • f)) a✝ = ↑↑(σ c • L.compLp f) a✝

Tactic:
simp only [ha1, ha2, ha3, ha4, Pi.smul_apply, map_smulₛₗ]

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
Φ : ↑(range (g ∘ f)) ≃ₜ ↑(range g) := Homeomorph.setCongr ⋯
key : rangeFactorization g ∘ f = ⇑Φ ∘ rangeFactorization (g ∘ f)
⊢ IsQuotientMap (rangeFactorization g) ↔ IsQuotientMap (rangeFactorization (g ∘ f))

Tactic:
← f_quot.of_comp_iff,

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 ⋯
key : rangeFactorization g ∘ f = ⇑Φ ∘ rangeFactorization (g ∘ f)
⊢ IsQuotientMap (rangeFactorization g ∘ f) ↔ IsQuotientMap (rangeFactorization (g ∘ f))
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
⊢ ∀ (ib : Set (ContinuousMultilinearMap 𝕜 E F) × Set ((i : ι) → E i) × Set G),
    IsVonNBounded 𝕜 ib.1 ∧ IsVonNBounded 𝕜 ib.2.1 ∧ ib.2.2 ∈ 𝓝 0 →
      ∃ ia,
        (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧
          ∀ x ∈ {f | ∀ x ∈ ia.1, f x ∈ ia.2}, aux x ∈ {f | ∀ x ∈ ib.1, f x ∈ {f | MapsTo (⇑f) ib.2.1 ib.2.2}}

Tactic:
rintro ⟨U, V, W⟩ ⟨hU, hV, hW⟩

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst✝¹³ : NormedField 𝕜
inst✝¹² : (i : ι) → TopologicalSpace (E i)
inst✝¹¹ : (i : ι) → AddCommGroup (E i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  { toFun := fun g ↦ { toFun := g.compContinuousMultilinearMap, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : (U, V, W).2.2 ∈ 𝓝 0
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧
      ∀ x ∈ {f | ∀ x ∈ ia.1, f x ∈ ia.2},
        aux x ∈ {f | ∀ x ∈ (U, V, W).1, f x ∈ {f | MapsTo ⇑f (U, V, W).2.1 (U, V, W).2.2}}
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (0, x✝)

Tactic:
ext <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
⊢ s =ᶠ[l] t

Tactic:
exact this.symm.trans <| h.mulSupport.trans this

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
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by
  by_cases hp_top : p = ∞
  · rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]
    exact norm_indicatorConstLp_top hμs_pos
  · exact norm_indicatorConstLp hp_pos hp_top

Goal state after: