mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
⊢ AffineIndependent k p

Tactic:
intro s w hw hs
    let s' : Finset { y // y ≠ i } := s.subtype (· ≠ i)
    let p' : { y // y ≠ i } → P := fun x => p x
    by_cases his : i ∈ s ∧ w i ≠ 0
    · refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'
    · rw [not_and_or, Classical.not_not] at his
      let w' : { y // y ≠ i } → k := fun x => w x
      have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      intro j hj
      by_cases hji : j = i
      · rw [hji] at hj
        exact hji.symm ▸ his.neg_resolve_left hj
      · exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ![p₁, p₂, p₃] '' {x | x ≠ 2} ⊆ ↑s

Tactic:
Set.image_subset_iff,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ {x | x ≠ 2} ⊆ ![p₁, p₂, p₃] ⁻¹' ↑s
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
u : Set E
h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x
hu_nhds : u ∈ 𝓝 x₀
hu_convex : Convex 𝕜 u
⊢ ∃ i, (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y

Tactic:
refine ⟨u, ⟨hu_nhds, hu_convex⟩, fun x hxu hxs y hy ↦ h ?_ (hs.segment_subset hx₀s hxs hy)⟩

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
u : Set E
h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x
hu_nhds : u ∈ 𝓝 x₀
hu_convex : Convex 𝕜 u
x : E
hxu : x ∈ id u
hxs : x ∈ s
y : E
hy : y ∈ [x₀ -[𝕜] x]
⊢ y ∈ id u
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: 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
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x' y') ≤ ediam s

Tactic:
← edist_dist

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
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ ediam s
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: case h₁
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∑ i ∈ t with w i ≠ 0, w i = 1

Tactic:
sum_filter_ne_zero

Goal state after:
case h₁
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∑ x ∈ t, w x = 1
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✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ 0 < ∑ i ∈ t with w i ≠ 0, w i

Tactic:
sum_filter_ne_zero

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✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ 0 < ∑ x ∈ t, w x
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ S
⊢ ∀ y ∈ s, f y ∈ c • U

Tactic:
x

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ S
x : E
⊢ x ∈ s → f x ∈ c • U
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ≥0∞
hf : ‖f‖ₑ ≤ a
hx : ‖x‖ₑ ≤ b
⊢ ‖f‖ₑ * ‖x‖ₑ ≤ a * b

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
⊢ Continuous[inst✝², inst✝¹] ((⇑(CompactCoherentification.mk Y).symm ∘ ⇑(CompactCoherentification.mk Y)) ∘ f) ↔
    Continuous[inst✝², inst✝¹] f

Tactic:
Equiv.symm_comp_self,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
⊢ Continuous[inst✝², inst✝¹] (id ∘ f) ↔ Continuous[inst✝², inst✝¹] f
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

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

Tactic:
simp_rw [continuousOn_iff_continuous_domRestrict]
  let := isCompact_iff_compactSpace.1 hA
  exact continuous_mk_comp_iff_of_compactSpace

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
x

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
⊢ x ∈ K → ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
hf : MapsTo (⇑f) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ x ∈ ⇑f '' K, ball x V ⊆ U
g : ι
hg : ∀ x ∈ K, (f x, (F g) x) ∈ V
⊢ MapsTo (⇑(F g)) K U

Tactic:
x

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
hf : MapsTo (⇑f) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ x ∈ ⇑f '' K, ball x V ⊆ U
g : ι
hg : ∀ x ∈ K, (f x, (F g) x) ∈ V
x : α
⊢ x ∈ K → (F g) x ∈ U
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mp
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ b, ∀ᶠ (a : ι) in f, ↑(u a) ≥ b) → ∃ x, ∃ (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ ↑(u a)

Tactic:
rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, by simpa⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
L : SummationFilter γ
hf : HasProd f g L
x : α
⊢ HasProd (fun i ↦ (f i) x) (g x) L

Tactic:
by
  let ev : C(α, β) →* β := (Pi.evalMonoidHom _ x).comp coeFnMonoidHom
  exact hf.map ev (continuous_eval_const x)

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c : R
f : C(α, A)
⊢ C c * f = f * C c

Tactic:
ext x; exact Algebra.commutes' _ _

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

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

Tactic:
cases nonempty_encodable ι
  apply le_antisymm
  · refine iSup_le ?_; intro i; rw [comap_generateFrom]
    apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    choose t h1t h2t using hC
    simp_rw [eval_preimage, ← h2t]
    rw [← @iUnion_const _ ℕ _ s]
    have : Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
        Set.pi univ fun k => ⋃ j : ℕ,
        @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k := by
      ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
      by_cases h : i' = i
      · subst h; simp
      · simp [h]
    rw [this, ← iUnion_univ_pi]
    apply MeasurableSet.iUnion
    intro n; apply measurableSet_generateFrom
    -- `grind` can close the goal alone, but is slow
    apply mem_image_of_mem
    grind
  · 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.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
i : α
⊢ ∀ b ∈ {a | μ {x | a < f x} = 0}, f i ≤ b

Tactic:
intro b hb

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
i : α
b : β
hb : b ∈ {a | μ {x | a < f x} = 0}
⊢ f i ≤ b
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod [] μ)

Tactic:
rw [tprod_nil]; infer_instance

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
B : 0 < (μ.restrict s) t
⊢ d ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}

Tactic:
apply le_sInf (fun b hb ↦ ?_)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
B : 0 < (μ.restrict s) t
b : ℝ≥0∞
hb : b ∈ {a | (μ.restrict s) {x | a < f x} = 0}
⊢ d ≤ b
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
B : 0 < (μ.restrict s) t
b : ℝ≥0∞
hb : b < d
⊢ b ∉ {a | (μ.restrict s) {x | a < f x} = 0}

Tactic:
exact ne_of_gt (B.trans_le (measure_mono (fun x hx ↦ hb.trans hx)))

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)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
⊢ Measure.pi μ = μν

Tactic:
by
  have h4C : ∀ (i) (s : Set (α i)), s ∈ C i → MeasurableSet s := by
    intro i s hs; rw [← hC]; exact measurableSet_generateFrom hs
  refine
    (FiniteSpanningSetsIn.pi h3C).ext
      (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm (IsPiSystem.pi h2C) ?_
  rintro _ ⟨s, hs, rfl⟩
  rw [mem_univ_pi] at hs
  have := fun i => (h3C i).sigmaFinite
  simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]

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)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
r : ℝ
hr :
  ∀ (i : ι) (x : X i),
    (μ i) (Metric.closedBall x (2 * r)) ≤
      ↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (μ i) (Metric.closedBall x r)
hr₀ : 0 < r
⊢ ∀ (x : (i : ι) → X i),
    (Measure.pi μ) (Metric.closedBall x (2 * r)) ≤
      ↑(∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (Measure.pi μ) (Metric.closedBall x r)

Tactic:
x

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
α : ι✝ → Type u_3
inst✝⁷ : Fintype ι✝
m : (i : ι✝) → OuterMeasure (α i)
inst✝⁶ : (i : ι✝) → MeasurableSpace (α i)
μ✝ : (i : ι✝) → Measure (α i)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
r : ℝ
hr :
  ∀ (i : ι) (x : X i),
    (μ i) (Metric.closedBall x (2 * r)) ≤
      ↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (μ i) (Metric.closedBall x r)
hr₀ : 0 < r
x : (i : ι) → X i
⊢ (Measure.pi μ) (Metric.closedBall x (2 * r)) ≤
    ↑(∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (Measure.pi μ) (Metric.closedBall x r)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
⊢ essSup (fun x ↦ ‖c‖ₑ * ‖f x‖ₑ) μ = ‖c‖ₑ * essSup (fun x ↦ ‖f x‖ₑ) μ

Tactic:
ENNReal.essSup_const_mul

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : p = ∞
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

pp: case neg
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Tactic:
· exact eLpNormEssSup_mono_enorm_ae h

Goal state after:
case neg
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h✝¹ : ¬p = 0
h✝ : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ∞ ↔ q = 1

Tactic:
eq_top_iff_eq_one p q

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 ↔ q = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
hp : 1 < p
h : q = p / (p - 1)
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
by simp [field, h]

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

Goal state before:
pp: p q r : ℝ≥0
⊢ (↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r

Tactic:
by
  rw_mod_cast [Real.holderTriple_iff, holderTriple_iff]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst✝ : ENorm ε
f : α → ε
μ ν : Measure α
⊢ eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

Tactic:
eLpNorm_one_eq_lintegral_enorm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst✝ : ENorm ε
f : α → ε
μ ν : Measure α
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ eLpNorm f p (μ + ν)

Tactic:
grw [← Measure.le_add_right le_rfl]

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
⊢ 1 + p * (x / y - y / y) < (1 + (x / y - 1)) ^ p

Tactic:
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 < z - y
⊢ 1 + p * (z / y - y / y) < (1 + (z / y - 1)) ^ p

Tactic:
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 < z - y
⊢ 1 + p * (z / y - 1) < (1 + (z / y - 1)) ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
simp only [hp0, ENNReal.rpow_zero]
    filter_upwards with _
    rw [liminf_const (1 : ℝ≥0∞)]
    exact ENNReal.one_lt_top

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inr
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
convert!
    rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp using 1

Goal state after:
case e'_3
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

case e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ≥0
⊢ w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
    Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using!
    geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]

Goal state after: