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

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : 0 < c₁
h₂ : 0 < c₂
⊢ SameRay R (c₁ • v) (c₂ • v)

pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : c₁ < 0
h₂ : c₂ < 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
· exact Or.inr (Or.inr ⟨c₂, c₁, h₂, h₁, by module⟩)

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : c₁ < 0
h₂ : c₂ < 0
⊢ SameRay R (c₁ • v) (c₂ • v)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₁
⊢ (p -ᵥ hn.some) +ᵥ hn.some ∈ s₂

Tactic:
refine vadd_mem_of_mem_direction ?_ hq2

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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₁
⊢ p -ᵥ hn.some ∈ s₂.direction
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Tactic:
balancedCore,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ ⋃₀ {t | Balanced 𝕜 t ∧ t ⊆ s} ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
he : ↑s₁ ∩ ↑s₂ = ∅
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
obtain ⟨p₁, hp₁⟩ := h1
  obtain ⟨p₂, hp₂⟩ := h2
  rw [SetLike.lt_iff_le_and_exists]
  use sup_direction_le s₁ s₂, p₂ -ᵥ p₁,
    vsub_mem_direction ((le_sup_right : s₂ ≤ s₁ ⊔ s₂) hp₂) ((le_sup_left : s₁ ≤ s₁ ⊔ s₂) hp₁)
  intro h
  rw [Submodule.mem_sup] at h
  rcases h with ⟨v₁, hv₁, v₂, hv₂, hv₁v₂⟩
  rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v₁, add_assoc, ←
    vadd_vsub_assoc, ← neg_neg v₂, add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub,
    vsub_eq_zero_iff_eq] at hv₁v₂
  refine Set.Nonempty.ne_empty ?_ he
  use v₁ +ᵥ p₁, vadd_mem_of_mem_direction hv₁ hp₁
  rw [hv₁v₂]
  exact vadd_mem_of_mem_direction (Submodule.neg_mem _ hv₂) hp₂

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
⊢ Absorbs 𝕜 V (closure[inst✝³] a)

Tactic:
filter_upwards [ha] with b ha'

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
b : 𝕜
ha' : a ⊆ b • W
⊢ closure[inst✝³] a ⊆ b • V
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x ↦ x + z) '' s)

Tactic:
by simpa only [add_comm] using hs.add_left z

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
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : Nonempty ↥s
a b : ↥s.direction
c : ↥s
⊢ (a + b) +ᵥ c = a +ᵥ b +ᵥ c

Tactic:
ext
    apply add_vadd

Goal state after:
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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂) r = (p -ᵥ p₁) +ᵥ p₁

Tactic:
← hr,

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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂) r = r • (p₂ -ᵥ p₁) +ᵥ p₁
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)

Tactic:
rw [inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr h)]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ f x ≤ ‖r‖⁻¹ * f (r • x)
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
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : ↥s → P
hf : Function.Injective f
⊢ (affineCombination k s.attach f) (w ∘ f) = (affineCombination k (image f univ) id) w

Tactic:
by
  simp [affineCombination, hf]

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 : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i = (s.weightedVSub p) w

Tactic:
← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his),

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 : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i =
    (affineCombination k (s \ {i}) p) w -ᵥ (affineCombination k {i} p) (-w)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
⊢ (⨆ p, ⇑↑p) (x + y) ≤ (⨆ p, ⇑↑p) x + (⨆ p, ⇑↑p) y

Tactic:
simp only [iSup_apply]

Goal state after:
case inr
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i, ↑i (x + y) ≤ (⨆ i, ↑i x) + ⨆ i, ↑i y
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
x : E
⊢ (⨆ p, ⇑↑p) (-x) = (⨆ p, ⇑↑p) x

Tactic:
simp only [iSup_apply]

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
x : E
⊢ ⨆ i, ↑i (-x) = ⨆ i, ↑i x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ (⨆ p, ⇑↑p) (a • x) = ‖a‖ * (⨆ p, ⇑↑p) x

Tactic:
simp only [iSup_apply]

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ‖a‖ * ⨆ i, ↑i x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case pos
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₁ ∥ s₂

Tactic:
rw [hs₁, bot_parallel_iff_eq_bot]
      exact hb.1 hs₁

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

Goal state before:
pp: case refine_2
ι : 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
hw0 : ∑ i ∈ s', w0 i = 1
hw0s : (Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = (Finset.affineCombination k s' p) (w0 + w')

Tactic:
· rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ a • p.ball 0 r₁

Tactic:
smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha),

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ p.ball 0 (‖a‖ * r₁)
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₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E →ᵃ[k] ↥F

Tactic:
refine ⟨?_, ?_, ?_⟩
  · exact fun x => ⟨φ x, hEF <| AffineSubspace.mem_map.mpr ⟨x, x.property, rfl⟩⟩
  · refine φ.linear.restrict (?_ : E.direction ≤ F.direction.comap φ.linear)
    rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
    exact AffineSubspace.direction_le hEF
  · intro p v
    simp only [Subtype.ext_iff, AffineSubspace.coe_vadd]
    apply AffineMap.map_vadd

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
ι : Type u_4
p : ι → P
⊢ AffineIndependent k p ↔
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i ∈ s1, w1 i = 1 →
        ∑ i ∈ s2, w2 i = 1 →
          (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2

Tactic:
constructor
    · intro ha s1 s2 w1 w2 hw1 hw2 heq
      ext i
      by_cases hi : i ∈ s1 ∪ s2
      · rw [← sub_eq_zero]
        rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1
        rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2
        have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
        rw [Finset.affineCombination_indicator_subset w1 p (s1.subset_union_left (s₂ := s2)),
          Finset.affineCombination_indicator_subset w2 p s1.subset_union_right,
          ← @vsub_eq_zero_iff_eq V, Finset.affineCombination_vsub] at heq
        exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi
      · simp_all
    · intro ha s w hw hs i0 hi0
      let w1 : ι → k := Function.update (Function.const ι 0) i0 1
      have hw1 : ∑ i ∈ s, w1 i = 1 := by
        rw [Finset.sum_update_of_mem hi0]
        simp only [Finset.sum_const_zero, add_zero, const_apply]
      have hw1s : s.affineCombination k p w1 = p i0 :=
        s.affineCombination_of_eq_one_of_eq_zero w1 p hi0 (Function.update_self ..)
          fun _ _ hne => Function.update_of_ne hne ..
      let w2 := w + w1
      have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]
      have hw2s : s.affineCombination k p w2 = p i0 := by
        simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
      replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
      have hws : w2 i0 - w1 i0 = 0 := by
        rw [← Finset.mem_coe] at hi0
        rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
      simpa [w2] using hws

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
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k (map e s₂) p) (extend (⇑e) w₂ 0) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
⊢ ∑ i ∈ map e s₂, extend (⇑e) w₂ 0 i = 1

Tactic:
rw [sum_map]

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
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k (map e s₂) p) (extend (⇑e) w₂ 0) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
⊢ ∑ x ∈ s₂, extend (⇑e) w₂ 0 (e x) = 1
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) ↔ i ∈ s

Tactic:
constructor
  · intro hs
    have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
    rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
  · exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)

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

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
u : ↑(stdSimplex S X)
j : X
a✝ : j ∈ Finset.univ
⊢ j ≠ i → u j = 0

Tactic:
hj

Goal state after:
S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
u : ↑(stdSimplex S X)
j : X
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ u j = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a * 1 + b * ∑ i ∈ t, wt i = 1

Tactic:
hwt,

Goal state after:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a * 1 + b * 1 = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case 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
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
w' : ι → k := fun i ↦ r * (w₁ i - w₂ i)
hr : ∀ i ∈ s, w i = w' i
⊢ r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w

Tactic:
s.weightedVSub_congr hr fun _ _ => rfl,

Goal state after:
case 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
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
w' : ι → k := fun i ↦ r * (w₁ i - w₂ i)
hr : ∀ i ∈ s, w i = w' i
⊢ r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w'
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case neg.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
j : ι
⊢ j ∈ t → z j ∈ s

Tactic:
hj

Goal state after:
case neg.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
j : ι
hj : j ∈ t
⊢ z j ∈ s
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s

Tactic:
by
  simp only [← nhdsKer_subset_iff_isOpen, Set.subset_def, mem_nhdsKer_iff_specializes, exists_imp,
    and_imp, @forall_comm (_ ⤳ _)]

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

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

Tactic:
rcases hs' with ⟨x, hx⟩

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
⊢ y ∈ interior 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
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
⊢ t.centerMass w z ∈ (convexHull R) s

Tactic:
by
  rw [← centerMass_neg_left]
  exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

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
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ (affineCombination R t p) w = t.centerMass w p

Tactic:
by
  rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
    Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]
  simp_rw [vsub_eq_sub, sub_zero]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t

Tactic:
refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩

Goal state after:
case inl.refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ pathComponentIn u (inl x)

case inl.refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

case inl.refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl x ∈ inl '' pathComponentIn (inl ⁻¹' u) x