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

Goal state before:
pp: ι : 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
v : V
p : ι → P
⊢ v ∈ vectorSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
constructor
    · rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
      swap
      · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]
        rintro ⟨l, _, hv⟩
        use insert i0 l.support
        set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef
        use w
        have hw : ∑ i ∈ insert i0 l.support, w i = 0 := by
          rw [hwdef]
          simp_rw [Pi.sub_apply, Finset.sum_sub_distrib,
            Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
            Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff.1]
          simp only [Function.const_apply, Finset.sum_const_zero, add_zero, sub_self]
        use hw
        have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
        change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0),
          Finset.weightedVSubOfPoint_apply, ← hv, Finsupp.linearCombination_apply,
          @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
        change (∑ i ∈ l.support, l i • _) = _
        congr with i
        by_cases h : i = i0
        · simp [h]
        · simp [hwdef, h]
      · rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
        rintro rfl
        use ∅
        simp
    · rintro ⟨s, w, hw, rfl⟩
      exact weightedVSub_mem_vectorSpan hw p

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
    map_smul_eq_mul]
  intro a ha b hb
  rw [mul_comm, mul_comm r₁]
  refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_gt.resolve_left ?_)
  exact ((apply_nonneg p b).trans hb).not_gt

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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}))) ↦ ↑v

Tactic:
h

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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔ LinearIndependent k fun (v : ↑s) ↦ ↑v
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
⊢ (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2

Tactic:
heq

Goal state after:
case mp
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
⊢ (↑s1).indicator w1 = (↑s2).indicator w2
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0

Tactic:
simp [hw1, hw2]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
⊢ (φ.restrict hEF) x = (φ.restrict hEF) y → x = y

Tactic:
h

Goal state after:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : (φ.restrict hEF) x = (φ.restrict hEF) y
⊢ x = y
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ Continuous[inst✝².toTopologicalSpace, _] ⇑p

Tactic:
rcases h₁ with ⟨r, hr⟩

Goal state after:
case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
r : ℝ
hr : p.closedBall 0 r ∈ 𝓝 0
⊢ Continuous[inst✝².toTopologicalSpace, _] ⇑p
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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent k (p ∘ ⇑f)

Tactic:
intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']

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

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι → f ∈ Icc 0 1

Tactic:
h

Goal state after:
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
⊢ f ∈ Icc 0 1
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
x y : X
⊢ vertex x = vertex y → x = y

Tactic:
h

Goal state after:
S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
x y : X
h : vertex x = vertex y
⊢ x = y
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
s : Simplex k P 0
p : P
w : Fin 1 → k
⊢ w 0 = 1 → (∀ (i : Fin 1), 0 < w i ∧ w i < 1) → ¬(affineCombination k {0} s.points) w = p

Tactic:
h

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
s : Simplex k P 0
p : P
w : Fin 1 → k
h : w 0 = 1
⊢ (∀ (i : Fin 1), 0 < w i ∧ w i < 1) → ¬(affineCombination k {0} s.points) w = p
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 : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst✝², inst✝⁵] fun δ ↦ (homothety x δ) y
a✝ : R
⊢ (homothety x a✝) y ∈ interior s → (homothety x a✝) y ∈ s

Tactic:
h

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 : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst✝², inst✝⁵] fun δ ↦ (homothety x δ) y
a✝ : R
h : (homothety x a✝) y ∈ interior s
⊢ (homothety x a✝) y ∈ 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 • x + b • y ∈ s

Tactic:
rw [h_cases, ← add_smul, hab, one_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
⊢ y ∈ s
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 : Finset E
hs : s.Nonempty
⊢ centroid R s id ∈ (convexHull R) ↑s

Tactic:
rw [s.centroid_eq_centerMass hs]

Goal state after:
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
hs : s.Nonempty
⊢ s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s
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}] a, s \ {a} ∈ 𝓝 x

Tactic:
h

Goal state after:
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
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ i ∈ s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
hw' : ∑ x ∈ s', w' x = 1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) wm ∈ affineSpan k (Set.range (p ∘ Subtype.val))

Tactic:
←
        s.affineCombination_subtype_eq_filter

Goal state after:
case pos
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
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ i ∈ s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
hw' : ∑ x ∈ s', w' x = 1
⊢ ((affineCombination k (Finset.subtype (fun x ↦ x ≠ i) s) fun i_1 ↦ p ↑i_1) fun i_1 ↦ wm ↑i_1) ∈
    affineSpan k (Set.range (p ∘ Subtype.val))
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
s : Finset E
⊢ Convex R {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

pp: case 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 : Finset E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} ⊆ (convexHull R) ↑s

Tactic:
· rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]

Goal state after:
case 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 : Finset E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} ⊆ (convexHull R) ↑s
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_eq_iInter_thickening hδ]

Goal state after:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε s)
Module: Mathlib.Analysis.Normed.Module.Convex

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

Tactic:
by
  by_cases hx : x = 0; · simpa [hx] using isConnected_univ (α := E)
  simp_rw [← exists_nonneg_left_iff_sameRay hx]
  exact isConnected_Ici.image _ (by fun_prop)

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

Goal state before:
pp: case fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ ∑ x, ∑ x_1, v x_1 • w x • f x = x

Tactic:
sum_comm (γ := ι),

Goal state after:
case fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ ∑ y, ∑ x, v y • w x • f x = x
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)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
φ' : H →ₗ[𝕜] ↑s → E := { toFun := s.domRestrict ∘ ⇑φ, map_add' := ⋯, map_smul' := ⋯ }
u : H
⊢ Bornology.IsVonNBounded 𝕜 (Set.range (φ' u))

Tactic:
simpa only [Set.image_eq_range] using! h u s hs

Goal state after:
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
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ ∀ (x : E), x ∈ (convexHull R) ↑t₁ ∧ x ∈ (convexHull R) ↑t₂ → x ∈ (convexHull R) (↑t₁ ⊓ ↑t₂)

Tactic:
Set.inf_eq_inter,

Goal state after:
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
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ ∀ (x : E), x ∈ (convexHull R) ↑t₁ ∧ x ∈ (convexHull R) ↑t₂ → x ∈ (convexHull R) (↑t₁ ∩ ↑t₂)
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
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂ ⊆ (convexHull R) (↑t₁ ⊓ ↑t₂)

Tactic:
simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']

Goal state after:
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
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ ∀ (x : E),
    ((∃ w, (∀ y ∈ t₁, 0 ≤ w y) ∧ ∑ y ∈ t₁, w y = 1 ∧ ∑ y ∈ t₁, w y • y = x) ∧
        ∃ w, (∀ y ∈ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₂, w y = 1 ∧ ∑ y ∈ t₂, w y • y = x) →
      ∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
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 ι
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₂
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
use ((s ∪ t).sup p).ball 0 (min r₁ r₂)

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₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
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
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ {x | ‖x‖ < r / (s.sup p) v} ∈ 𝓝 0

Tactic:
rw [← _root_.ball_zero_eq]

Goal state after:
case pos
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
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ Metric.ball 0 (r / (s.sup p) v) ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst✝, _] ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous[inst✝, _] ⇑(s.sup p)

Tactic:
induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs

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
⊢ Bornology.IsBounded (⇑ℓ '' s)

Tactic:
isBounded_iff_forall_norm_le

Goal state after:
𝕜 : 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
⊢ ∃ C, ∀ x ∈ ⇑ℓ '' s, ‖x‖ ≤ C
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case e'_5
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ 0 = ((q i).comp f) 0

Tactic:
exact (map_zero _).symm

Goal state after: