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

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
p p₁ p₂ : P
h : (p -ᵥ p₁) +ᵥ p₁ ∈ line[k, p₁, p₂]
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p

Tactic:
vadd_left_mem_affineSpan_pair

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
p p₁ p₂ : P
h : ∃ r, r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p
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
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  exact Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Goal state after:
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 ι
w₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) (w₁ -ᵥ w₂) = (s.weightedVSub p) (w₁ - w₂)

Tactic:
vsub_eq_sub

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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) (w₁ - w₂) = (s.weightedVSub p) (w₁ - w₂)
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 ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ (affineCombination k s p) w = (AffineMap.lineMap p₁ p₂) (∑ i ∈ s ∩ s', w i)

Tactic:
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h p₁,
    weightedVSubOfPoint_apply, ← s.sum_inter_add_sum_sdiff s', AffineMap.lineMap_apply,
    vadd_right_cancel_iff, sum_smul]
  convert! add_zero _ with i hi
  · convert! Finset.sum_const_zero with i hi
    simp [hp₁ i hi]
  · exact (hp₂ i hi).symm

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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k s = ⊤ ↔ affineSpan k (⇑e '' s) = ⊤

Tactic:
by
  refine ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, ?_⟩
  intro h
  have : s = e.symm '' e '' s := by rw [← image_comp]; simp
  rw [this]
  exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective 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_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂)) s₁ ∥ s₃
⊢ s₁ ∥ s₃

Tactic:
rcases h₂₃ with ⟨v₂₃, rfl⟩

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
s₁ : AffineSubspace k P
v₁₂ v₂₃ : V
⊢ s₁ ∥ map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case h
ι : 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, ∑ i ∈ insert i0 l.support, w i = 0 ∧ v = ((insert i0 l.support).weightedVSub p) w

Tactic:
set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef

Goal state after:
case h
ι : 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)
⊢ ∃ w, ∑ i ∈ insert i0 l.support, w i = 0 ∧ v = ((insert i0 l.support).weightedVSub p) w
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
p₁ p₂ p₃ p₄ : P
hp₁ : (p₁ -ᵥ p₃) +ᵥ p₃ ∈ line[k, p₃, p₄]
hp₂ : p₂ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]

Tactic:
vadd_left_mem_affineSpan_pair

Goal state after:
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
p₁ p₂ p₃ p₄ : P
hp₁ : ∃ r, r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
hp₂ : p₂ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
p₁ p₂ p₃ p₄ : P
hp₂ : (p₂ -ᵥ p₃) +ᵥ p₃ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]

Tactic:
vadd_left_mem_affineSpan_pair

Goal state after:
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
p₁ p₂ p₃ p₄ : P
hp₂ : ∃ r, r • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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

Tactic:
· rintro ⟨s, w, hw, rfl⟩
      exact weightedVSub_mem_vectorSpan hw p

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
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
⊢ 1 + ∑ x ∈ insert i0 s \ {i0}, Function.const ι 0 x = 1

Tactic:
simp only [Function.const_apply, Finset.sum_const_zero,
        add_zero]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]

Goal state after:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ ⊥.closedBall e r = univ
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
⊢ 𝓝 0 ≤ 𝓝 0

Tactic:
(@NormedAddGroup.nhds_zero_basis_norm_lt E
      p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb

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₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ ∀ (i' : ι), p' i' → ∃ i, 0 < i ∧ {y | ‖y‖ < i} ⊆ s i'
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent k (⇑f ∘ p)
h : Nonempty ι
⊢ AffineIndependent k p

Tactic:
obtain ⟨i⟩ := h

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent k (⇑f ∘ p)
i : ι
⊢ AffineIndependent k p
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective ⇑f
h : Nonempty ι
⊢ AffineIndependent k (⇑f ∘ p)

Tactic:
obtain ⟨i⟩ := h

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
⊢ AffineIndependent k (⇑f ∘ p)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.closedBall 0 r)

Tactic:
by
  rw [← closedBall_normSeminorm 𝕜]
  exact (normSeminorm _ _).balanced_closedBall_zero r

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
by
  cases isEmpty_or_nonempty ι with
  | inl h => rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]
  | inr h => rw [stdSimplex_unique, Metric.diam_singleton]

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

Goal state before:
pp: case pos
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₂) = ⊥
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
vectorSpan_eq_bot_iff_subsingleton

Goal state after:
case pos
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 : (p '' s₂).Subsingleton
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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₁) = ⊥
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
vectorSpan_eq_bot_iff_subsingleton

Goal state after:
case pos
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 : (p '' s₁).Subsingleton
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
ι : Type u_5
α : Type u_7
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : Module R α
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid α
inst✝ : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ s.centerMass w f ≤ s.sup' ⋯ f

Tactic:
rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]

Goal state after:
R : Type u_1
ι : Type u_5
α : Type u_7
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : Module R α
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid α
inst✝ : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ ∑ i ∈ s, w i • f i ≤ ∑ i ∈ s, w i • s.sup' ⋯ f
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi✝ : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
he' : (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) = w
i : Fin (n + 1)
hi : i ∈ fs
⊢ (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) i ∈ I

Tactic:
simp only [RelEmbedding.coe_toEmbedding, range_orderEmbOfFin, mem_coe, hi, Set.indicator_of_mem]

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi✝ : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
he' : (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) = w
i : Fin (n + 1)
hi : i ∈ fs
⊢ extend (⇑(fs.orderEmbOfFin h)) w' 0 i ∈ I
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
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s, r • w₁ x - ∑ x ∈ s, r • w₂ x - ∑ x ∈ s, w x = 0

Tactic:
←
        Finset.smul_sum,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ r • ∑ x ∈ s, w₁ x - r • ∑ x ∈ s, w₂ x - ∑ x ∈ s, w x = 0
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure ((fun θ ↦ (1 - θ) • x + θ • y) '' Ioo 0 1) = (fun θ ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1)

Tactic:
exact (image_closure_of_isCompact (isBounded_Ioo _ _).isCompact_closure <|
    Continuous.continuousOn <| by fun_prop).symm

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
t : Set α
a : α
⊢ nhdsKer {a} ⊆ t ↔ t ∈ 𝓝 a

Tactic:
by
  simp [nhdsKer_subset_iff_mem_nhdsSet]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

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

Tactic:
isOpen_nhdsKer.nhdsSet_eq

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ 𝓟 (nhdsKer s) = 𝓟 (nhdsKer s)
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
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
⊢ ∀ a ∈ {x | x ≠ i}, p a = f a

Tactic:
by simpa using congr_fun h₁

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

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

Tactic:
refine hu.rec ?_ _
      intro
      refine nhds_top_basis.to_hasBasis' ?_ ?_
      · intros
        refine ⟨Set.Ioi _, ?_, subset_rfl⟩
        simp_all
      · simp +contextual

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
p₁ p₂ : E
⊢ R ∙ (p₂ -ᵥ p₁) = R ∙ (p₂ -ᵥ p₁)

Tactic:
vsub_eq_sub

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
p₁ p₂ : E
⊢ R ∙ (p₂ - p₁) = R ∙ (p₂ - p₁)
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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)

Tactic:
b.coord_apply_combination_of_mem hi hw₁

Goal state after:
case pos
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, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
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 ∈ affineSpan R (Set.range ⇑b)
i : ι
hx : 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)
hi : i ∈ s
⊢ 0 ≤ w i

Tactic:
b.coord_apply_combination_of_mem hi hw₁

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 ∈ affineSpan R (Set.range ⇑b)
i : ι
hx : 0 ≤ w i
hi : i ∈ s
⊢ 0 ≤ w i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
⊢ ∀ (i' : ℝ), 0 < i' → ∃ i_1 ∈ p.moduleFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 i'

Tactic:
intro ε

Goal state after:
case refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
⊢ 0 < ε → ∃ i_1 ∈ p.moduleFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case inr
𝕜 : 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
hf : IsBounded p q f
s' : Finset ι'
h✝ : s'.Nonempty
⊢ ∃ C s, (s'.sup q).comp f ≤ C • s.sup p

Tactic:
choose fₛ fC hf using hf

Goal state after:
case inr
𝕜 : 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
⊢ ∃ C s, (s'.sup q).comp f ≤ C • s.sup p
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
⊢ ∀ (f : E →SL[σ₁₂] F), comap (⇑f) (cobounded F) ≤ cobounded E

Tactic:
intro ℓ
    rw [Bornology.comap_cobounded_le_iff]
    intro s hs
    obtain ⟨M, hM⟩ := hs.exists_norm_le
    rw [isBounded_iff_forall_norm_le]
    use ‖ℓ‖ * M
    intro y hy
    obtain ⟨σ, hσ⟩ := (mem_image _ _ _).1 hy
    calc ‖y‖
      _ ≤ ‖ℓ σ‖ := by rw [hσ.2]
      _ ≤ ‖ℓ‖ * ‖σ‖ := ContinuousLinearMap.le_opNorm ℓ σ
      _ ≤ ‖ℓ‖ * M := mul_le_mul (by rfl) (hM σ hσ.1) (norm_nonneg σ) (opNorm_nonneg ℓ)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case inr.refine_1
𝕜 : 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
h✝ : Nontrivial E
this : NormedSpace ℝ E
x : E
hx : x ∈ sphere 0 1
⊢ (fun x ↦ ‖f x‖₊) x ≤ ‖f‖₊

Tactic:
simpa only [mul_one] using! f.le_opNorm_of_le (mem_sphere_zero_iff_norm.1 hx).le

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
K : Set (𝐤X)
⊢ IsCompact K → IsCompact (⇑(CompactCoherentification.mk X) ⁻¹' K)

Tactic:
intro hK
    exact Equiv.image_symm_eq_preimage _ _ ▸ hK.image continuous_mk_symm

Goal state after: