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

Goal state before:
pp: case neg
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
⊢ (insert i t).centerMass w z ∈ s

Tactic:
Finset.centerMass_insert _ _ _ hi hsum_t

Goal state after:
case neg
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1

Tactic:
intro y hxy

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
⊢ (pathComponent x)ᶜ ∈ 𝓝 y
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_3
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
⊢ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x} ⊆ (convexHull R) (Set.range v)

Tactic:
rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ hw₁

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
have hj : j ∉ u := by simp [u]

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj✝ : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ ediam ((convexHull ℝ) s) = ediam s

Tactic:
refine (ediam_le fun x hx y hy => ?_).antisymm (ediam_mono <| subset_convexHull ℝ s)

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
⊢ edist x y ≤ ediam s
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ (w j / c) • p j + (w k / c) • p k ∈ s

Tactic:
by
           refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc <;> positivity

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

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c⁻¹‖
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ∀ (x : E), ε / ‖c⁻¹‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖

Tactic:
rwa [norm_inv, div_eq_mul_inv, inv_inv]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Tactic:
by
  simpa [enorm, ← ENNReal.coe_mul] using opNNNorm_comp_le h f

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)

Tactic:
by
  by_cases hf : f.IsCoboundedUnder (· ≥ ·) u; swap
  · simp [*]
  refine eq_of_forall_le_iff fun c ↦ ?_
  rw [← Real.toNNReal_le_iff_le_coe, le_liminf_iff (by simpa) ⟨0, by simp⟩, le_liminf_iff]
  simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]
  refine forall₂_congr fun r hr ↦ ?_
  simpa using (le_or_gt 0 r).imp_right fun hr ↦ .of_forall fun i ↦ hr.trans_le (by simp)

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

Goal state before:
pp: case inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

Tactic:
by_cases hf : f.IsBoundedUnder (· ≤ ·) u

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (univ.pi fun a ↦ ⋃ j, s a j) = univ

Tactic:
h2s,

Goal state after:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (univ.pi fun a ↦ univ) = univ
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y) → ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y

Tactic:
rintro h x hx
    have : 0 < x := hx.trans_le' (by simp)
    filter_upwards [h (.ofReal x) (by simpa [this] using hx)] with a ha
    exact (toReal_lt_of_lt_ofReal ha).trans_le' (by simp [toReal_ofReal'])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
by
  simp_rw [essSup, Measure.ae_smul_measure_eq hc]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ (uniformOn s) (t ∪ u) = (uniformOn s) t + (uniformOn s) u

Tactic:
by
  rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]
  exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]

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

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

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Goal state after:
case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

case inr.inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

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

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : univ.pi s = ∅
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i, (m i) (s i)

case inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : (univ.pi s).Nonempty
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i, (m i) (s i)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case empty
α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
f : ι → α →ₘ[μ] γ
⊢ ↑(∏ i ∈ ∅, f i) =ᵐ[μ] ∏ i ∈ ∅, ↑(f i)

Tactic:
simp [coeFn_one]

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)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
⊢ (Measure.pi μ).FiniteSpanningSetsIn (univ.pi '' univ.pi C)

Tactic:
haveI := fun i => (hμ i).sigmaFinite
  haveI := Fintype.toEncodable ι
  refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).getD default i),
    fun n => ?_, fun n => ?_, ?_⟩ <;>
  -- TODO (kmill) If this let comes before the refine, while the noncomputability checker
  -- correctly sees this definition is computable, the Lean VM fails to see the binding is
  -- computationally irrelevant. The `noncomputable section` doesn't help because all it does
  -- is insert `noncomputable` for you when necessary.
  let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).getD default
  · refine mem_image_of_mem _ fun i _ => (hμ i).set_mem _
  · calc
      Measure.pi μ (Set.pi univ fun i => (hμ i).set (e n i)) ≤
          Measure.pi μ (Set.pi univ fun i => toMeasurable (μ i) ((hμ i).set (e n i))) :=
        measure_mono (pi_mono fun i _ => subset_toMeasurable _ _)
      _ = ∏ i, μ i (toMeasurable (μ i) ((hμ i).set (e n i))) :=
        (pi_pi_aux μ _ fun i => measurableSet_toMeasurable _ _)
      _ = ∏ i, μ i ((hμ i).set (e n i)) := by simp only [measure_toMeasurable]
      _ < ∞ := ENNReal.prod_lt_top fun i _ => (hμ i).finite _
  · simp_rw [(surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x =>
        Set.pi univ fun i => (hμ i).set (x i),
      iUnion_univ_pi fun i => (hμ i).set, (hμ _).spanning, Set.pi_univ]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : (μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : (μ i) t = 0
⊢ (Measure.pi μ) (eval i ⁻¹' t) = 0

Tactic:
← univ_pi_update_univ,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : (μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : (μ i) t = 0
⊢ (Measure.pi μ) (univ.pi (update (fun j ↦ univ) i t)) = 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
this : (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))
⊢ Measure.map (⇑e) (Measure.map (⇑e.symm) (μ default)) = μ default

Tactic:
MeasurableEquiv.map_map_symm

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
⊢ Measure.map (⇑(MeasurableEquiv.piUnique X)) (Measure.pi μ) = μ default

Tactic:
set e := MeasurableEquiv.piUnique X
    have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by
      ext1 s
      rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
      congr 1; exact e.toEquiv.image_eq_preimage_symm s
    simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]

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

Goal state before:
pp: ι : Type u_4
inst✝² : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝¹ : (i : ι) → MeasurableSpace (α i)
inst✝ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (Measure.map (f i) (μ i))
⊢ Measure.map (fun a i ↦ f i (a i)) (Measure.pi μ) = Measure.pi ν

Tactic:
rw [pi_map_pi (fun i ↦ (hf i).aemeasurable)]

Goal state after:
ι : Type u_4
inst✝² : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst✝¹ : (i : ι) → MeasurableSpace (α i)
inst✝ : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (Measure.map (f i) (μ i))
⊢ (Measure.pi fun i ↦ Measure.map (f i) (μ i)) = Measure.pi ν
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝¹ : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst✝ : p.HolderTriple q' r
⊢ r⁻¹ - p⁻¹ = q'⁻¹

Tactic:
← inv_sub_inv_eq_inv q' p hr

Goal state after:
p q r : ℝ≥0∞
inst✝¹ : p.HolderTriple q r
q' : ℝ≥0∞
hr : r ≠ 0
inst✝ : p.HolderTriple q' r
⊢ r⁻¹ - p⁻¹ = r⁻¹ - p⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
have hp_pos : 0 < p := by positivity
  by_cases h_zero : a + b = 0
  · simp [add_eq_zero.mp h_zero, hp_pos.ne']
  have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
  have h_add : a / (a + b) + b / (a + b) = 1 := by rw [← add_div, div_self h_zero]
  have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
  rw [div_rpow a (a + b), div_rpow b (a + b)] at h
  have hab_0 : (a + b) ^ p ≠ 0 := by simp [h_nonzero]
  have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p := by
    nth_rw 4 [← mul_one ((a + b) ^ p)]; gcongr
  rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ←
    mul_assoc, mul_inv_cancel₀ hab_0, one_mul, one_mul] at h_mul

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : 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 ≠ ∞
i : ι
h_top : w i * z i ≠ ∞
hi : i ∈ s
⊢ w i * z i ^ p ≠ ∞

Tactic:
rwa [Ne, ← h_top_iff_rpow_top i hi]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case a
ι : 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 : ι
hi : i ∈ s
⊢ ∑ x ∈ s, w x ≠ ∞

Tactic:
exact hw'.symm ▸ ENNReal.one_ne_top

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
hpq_eq,

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ eLpNorm' f q μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / q - 1 / q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p ∂μ < ∞

Tactic:
lintegral_add_left',

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), 2 ^ (p - 1) * f a ^ p ∂μ + ∫⁻ (a : α), 2 ^ (p - 1) * g a ^ p ∂μ < ∞

case hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ AEMeasurable (fun a ↦ 2 ^ (p - 1) * f a ^ p) μ
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ∞
⊢ (f + g) a ^ p = (f + g) a ^ (1 + (p - 1))

Tactic:
add_sub_cancel

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ∞
⊢ (f + g) a ^ p = (f + g) a ^ p
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 μ)
⊢ (fun a ↦ (L + L') (↑↑f a)) =ᵐ[μ] (fun a ↦ L (↑↑f a)) + ↑↑(L'.compLp f)

Tactic:
coeFn_compLp'

Goal state after:
α : 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 μ)
⊢ (fun a ↦ (L + L') (↑↑f a)) =ᵐ[μ] (fun a ↦ L (↑↑f a)) + fun a ↦ L' (↑↑f a)
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 σ
𝕜'' : Type u_8
inst✝³ : NormedRing 𝕜''
inst✝² : Module 𝕜'' F
inst✝¹ : IsBoundedSMul 𝕜'' F
inst✝ : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (fun a ↦ (c • L) (↑↑f a)) =ᵐ[μ] c • ↑↑(L.compLp f)

Tactic:
coeFn_compLp'

Goal state after:
α : 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 σ
𝕜'' : Type u_8
inst✝³ : NormedRing 𝕜''
inst✝² : Module 𝕜'' F
inst✝¹ : IsBoundedSMul 𝕜'' F
inst✝ : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (fun a ↦ (c • L) (↑↑f a)) =ᵐ[μ] c • fun a ↦ L (↑↑f a)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
by
  have h_summable : ∀ᵐ x ∂μ, Summable fun i : ℕ => f (i + 1) x - f i x := by
    have h1 :
      ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
      eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau
    have h2 n :
        ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p :=
      lintegral_rpow_sum_enorm_sub_le_rpow_tsum hp1 n (h1 n)
    have h3 : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i :=
      lintegral_rpow_tsum_coe_enorm_sub_le_tsum hf hp1 h2
    have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
      tsum_enorm_sub_ae_lt_top hf hp1 hB h3
    exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne
  refine h_summable.mono fun x hx ↦ ?_
  have hx_sum := hx.hasSum.tendsto_sum_nat
  rw [funext fun n ↦ Finset.sum_range_sub (fun m ↦ f m x) n] at hx_sum
  exact ⟨∑' i, (f (i + 1) x - f i x) + f 0 x, by simpa using hx_sum.add_const (f 0 x)⟩

Goal state after: