mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

Tactic:
exact isOpenMap_inr _ <| (hu.preimage continuous_inr).pathComponentIn _

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝¹ y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
x✝ : X × Y
x : X
y : Y
U : Set (X × Y)
hU : U ∈ 𝓝 (x, y)
⊢ ∃ r ∈ 𝓝 (x, y), IsPathConnected r ∧ r ⊆ U

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.mp hU
    exact ⟨pathComponentIn u x ×ˢ pathComponentIn v y,
      prod_mem_nhds (pathComponentIn_mem_nhds hu) (pathComponentIn_mem_nhds hv),
      (isPathConnected_pathComponentIn (mem_of_mem_nhds hu)).prod
        (isPathConnected_pathComponentIn (mem_of_mem_nhds hv)),
      (Set.prod_mono pathComponentIn_subset pathComponentIn_subset).trans huv⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E

Tactic:
cases b

Goal state after:
case false
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

case true
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs : (affineCombination k s p) w ∈ line[k, p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)

Tactic:
rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩

Goal state after:
case refine_1.refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ s
⊢ ∀ y ∈ s, 0 ≤ if x = y then 1 else 0

case refine_1.refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ s
⊢ (∑ y ∈ s, if x = y then 1 else 0) = 1
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = 𝓝 0

Tactic:
nhds_iInf

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = 𝓝 0

Tactic:
nhds_iInf

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace

Tactic:
by
  rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
  congrm _ = ⨅ i, ?_
  exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
a : 𝕜
ha : r < ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
specialize h a (le_of_lt ha)

Goal state after:
case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
h : s ⊆ a • (I.sup p).ball 0 1
ha : r < ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → 𝐤Y
K : Set X
hK : IsCompact K
⊢ ContinuousOn f K ↔ ContinuousOn (⇑(CompactCoherentification.mk Y).symm ∘ f) K

Tactic:
by
  refine ⟨fun H ↦ continuous_mk_symm.comp_continuousOn H, fun H ↦ ?_⟩
  exact continuousOn_isCompact_mk (hK.image_of_continuousOn H) |>.comp H (mapsTo_image f K)

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht')

Goal state after:
case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : ∅.Finite
hst : Disjoint ∅ ∅
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ + (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ = (uniformOn (∅ ∪ ∅)) u

case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht')

Goal state after:
case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u
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 : (univ.pi s).Nonempty
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i, (m i) (s i)

Tactic:
exact (boundedBy_le _).trans_eq (piPremeasure_pi h)

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀, ENNReal.rpow_one]

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0
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✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (map (⇑(MeasurableEquiv.piMeasurableEquivTProd ?hnd ⋯).symm) (Measure.tprod (sortedUniv ι) μ)) (univ.pi s) =
    ∏ i, (μ i) (s i)

pp: case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

Tactic:
MeasurableEquiv.map_apply,

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.tprod (sortedUniv ι) μ) (⇑(MeasurableEquiv.piMeasurableEquivTProd ?hnd ⋯).symm ⁻¹' univ.pi s) =
    ∏ i, (μ i) (s i)

case hnd
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
x : α
this : ¬p < 0
⊢ ↑c ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p

Tactic:
simp [ENNReal.mul_rpow_eq_ite, this]

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 : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' ↦ μ (f i'))) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
MeasurableEquiv.map_apply,

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi fun i' ↦ μ (f i')) (⇑(MeasurableEquiv.piCongrLeft α f) ⁻¹' univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i ↦ (μ i).prod (ν i)))
      ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t))

Tactic:
MeasurableEquiv.map_apply,

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i))
      (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t))
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (X i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
        ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i))))
      (univ.pi s) =
    ∏ i, (μ i) (s i)

Tactic:
MeasurableEquiv.map_apply,

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (X i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i)))
      (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm ⁻¹' univ.pi s) =
    ∏ i, (μ i) (s i)
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
⊢ (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))

Tactic:
ext1 s

Goal state after:
ι : 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
s : Set ((i : ι) → X i)
⊢ piPremeasure (fun i ↦ (μ i).toOuterMeasure) s = (Measure.map (⇑e.symm) (μ default)) s
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (Measure.map (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = (μ 0) s * (μ 1) t

Tactic:
MeasurableEquiv.map_apply,

Goal state after:
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (Measure.pi μ) (⇑(MeasurableEquiv.piFinTwo α) ⁻¹' s ×ˢ t) = (μ 0) s * (μ 1) t
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
rw [eLpNorm_eq_eLpNorm' h0 hp_top, eLpNorm_eq_eLpNorm' _ (by finiteness)]

Goal state after:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ∞
⊢ p * ENNReal.ofReal q ≠ 0
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p⁻¹ - 1 = -q⁻¹

Tactic:
simpa using congr(-$(h.one_sub_inv))

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

Goal state before:
pp: p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r

Tactic:
by
  simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
  apply toReal_iff r ?_ ?_
  all_goals simpa [← coe_toNNReal_eq_toReal]

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ (y ^ p - x ^ p) / (y - x) < p * y ^ (p - 1)

Tactic:
rw [div_lt_iff₀ q, ← div_lt_div_iff_of_pos_right hy', _root_.sub_div, div_self hy'.ne',
      ← div_rpow hx hy.le, sub_lt_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc,
      ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
      mul_assoc, ← div_eq_inv_mul, sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div,
      div_self hy.ne']

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 + p * (x / y - 1) < (1 + (x / y - 1)) ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ x / y - 1 ≠ 0

Tactic:
· rw [sub_ne_zero]
      exact ((div_lt_one hy).mpr hxy).ne

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case convert_2
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∑ i ∈ s, w i) * (∑ i ∈ s, w i)⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ (by linarith)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i

Tactic:
rw [hx i hi h₀]

Goal state after:
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 * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
rw [@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]), ← ENNReal.rpow_mul, ←
        ENNReal.rpow_mul]
      have hpp2 : p * p2 = q := by
        symm
        rw [mul_comm, ← div_eq_iff hp0_ne]
      have hpq2 : p * q2 = r := by
        rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
        simp [field, p2, q2, Real.conjExponent]
      simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
⊢ (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) n ≤ (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) n

Tactic:
simp only [hε_top]

Goal state after:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
⊢ μ {x | ∞ ≤ edist (f n x) (g x)} ≤ μ {ω | 1 ≤ edist (f n ω) (g ω)}
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ
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:
by
  have := NNReal.coe_le_coe.2
    (NNReal.Lp_add_le s (fun i => .mk _ (abs_nonneg (f i))) (fun i => .mk _ (abs_nonneg (g i))) hp)
  push_cast at this
  refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this <;>
    simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝

Tactic:
← hx₂

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝
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 : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) p μ

Tactic:
exact eLpNorm_congr_ae (hf.coeFn_toLp.sub hg.coeFn_toLp)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i = ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_
      simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]

Goal state after: