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

Goal state before:
pp: case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)

Tactic:
rintro ⟨s, w, hw, rfl⟩

Goal state after:
case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ 1 - (b.basisOf i).sumCoords ((v +ᵥ q) -ᵥ b i) = (-(b.basisOf i).sumCoords) v +ᵥ 1 - (b.basisOf i).sumCoords (q -ᵥ b i)

Tactic:
by
    rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
simp_rw [Seminorm.closedBall_zero_eq_preimage_closedBall] at hp

Goal state after:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
⊢ (s.face h).closedInterior ⊂ s.closedInterior

Tactic:
apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
⊢ ∃ x ∈ s.closedInterior, x ∉ (s.face h).closedInterior
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
⊢ (s.face h).closedInterior ⊂ s.closedInterior

Tactic:
obtain ⟨a, ha⟩ := Classical.not_forall.mp <| Finset.eq_univ_iff_forall.not.mp hfs
  apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr
  exact ⟨s.points a, s.point_mem_closedInterior a, fun hs ↦ ha (by simpa using hs)⟩

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ nhdsKer s ⊆ nhdsKer t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
by
  simp +contextual only [subset_nhdsKer_iff, (hasBasis_nhdsSet _).ge_iff,
    and_imp, IsOpen.mem_nhdsSet, IsOpen.nhdsKer_subset]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst✝²] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ f ⁻¹' ⋂ i, ⋂ (j : i ∈ S), U i j = ⋂₀ S

Tactic:
preimage_iInter,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst✝²] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ⋂ i, ⋂ (i_1 : i ∈ S), f ⁻¹' U i i_1 = ⋂₀ S
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})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
hw' : ∑ x ∈ s', w' x = 0
⊢ (((Finset.subtype (fun x ↦ x ≠ i) s).weightedVSub fun x ↦ p ↑x) fun x ↦ w ↑x) = 0

Tactic:
Finset.weightedVSub_subtype_eq_filter

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
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
hw' : ∑ x ∈ s', w' x = 0
⊢ ({x ∈ s | x ≠ i}.weightedVSub p) w = 0
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
h : ∀ᶠ (x : E) in 𝓝 x₀, x ∈ s → p x
⊢ ∀ᶠ (x : E) in 𝓝 x₀, x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y

Tactic:
(LocallyConvexSpace.convex_basis (𝕜 := 𝕜) x₀).eventually_iff

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
h : ∃ i, (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → p x
⊢ ∃ i, (i ∈ 𝓝 x₀ ∧ Convex 𝕜 i) ∧ ∀ ⦃x : E⦄, x ∈ id i → x ∈ s → ∀ y ∈ [x₀ -[𝕜] x], p y
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x✝ : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x✝
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x✝
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
x : E
hx₁ : x ∈ t₁
hx₂ : x ∉ t₂
⊢ w₁ x = 0

Tactic:
simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)

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

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p
⊢ p ∈ s.closedInterior

Tactic:
obtain ⟨u, w, hw, hw1, rfl⟩ := h

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior
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
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ContinuousSMul 𝕜 E

Tactic:
rw [hp.withSeminorms_eq]
  exact ModuleFilterBasis.continuousSMul _

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst✝¹⁴ : SeminormedAddCommGroup E
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜₂
inst✝⁸ : NontriviallyNormedField 𝕜₃
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : y ∈ ⇑ℓ '' s
σ : E
hσ : σ ∈ s ∧ ℓ σ = y
⊢ ‖y‖ ≤ ‖ℓ σ‖

Tactic:
rw [hσ.2]

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
⊢ (List.map (fun p ↦ p i)
      [fun k ↦ EquicontinuousAt (DFunLike.coe ∘ f) 0, fun k ↦ Equicontinuous (DFunLike.coe ∘ f), fun k ↦
        UniformEquicontinuous (DFunLike.coe ∘ f), fun i ↦
        ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, fun i ↦
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))]).TFAE

Tactic:
let _ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
⊢ (List.map (fun p ↦ p i)
      [fun k ↦ EquicontinuousAt (DFunLike.coe ∘ f) 0, fun k ↦ Equicontinuous (DFunLike.coe ∘ f), fun k ↦
        UniformEquicontinuous (DFunLike.coe ∘ f), fun i ↦
        ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, fun i ↦
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))]).TFAE
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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
rw [iInf_sigma]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, ⨅ j, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x✝ y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x

Tactic:
dif_pos hx,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x✝ y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
⊢ g x = f x * c x hx
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_cases hf : f.IsCoboundedUnder (· ≥ ·) u

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)

case neg
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf (fun i ↦ ↑(u i)) f = ↑(liminf u f)
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
eventually_map

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
⊢ limsup u f ≠ ∞
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Tactic:
eventually_map

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : Measurable g
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Tactic:
eventually_map

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : Measurable g
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : 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
| (Measure.count s)⁻¹ * Measure.count (s ∩ u) * Measure.count s * (Measure.count (s ∪ t))⁻¹ +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count t * (Measure.count (s ∪ t))⁻¹

Tactic:
mul_comm _ (Measure.count s),

Goal state after:
Ω : 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
| Measure.count s * ((Measure.count s)⁻¹ * Measure.count (s ∩ u)) * (Measure.count (s ∪ t))⁻¹ +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count t * (Measure.count (s ∪ t))⁻¹
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun i ↦ (f i).toReal
⊢ (essSup f μ).toReal = essSup (fun a ↦ (f a).toReal) μ

Tactic:
by
  obtain rfl | hμ := eq_zero_or_neZero μ
  · simp [essSup, limsup, limsSup]
  · exact ENNReal.toReal_limsup h₁

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✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.tprod (sortedUniv ι) μ) (TProd.elim' ⋯ ⁻¹' 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:
elim_preimage_pi,

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 ι) μ) (Set.tprod (sortedUniv ι) 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

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.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝¹ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
x✝ : (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none
i : Option ι
⊢ e_meas x i ∈ s i

Tactic:
rcases i

Goal state after:
case none
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝¹ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
x✝ : (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none
⊢ e_meas x none ∈ s none

case some
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝¹ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
x✝ : (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none
val✝ : ι
⊢ e_meas x (some val✝) ∈ s (some val✝)
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 : α
⊢ ↑c ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p

Tactic:
have : ¬(p < 0) := by linarith

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
by_cases h_top : p = ∞
  · simp [h_top, eLpNormEssSup_const c hμ]
  simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]

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

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
c : 𝕜
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
by simp [nnnorm_smul_le]

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

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
c : 𝕜
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
by simp [nnnorm_smul_le]

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 y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
⊢ f (a * x + b * z) ≤ a * f x + b * f z

Tactic:
have hyz : a * x + b * z < z := by linear_combination a * hxz + z * hab

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 y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x < a * x + b * z
hyz : a * x + b * z < z
⊢ f (a * x + b * z) ≤ a * f x + b * f z