mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : AffineSpace V P
s : Set P
h : s.Subsingleton
⊢ vectorSpan k s = ⊥

Tactic:
rcases h.eq_empty_or_singleton with rfl | ⟨p, rfl⟩ <;> simp

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ico x y
⊢ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y

Tactic:
· obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz)
    obtain rfl | ha' := ha.eq_or_lt
    · rw [zero_add] at hab
      rw [hab, one_mul, zero_mul, zero_add] at hz
      exact (hz.2.ne rfl).elim
    · exact ⟨a, b, ha', hb, hab, rfl⟩

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y
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 : Set P
h : affineSpan k s = ⊤
⊢ vectorSpan k s = ⊤

Tactic:
rw [← direction_affineSpan, h, direction_top]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
⊢ balancedHull 𝕜 s ⊆ t

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ t
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
⊢ balancedHull 𝕜 s ⊆ balancedHull 𝕜 t

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ balancedHull 𝕜 t
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ x✝¹ • ∅ ⊆ ∅

Tactic:
smul_set_empty

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ ∅ ⊆ ∅
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ x ∈ ⇑f ⁻¹' s

Tactic:
by
  rw [mem_preimage, ← hy₂, map_smul]
  exact hs a ha (smul_mem_smul_set hy₁)

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

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s

pp: case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s

Tactic:
· rw [norm_zero, norm_le_zero_iff] at h
    simp only [h, ← image_smul, zero_smul, Subset.rfl]

Goal state after:
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ ∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ i • ∅

Tactic:
smul_set_empty

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ ∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ ∅
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ affineSpan k s ≤ ↑(Submodule.span k s)

Tactic:
intro x hx

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ affineSpan k s
⊢ x ∈ ↑(Submodule.span k s)
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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ p i -ᵥ x) '' p '' insert i (s \ {i}))

Tactic:
Set.image_insert_eq,

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
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ p i -ᵥ x) '' insert (p i) (p '' (s \ {i})))
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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ x -ᵥ p i) '' p '' insert i (s \ {i}))

Tactic:
Set.image_insert_eq,

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
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ x -ᵥ p i) '' insert (p i) (p '' (s \ {i})))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
· change (affineSpan k ((s₁ : Set P) ∪ s₂)).direction ≤ _
    rw [← mem_coe] at hp₁
    rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp₁),
      Submodule.span_le]
    rintro v ⟨p₃, hp₃, rfl⟩
    rcases hp₃ with hp₃ | hp₃
    · rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]
      use 0, Submodule.zero_mem _, p₃ -ᵥ p₁, vsub_mem_direction hp₃ hp₁
      rw [zero_add]
    · rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]
      use 0, Submodule.zero_mem _, p₃ -ᵥ p₁
      rw [and_comm, zero_add]
      use rfl
      rw [← vsub_add_vsub_cancel p₃ p₂ p₁, Submodule.mem_sup]
      use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _

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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

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 ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
by_cases h : i₁ = i₂

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
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

case neg
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 ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

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
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
⊢ centroid k s p = centroid k univ fun x ↦ ↑x

Tactic:
let f : p '' ↑s → ι := fun x => x.property.choose

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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
⊢ centroid k s p = centroid k univ fun x ↦ ↑x
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

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
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
⊢ centroid k s p = centroid k univ fun x ↦ ↑x

Tactic:
let f : p '' ↑s → ι := fun x => x.property.choose
  have hf : ∀ x, f x ∈ s ∧ p (f x) = x := fun x => x.property.choose_spec
  let f' : ps → ι := fun x => f ⟨x, hps ▸ x.property⟩
  have hf' : ∀ x, f' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩
  have hf'i : Function.Injective f' := by
    intro x y h
    rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
  let f'e : ps ↪ ι := ⟨f', hf'i⟩
  have hu : Finset.univ.map f'e = s := by
    ext x
    rw [mem_map]
    constructor
    · rintro ⟨i, _, rfl⟩
      exact (hf' i).1
    · intro hx
      use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
      refine hi _ (hf' _).1 _ hx ?_
      rw [(hf' _).2]
  rw [← hu, centroid_map]
  congr with x
  change p (f' x) = ↑x
  rw [(hf' x).2]

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 : p x < r₂
⊢ p x < ‖a‖ * r₁

Tactic:
exact hx.trans (hr.trans_le <| by gcongr)

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ (fun a ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y

Tactic:
convert! image_affine_Ioc (sub_pos_of_lt h) x 0 1 using 2

Goal state after:
case e'_2
x y : ℝ
h : x < y
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioc 0 1
⊢ a✝¹ * (y - x) + x = (y - x) * a✝¹ + x

case e'_3.e'_3
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

case e'_3.e'_4
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x
Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst✝¹ : Finite X
inst✝ : Finite Y
f : X → Y
⊢ Continuous (map f)

Tactic:
have := Fintype.ofFinite X

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst✝¹ : Finite X
inst✝ : Finite Y
f : X → Y
this : Fintype X
⊢ Continuous (map f)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
⊢ stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1 -[𝕜] Pi.single 1 1]

Tactic:
refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)
  rintro f ⟨hf₀, hf₁⟩
  rw [Fin.sum_univ_two] at hf₁
  refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
  simp

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

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
s : Simplex k P 0
p : P
⊢ (∃ w, w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points) w = p) → p = s.points 0

Tactic:
rintro ⟨w, h0, hi, rfl⟩

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
s : Simplex k P 0
w : Fin 1 → k
h0 : w 0 = 1
hi : ∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1
⊢ (affineCombination k {0} s.points) w = s.points 0
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'
⊢ (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0

Tactic:
have he' := s.independent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype
      hw hw' (fs.orderEmbOfFin h).toEmbedding he.symm

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 ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ (s.face h).closedInterior ⊆ s.closedInterior

Tactic:
intro p hp
  have hp' : p ∈ affineSpan k (Set.range s.points) :=
    Set.mem_of_mem_of_subset hp <|
      (s.face h).closedInterior_subset_affineSpan.trans <|
        affineSpan_mono k <| by simp
  obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'
  rw [affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1] at hp
  rw [affineCombination_mem_closedInterior_iff hw1]
  intro i
  by_cases hi : i ∈ fs <;> aesop

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hfs : j ∈ fs
⊢ s.points j ∈ (s.face h).closedInterior

Tactic:
obtain ⟨i, rfl⟩ : ∃ i, fs.orderEmbOfFin h i = j := range_orderEmbOfFin fs h |>.ge hfs

Goal state after:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (m + 1)
hfs : (fs.orderEmbOfFin h) i ∈ fs
⊢ s.points ((fs.orderEmbOfFin h) i) ∈ (s.face h).closedInterior
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case neg
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
⊢ (insert i t).centerMass w z ∈ s

Tactic:
· rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)

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

Goal state before:
pp: case h₁
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
⊢ (affineCombination k univ s.points) w ∈ ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
refine Set.mem_iUnion.mpr ⟨j, ?_⟩

Goal state after:
case h₁
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
⊢ (affineCombination k univ s.points) w ∈ (s.faceOpposite j).closedInterior
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
i : ι
hpi : p x i
hi : s x i ⊆ t
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t

Tactic:
exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

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

Goal state before:
pp: case inr.refine_2.hd
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
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ ⇑(Equiv.vaddConst p).symm '' insert p (⇑(Equiv.vaddConst p) '' b) = insert 0 b

Tactic:
Set.image_insert_eq,

Goal state after:
case inr.refine_2.hd
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
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm '' ⇑(Equiv.vaddConst p) '' b) = insert 0 b
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[Iio a ∪ Ioi a] a

Tactic:
inter_union_distrib_left,

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[Iio a ∪ Ioi a] a
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[<] a

Tactic:
inter_union_distrib_left,

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[<] a
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[>] a

Tactic:
inter_union_distrib_left,

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[>] a
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
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
v : ι → E
⊢ Set.range v ⊆ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
intro x hx

Goal state after:
case refine_1
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
v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
hU : U ∈ 𝓝 x
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U

Tactic:
by
    rw [nhds_pi, Filter.mem_pi] at hU
    obtain ⟨J, hJ, t, ht, htU⟩ := hU
    let K := J ∪ {i | ¬PathConnectedSpace (Z i)}
    refine ⟨K.pi fun i ↦ pathComponentIn (t i) (x i),
      set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ pathComponentIn_mem_nhds (ht i), ?_,
      fun f hf ↦ htU fun i hiJ ↦ pathComponentIn_subset (hf i (mem_union_left _ hiJ))⟩
    classical
    rw [← univ_pi_piecewise_univ]
    refine .pi fun i ↦ ?_
    by_cases hi : i ∈ K
    · rw [piecewise_eq_of_mem _ _ _ hi]
      exact isPathConnected_pathComponentIn (mem_of_mem_nhds (ht i))
    · rw [piecewise_eq_of_notMem _ _ _ hi]
      have : PathConnectedSpace (Z i) := not_not.mp (not_or.1 hi).2
      exact isPathConnected_univ

Goal state after: