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

Goal state before:
pp: case e'_2.e'_6
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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
⊢ ∀ x ∈ fs₁ \ fs₂, w₁ x = 0

Tactic:
intro i hi

Goal state after:
case e'_2.e'_6
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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁ \ fs₂
⊢ w₁ i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp.refine_2
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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
⊢ ∀ i ∈ fs₁, w₁ i = (↑(fs₁ ∩ fs₂)).indicator w₁ i

Tactic:
intro i hi

Goal state after:
case mp.refine_2
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
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁
⊢ w₁ i = (↑(fs₁ ∩ fs₂)).indicator w₁ i
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))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hj : s.points j ∈ (s.face h).closedInterior
this : s.points j ∈ affineSpan k (s.points '' ↑fs)
⊢ j ∈ fs

Tactic:
simpa

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s

Tactic:
add_comm

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • s + b • interior s ⊆ interior s

Tactic:
add_comm

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • y + b • y ∈ s

Tactic:
← add_smul,

Goal state after:
case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ (a + b) • y ∈ s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case neg.convert_3
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ x_1 ∈ {x, y}, x_1 ∈ s

Tactic:
intro i hi

Goal state after:
case neg.convert_3
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i ∈ {x, y}
⊢ i ∈ s
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
⊢ s.Nontrivial → (interior s).Nonempty

Tactic:
rintro ⟨x, hx, y, hy, h⟩

Goal state after:
case mp
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
⊢ (interior s).Nonempty
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
⊢ 0 < ∑ i ∈ t, -w i

Tactic:
simpa

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

Goal state before:
pp: case inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x

Tactic:
exact eventually_bot

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

Goal state before:
pp: 𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst✝¹⁴ : Field 𝕜
inst✝¹³ : LinearOrder 𝕜
inst✝¹² : IsStrictOrderedRing 𝕜
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : OrderClosedTopology 𝕜
inst✝⁹ : CompactIccSpace 𝕜
inst✝⁸ : ContinuousAdd 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : ContinuousSMul 𝕜 V
inst✝² : AffineSpace V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
this : IsCompact (⇑↑(AffineEquiv.vaddConst 𝕜 (s.points 0)).symm '' s.closedInterior)
⊢ IsCompact (⇑(Homeomorph.vaddConst (s.points 0)).symm '' s.closedInterior)

Tactic:
simpa

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine .ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
      (fun x => fun If : Set ts × (ts → Set E) =>
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
      (fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (𝓝 x).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) fun If ↦ ⋂ i ∈ If.1, If.2 i
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : OrderTopology R
x : R
hl : IsBot x
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ Convex R s) id

Tactic:
refine hl.rec ?_ _
      intro
      refine nhds_bot_basis.to_hasBasis' ?_ ?_
      · intros
        refine ⟨Set.Iio _, ?_, .rfl⟩
        simp_all [Iio_mem_nhds, convex_Iio]
      · simp +contextual

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

Goal state before:
pp: case refine_2.refine_3
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
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ i ∈ sx.disjSum sy, Sum.elim zx zy i ∈ s

Tactic:
intro i hi

Goal state after:
case refine_2.refine_3
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
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
hi : i ∈ sx.disjSum sy
⊢ Sum.elim zx zy i ∈ s
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'

Tactic:
use x', hx', y', hy'

Goal state after:
case right
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y : E
hx : x ∈ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}

Tactic:
by
  simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]
  exact isConnected_Ioi.image _ (by fun_prop)

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 : Set E
⊢ (convexHull R) s ⊆ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t

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
s : Set E
⊢ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t ⊆ (convexHull R) s

Tactic:
· rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)

Goal state after:
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
s : Set E
⊢ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t ⊆ (convexHull R) s
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 : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
obtain ⟨p, hp, δ, hδ, hr⟩ := eventually_prod_nhds_iff.mp hr
  rw [Metric.tendsto_nhds] at hy hz
  filter_upwards [hp, hy δ hδ, hz δ hδ] with χ hp hy hz
  exact fun v hv => hr hp <| convex_iff_segment_subset.mp (convex_ball x δ) hy hz hv

Goal state after:
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
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ ∀ i ∈ s, 0 ≤ w i

Tactic:
intro i hi

Goal state after:
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
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 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 ι
v : E
U : Set E
hU : U ∈ p.basisSets
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U

Tactic:
by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  rw [hU, Filter.eventually_iff]
  simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]
  by_cases! h : 0 < (s.sup p) v
  · simp_rw [(lt_div_iff₀ h).symm]
    rw [← _root_.ball_zero_eq]
    exact Metric.ball_mem_nhds 0 (div_pos hr h)
  simp_rw [le_antisymm h (apply_nonneg _ v), mul_zero, hr]
  exact IsOpen.mem_nhds isOpen_univ (mem_univ 0)

Goal state after:
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
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ ∀ i ∈ u, w i ≤ 1

Tactic:
intro i hi

Goal state after:
𝕜 : 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
i : Fin (n + 1)
hi : i ∈ u
⊢ w i ≤ 1
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_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
⊢ ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p

Tactic:
intro i hi

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
i : ι'
hi : i ∈ s'
⊢ (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup 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
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
⊢ Absorbs R U (image2 (fun f x ↦ f x) S s)

Tactic:
filter_upwards [hS (eventually_nhds_zero_mapsTo σ hs hU)] with c hc

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}
⊢ image2 (fun f x ↦ f x) S s ⊆ c • U
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
r : ℝ
hr : 0 < r
⊢ ‖0‖ < r

Tactic:
simpa

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

Goal state before:
pp: case refine_3.refine_1
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter

Tactic:
← this

Goal state after:
case refine_3.refine_1
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ p.ball 0 ‖c⁻¹‖ ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_3.refine_2.inr
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this✝ : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
this : c • p.ball 0 1 ⊆ p.ball 0 r
⊢ p.ball 0 r ∈ 𝓝 0

Tactic:
← this

Goal state after:
case refine_3.refine_2.inr
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this✝ : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
this : c • p.ball 0 1 ⊆ p.ball 0 r
⊢ c • p.ball 0 1 ∈ 𝓝 0
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : SeminormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
this : ‖(ContinuousLinearMap.id 𝕜 E) x‖ / ‖x‖ ≤ ‖ContinuousLinearMap.id 𝕜 E‖
⊢ 1 ≤ ‖ContinuousLinearMap.id 𝕜 E‖

Tactic:
rwa [id_apply, div_self hx] at this

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
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ ‖(h ∘SL f) x‖ ≤ ‖h‖ * ‖f‖ * ‖x‖

Tactic:
rw [mul_assoc]
    exact h.le_opNorm_of_le (f.le_opNorm x)

Goal state after:
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
M : ℝ≥0∞
hM : ∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ
⊢ ‖f‖ₑ ≤ M

Tactic:
rcases eq_top_or_lt_top M with rfl | h'M

Goal state after:
case inl
𝕜 : 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
hM : ∀ (x : E), ‖f x‖ₑ ≤ ∞ * ‖x‖ₑ
⊢ ‖f‖ₑ ≤ ∞

case inr
𝕜 : 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
M : ℝ≥0∞
hM : ∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ
h'M : M < ∞
⊢ ‖f‖ₑ ≤ M
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✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
⊢ r < 1⁻¹ * ‖f x‖₊

Tactic:
simpa

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 : α → β
lc : Filter γ
g : γ → α
hf : (↑f).IsConstant
hg : Tendsto g lc l
⊢ (↑(f ∘ g)).IsConstant

Tactic:
by
  rcases hf with ⟨b, hb⟩
  exact ⟨b, hb.comp_tendsto hg⟩

Goal state after: