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

Goal state before:
pp: k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V
inst✝⁷ : AddCommGroup V₂
inst✝⁶ : AddCommGroup V₃
inst✝⁵ : Module k V
inst✝⁴ : Module k V₂
inst✝³ : Module k V₃
inst✝² : AffineSpace V P
inst✝¹ : AffineSpace V₂ P₂
inst✝ : AffineSpace V₃ P₃
p : P
⊢ Subsingleton (Fin (1 + 0))

Tactic:
by rw [add_zero]; infer_instance

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ ⇑(p.prodEquivOfIsCompl q hpq) '' {0}ᶜ ×ˢ univ = Subtype.val '' {0}ᶜ + ↑q

Tactic:
ext
    simp [mem_add, and_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).reindex e.symm = s

Tactic:
rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * 1 + b * 1 = 1

Tactic:
mul_one,

Goal state after:
case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b * 1 = 1
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
I : Set k
n : ℕ
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I s ↔ ∀ (i : Fin (n + 1)), w i ∈ I

Tactic:
by
  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
    s.independent w' w hw' hw hww']
  exact hw'01

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✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
hn : ¬Injective fun s ↦ affineSpan k (p '' s)
⊢ False

Tactic:
rw [not_injective_iff] at hn

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
hn : ∃ a b, affineSpan k (p '' a) = affineSpan k (p '' b) ∧ a ≠ b
⊢ False
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
⊢ ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X ⊆ stdSimplex S Y

Tactic:
by
  classical
  rintro _ ⟨s, ⟨hs₀, hs₁⟩, rfl⟩
  refine ⟨fun y ↦ ?_, ?_⟩
  · rw [FunOnFinite.linearMap_apply_apply]
    exact Finset.sum_nonneg (by aesop)
  · simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]
    exact Finset.sum_fiberwise Finset.univ f s

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

Goal state before:
pp: case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a * 1 + b * 1 = 1

Tactic:
mul_one,

Goal state after:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a + b * 1 = 1
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a + b * 1 = 1

Tactic:
mul_one,

Goal state after:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a + b = 1
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
W : Type u_4
Q : Type u_5
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : AddTorsor W Q
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : IsTopologicalAddTorsor Q
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : Module R W
inst✝ : ContinuousSMul R W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : R) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : R) in 𝓝 1, ⇑(homothety x δ) '' t ⊆ s

Tactic:
Set.image_subset_iff

Goal state after:
R : Type u_1
W : Type u_4
Q : Type u_5
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : AddTorsor W Q
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : IsTopologicalAddTorsor Q
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : Module R W
inst✝ : ContinuousSMul R W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : R) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : R) in 𝓝 1, t ⊆ ⇑(homothety x δ) ⁻¹' s
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
⊢ s.closedInterior = s.interior ∪ ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
apply Set.Subset.antisymm
  · intro p hp
    obtain hp' := Set.mem_of_mem_of_subset hp s.closedInterior_subset_affineSpan
    obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'
    rw [Set.mem_union, or_iff_not_imp_left]
    intro h
    rw [affineCombination_mem_closedInterior_iff hw1] at hp
    simp_rw [affineCombination_mem_interior_iff hw1, Set.mem_Ioo] at h
    push +distrib Not at h
    obtain ⟨j, hj⟩ : ∃ j : Fin (n + 1), w j = 0 := by
      obtain ⟨i, hi | hi⟩ := h
      · exact ⟨i, le_antisymm hi (hp i).1⟩
      · have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1
        exact ⟨i + 1, hw1 _ (by simp)⟩
    refine Set.mem_iUnion.mpr ⟨j, ?_⟩
    rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1]
    exact ⟨fun k _ ↦ hp k, by simpa using hj⟩
  · refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)
    exact s.closedInterior_faceOpposite_subset_closedInterior i

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
f : ι → Set α
⊢ (closure[inst✝¹] (⋃ i, f i))ᶜ = (⋃ i, closure[inst✝¹] (f i))ᶜ

Tactic:
simpa only [← interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ 𝓟 (nhdsKer s) = 𝓝ˢ s

Tactic:
rw [← nhdsSet_nhdsKer, isOpen_nhdsKer.nhdsSet_eq]

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ (convexHull R) s

Tactic:
rw [← centerMass_neg_left]
  exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

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

Goal state before:
pp: case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
piecewise_eq_of_notMem _ _ _ hi

Goal state after:
case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected univ
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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)

Tactic:
simpa only [centerMass, h₁, inv_one, one_smul] using!
    hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem

Goal state after:
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:
rw [Finset.mem_coe] at hx

Goal state after:
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}
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U
⊢ x ∈ U

Tactic:
mul_one,

Goal state after:
case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * ‖x‖) • x ∈ U
⊢ x ∈ U
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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 : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ z '' ↑t ⊆ s

Tactic:
Set.image_subset_iff

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 : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ↑t ⊆ z ⁻¹' s
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}

Tactic:
have : Tendsto (fun x : 𝕜 × E ↦ x.1 • x.2) (𝓝 0) (𝓝 0) :=
      continuous_smul.tendsto' _ _ (zero_smul _ _)

Goal state after:
case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}
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
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

Tactic:
← uniformity_toTopologicalSpace_eq

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
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (instUniformSpace σ F 𝔖₁).toTopologicalSpace ≤ (instUniformSpace σ F 𝔖₂).toTopologicalSpace
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ Tendsto id l (𝓝 f) ↔ Tendsto id l (𝓝 f)

Tactic:
tendsto_iff_forall_isCompact_tendstoUniformlyOn,

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (id i) a) (⇑f) l K) ↔ Tendsto id l (𝓝 f)
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : CompactSpace ↑s
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ Tendsto (fun i ↦ { toFun := s.domRestrict (F i), continuous_toFun := ⋯ }) p
      (𝓝 { toFun := s.domRestrict f, continuous_toFun := ⋯ }) ↔
    TendstoUniformlyOn F f p s

Tactic:
ContinuousMap.tendsto_iff_tendstoUniformly,

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : CompactSpace ↑s
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ TendstoUniformly (fun i a ↦ { toFun := s.domRestrict (F i), continuous_toFun := ⋯ } a)
      (⇑{ toFun := s.domRestrict f, continuous_toFun := ⋯ }) p ↔
    TendstoUniformlyOn F f p s
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
⊢ Filter.Tendsto (fun p ↦ p.1 * p.2) (nhds (f, g)) (nhds ((f, g).1 * (f, g).2))

Tactic:
tendsto_iff_forall_isCompact_tendstoUniformlyOn,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (i.1 * i.2) a) (⇑((f, g).1 * (f, g).2)) (nhds (f, g)) K
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
⊢ μ.restrict t ≤ μ.restrict s

Tactic:
apply Measure.restrict_mono _ le_rfl

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 α := ⋯
A : 0 < (μ.restrict t) t
⊢ t ⊆ s
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]
  exact hq0_lt.ne'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑(f ⊓ g) a✝

Tactic:
rw [ha_inf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case insert
α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
f : ι → α →ₘ[μ] γ
a : ι
s : Finset ι
ha : a ∉ s
ih : ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)
⊢ ↑(f a * ∏ i ∈ s, f i) =ᵐ[μ] ↑(f a) * ∏ i ∈ s, ↑(f i)

Tactic:
coeFn_mul,

Goal state after:
case insert
α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
f : ι → α →ₘ[μ] γ
a : ι
s : Finset ι
ha : a ∉ s
ih : ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)
⊢ ↑(f a) * ↑(∏ i ∈ s, f i) =ᵐ[μ] ↑(f a) * ∏ i ∈ s, ↑(f i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) ≤ ∏ i, (μ i) (s i)

pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)

Tactic:
· rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
    apply OuterMeasure.pi_pi_le

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (fun a ↦ ‖g a‖ₑ ^ p) =ᵐ[μ] 0
x : α
hx : (fun a ↦ ‖g a‖ₑ ^ p) x = 0 x
⊢ ‖g x‖ₑ = 0

Tactic:
by simpa [hp, hp'] using hx

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
rw [hq_cancel, ENNReal.rpow_one]

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

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

Tactic:
mul_one,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)

Tactic:
mul_one,

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
by_cases hs' : s = 0

Goal state after:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p

case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hs' : ¬s = 0
⊢ 1 + p * s ≤ (1 + s) ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
by_cases hs' : s = 0

Goal state after:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s