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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
y : E
⊢ y ∈ interior (closure s) → y ∈ interior s

Tactic:
hy

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
y : E
hy : y ∈ interior (closure s)
⊢ y ∈ interior s
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
⊢ y ∈ closure s → y ∈ ⇑(homothety x t) '' interior s

Tactic:
hy

Goal state after:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
⊢ y ∈ ⇑(homothety x t) '' interior s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x y : X
⊢ y ∈ pathComponentIn F x → pathComponentIn F x ∈ 𝓝 y

Tactic:
hy

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x y : X
hy : y ∈ pathComponentIn F x
⊢ pathComponentIn F x ∈ 𝓝 y
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
⊢ f ⁻¹' pathComponentIn u y ∈ 𝓝 x

Tactic:
have hx' := preimage_mono pathComponentIn_subset hx

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ f ⁻¹' pathComponentIn u y ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
⊢ LocallyPathConnectedSpace Y

Tactic:
let _ := TopologicalSpace.coinduced f ‹_›; have hf : Continuous f := continuous_coinduced_rng
  refine locallyPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
    isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_
  have hx' := preimage_mono pathComponentIn_subset hx
  refine mem_nhds_iff.mpr ⟨pathComponentIn (f ⁻¹' u) x, ?_,
    (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩
  rw [← image_subset_iff, ← pathComponentIn_congr hx]
  exact ((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn
    ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
    (image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f

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✝ : AlexandrovDiscrete X
x y : X
⊢ y ⤳ x → JoinedIn (nhdsKer {x}) x y

Tactic:
hy

Goal state after:
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✝ : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) x y
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Field 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : ZeroLEOneClass 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst✝³] t
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
let : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
  rw [← uniformity_eq_comap_nhds_zero] at this
  rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
  refine ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
    subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩
  simp_rw [← iUnion_add_left_image, image_add_left]
  simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
  exact hV

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
⊢ dist (y χ) x < δ → dist (z χ) x < δ → ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
hy

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy✝ : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
χ : α
hp : p χ
hy : dist (y χ) x < δ
⊢ dist (z χ) x < δ → ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: 𝕜 : 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✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
⊢ ContinuousSMul 𝕜 H

Tactic:
refine continuousSMul_iInf fun s ↦ continuousSMul_iInf fun hs ↦ ?_

Goal state after:
𝕜 : 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✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousSMul 𝕜 H
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case 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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x}

Tactic:
· have hx' : x ∈ affineSpan R (range b) := by
      rw [b.tot]
      exact AffineSubspace.mem_top R E x
    obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
    refine ⟨s, w, ?_, hw₁, rfl⟩
    intro i hi
    specialize hx i
    rw [b.coord_apply_combination_of_mem hi hw₁] at hx
    exact hx

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

Goal state before:
pp: case refine_1.inr
𝕜 : 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
i₀ : ι
hi₀ : i₀ ∈ t
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
intro h_eq

Goal state after:
case refine_1.inr
𝕜 : 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
i₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
⊢ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ (s.sup p).ball 0 r₁ ∩ (t.sup p).ball 0 r₂

Tactic:
ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),

Goal state after:
case h
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂) ⊆ (s.sup p).ball 0 r₁ ∩ (t.sup p).ball 0 r₂
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : 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
⊢ (∃ 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:
constructor <;> intro 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
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

case mpr
𝕜 : 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 : p ∈ s.closedInterior
⊢ ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p
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
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Tactic:
rw [instTopologicalSpace]

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
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
𝕜 : 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 ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ (p i) x < I.sup' hI r

Tactic:
refine lt_of_lt_of_le (h i x hx) ?_

Goal state after:
case pos
𝕜 : 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 ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ r i ≤ I.sup' hI r
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case h
𝕜 : 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
⊢ y ∈ ⇑ℓ '' s → ‖y‖ ≤ ‖ℓ‖ * M

Tactic:
hy

Goal state after:
case h
𝕜 : 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
⊢ ‖y‖ ≤ ‖ℓ‖ * M
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x : E
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
gcongr; apply le_max_left

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
b : β
hb : f =ᶠ[l] fun x ↦ b
⊢ (↑(g ∘ f)).IsConstant

Tactic:
exact ⟨g b, hb.fun_comp g⟩

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
⊢ TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK

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
⊢ TendstoLocallyUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ univ ∩ S = S

Tactic:
univ_inter

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'

pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'

Tactic:
· subst h; simp

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'
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 : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
i : α
hi : (u i).toReal ≤ x
⊢ 0 ≤ x

Tactic:
exact toReal_nonneg.trans hi

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ Measure.count[t | {ω}] = if ω ∈ t then 1 else 0

Tactic:
cond_apply (measurableSet_singleton ω),

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ (Measure.count {ω})⁻¹ * Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #⋯.toFinset = #hsf.toFinset
this : s ∩ t = s
⊢ s ⊆ t

Tactic:
exact this ▸ fun x hx => hx.2

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = 0

Tactic:
uniformOn_eq_zero_iff hs,

Goal state after:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ s ∩ (t ∩ u) = ∅
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

Tactic:
simp [h0, ENNReal.zero_rpow_of_pos hq_pos]

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

Goal state before:
pp: case pos
α : 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:
simp only [hp_top, eLpNorm_exponent_top, ENNReal.top_mul', hq_pos.not_ge,
      ENNReal.ofReal_eq_zero, if_false, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Goal state after:
case pos
α : 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 = ∞
⊢ essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
← neg_div_neg_eq

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)

Tactic:
← neg_div_neg_eq

Goal state after:
case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : y < a
⊢ -(f y - f a) / -(y - a) = (f a - f y) / (a - y)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

Tactic:
← neg_div_neg_eq

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
hya : a < y
⊢ -(f x - f a) / -(x - a) = (f a - f x) / (a - x)