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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div,

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯)) w - (s₂.weightedVSubOfPoint p (Classical.choice ⋯)) (-w) =
    (s.weightedVSub p) w

Tactic:
exact s.weightedVSub_sdiff_sub h _ _

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

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✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ AffineSubspace.map f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]
  exact image_univ_of_surjective hf

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

Goal state before:
pp: case right
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := ⋯
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) (Finsupp.onFinset s w' hwx) = ∑ i ∈ s, w i • (p i -ᵥ p i0)

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case right
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ((Finsupp.onFinset s w' hwx).sum fun i a ↦ a • (p i -ᵥ p i0)) = ∑ i ∈ s, w i • (p i -ᵥ p i0)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case right
ι : 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
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
⊢ (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = ∑ i ∈ insert i0 l.support, w i • (p i -ᵥ p i0)

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case right
ι : 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
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
⊢ (l.sum fun i a ↦ a • (p i -ᵥ p i0)) = ∑ i ∈ insert i0 l.support, w i • (p i -ᵥ p i0)
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 : ℝ
⊢ p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r

Tactic:
ball_zero_eq,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ {y | p y < r} = ⇑p ⁻¹' Metric.ball 0 r
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 : ℝ
⊢ p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r

Tactic:
by
  rw [ball_zero_eq, preimage_metric_ball]

Goal state after:
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
hs2 : (s2.weightedVSub p) f = 0
⊢ f ↑i = 0

Tactic:
exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))

Goal state after:
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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ i ∈ s with i ∈ s', w i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)

Tactic:
← Finset.sum_subtype_eq_sum_filter

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
⊢ ⇑(b.coord i) = 1

Tactic:
by
  ext q
  have hp : (range b).Subsingleton := by
    rw [← image_univ]
    apply Subsingleton.image
    apply subsingleton_of_subsingleton
  have := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
  let s : Finset ι := {i}
  have hi : i ∈ s := by simp [s]
  have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp [s]
  have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by
    simp [eq_iff_true_of_subsingleton]
  rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Metric.ball x r)

Tactic:
by
  rw [← ball_normSeminorm 𝕜]
  exact (normSeminorm 𝕜 _).absorbent_ball hx

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

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝² : Semiring 𝕜
inst✝¹ : PartialOrder 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1}

Tactic:
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_ofPred_eq]

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

Goal state before:
pp: case neg
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
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
simp only [he, false_or]

Goal state after:
case neg
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
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) → s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

pp: case mpr
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
s₁ s₂ : Set ι
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton → vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)

Tactic:
· intro h
    by_cases he : s₁ = s₂
    · simp [he]
    simp only [he, false_or]
    by_cases h₁ : s₁.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩
    by_cases h₂ : s₂.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩
    simp only [h₁, h₂, false_and]
    have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁ := by grind
    rcases hi with ⟨i, his₁, his₂⟩ | ⟨i, his₂, his₁⟩
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm

Goal state after:
case mpr
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
s₁ s₂ : Set ι
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton → vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t) ((homothety x t⁻¹) e) = e

Tactic:
simp [← AffineMap.comp_apply, ← homothety_mul, ht]

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

Goal state before:
pp: case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t⁻¹) ((homothety x t) e) = e

Tactic:
simp [← AffineMap.comp_apply, ← homothety_mul, ht]

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
v : V
hv : v ∈ Basis.ofVectorSpaceIndex k V
⊢ v ≠ 0

Tactic:
simpa [hsv] using hsv.ne_zero ⟨v, hv⟩

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
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
    (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge

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
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ᶠ (i : ι), w i • z i ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_2
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
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k s

Tactic:
rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂

Goal state after:
case inr.refine_2
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
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b) = affineSpan k 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
i : E
hi : i = x ∨ i = y
⊢ i ∈ s

Tactic:
cases hi

Goal state after:
case neg.convert_3.inl
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
h✝ : i = x
⊢ i ∈ s

case neg.convert_3.inr
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
h✝ : i = y
⊢ i ∈ s
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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ (affineCombination R s v) w ∈ (convexHull R) (Set.range v)

Tactic:
by
  rw [affineCombination_eq_centerMass hw₁]
  apply s.centerMass_mem_convexHull hw₀
  · simp [hw₁]
  · simp

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

Goal state before:
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 : Set E
⊢ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x} ⊆ (convexHull R) s

Tactic:
· rintro _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    exact t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

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
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i, w i • z i = x
⊢ ∑ i, w i • z i ∈ (convexHull R) s

Tactic:
← centerMass_eq_of_sum_1 _ _ hw₁

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : Field R
inst✝⁴ : AddCommGroup E
inst✝³ : Module R E
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i, w i • z i = x
⊢ Finset.univ.centerMass w z ∈ (convexHull R) 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
this : Tendsto (fun x ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
a : 𝕜
ha : a ∈ V
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ W}
x : α
⊢ φ (a • u) x ∈ U

Tactic:
rw [map_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 : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
a : 𝕜
ha : a ∈ V
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ W}
x : α
⊢ (a • φ u) x ∈ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
  exact AddGroupFilterBasis.nhds_zero_hasBasis _

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds' u y₀]
  exact
    ⟨fun h i => by simpa only [Finset.sup_singleton] using h {i}, fun h s ε hε =>
      (s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩

Goal state after:
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)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (E →SLᵤ[σ, 𝔖] F)

Tactic:
rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]

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)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ IsComplete (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))
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), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ‖x‖₊ ≠ 0

Tactic:
rwa [← NNReal.coe_ne_zero]

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

Goal state before:
pp: case hbasis
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

pp: case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ ∀ i ∈ p.basisSets, Convex ℝ (id i)

Tactic:
· rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
    exact FilterBasis.hasBasis _

Goal state after:
case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ ∀ i ∈ p.basisSets, Convex ℝ (id i)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕜₂
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
𝕜 : Type u_11
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝², _] ⇑p
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ ∃ p₂, Continuous[inst✝⁵, _] ⇑p₂ ∧ p ≤ p₂.comp f

Tactic:
obtain ⟨s, C, -, hqC⟩ := Seminorm.bound_comp_of_isInducing hp
    (PolynormableSpace.withSeminorms 𝕜₂ F) hf
  have := (PolynormableSpace.withSeminorms 𝕜₂ F).topologicalAddGroup
  exact ⟨_, Continuous.const_smul (continuous_finsetSup fun i _ => i.2) C, hqC⟩

Goal state after: