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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x✝¹ : R
x✝ : P₁ →ᵃ[R] V₃
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x✝¹ : P₁ →ᵃ[R] P₃
x✝ : P₁ →ᵃ[R] V₃
⊢ (e₁.arrowCongrEquiv e₂) (x✝ +ᵥ x✝¹) = (e₁.arrowCongrₗ e₂.linear) x✝ +ᵥ (e₁.arrowCongrEquiv e₂) x✝¹

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k W)).toFun (x✝¹ + x✝) =
    (e.arrowCongrEquiv (refl k W)).toFun x✝¹ + (e.arrowCongrEquiv (refl k W)).toFun x✝

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ : R
x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k W)).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (e.arrowCongrEquiv (refl k W)).toFun x✝

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹) = (congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹

Tactic:
by ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
by rw [f.map_add, f.map_smul, f.map_smul]

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

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Tactic:
rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
      div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
by rw [f.map_add, f.map_smul, f.map_smul]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
T : Set (Set α)
hT : T.Finite
⊢ Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t

Tactic:
by
  simp [Absorbs, hT]

Goal state after:
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
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Tactic:
ext v
  rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
rw [← @norm_one 𝕜] at ha

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖1‖ ≤ ‖a‖
⊢ s ⊆ a • 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
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U

Tactic:
have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using!
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕝 s

Tactic:
obtain ⟨ε, hε, hε₀⟩ : ∃ ε : ℕ → 𝕜, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ n in atTop, ε n ≠ 0 := by
    simpa only [tendsto_nhdsWithin_iff] using! exists_seq_tendsto (𝓝[≠] (0 : 𝕜))
  refine isVonNBounded_of_smul_tendsto_zero (ε := (ε · • 1)) (by simpa) fun x hx ↦ ?_
  have := h.smul_tendsto_zero (.of_forall hx) hε
  simpa only [Pi.smul_def', smul_one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x✝⁸ : E
x✝⁷ : x✝⁸ ∈ s
x✝⁶ : E
x✝⁵ : x✝⁶ ∈ s
x✝⁴ x✝³ : 𝕜
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶) ≤ x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶

Tactic:
by rw [f.map_add, f.map_smul, f.map_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x✝⁸ : E
x✝⁷ : x✝⁸ ∈ s
x✝⁶ : E
x✝⁵ : x✝⁶ ∈ s
x✝⁴ x✝³ : 𝕜
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶ ≤ f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶)

Tactic:
by rw [f.map_add, f.map_smul, f.map_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f.symm (a • f x' + b • f y') < a • x' + b • y'

Tactic:
rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • f x' + b • f y' < f (a • x' + b • y')
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • x' + b • y' < f.symm (a • f x' + b • f y')

Tactic:
rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f (a • x' + b • y') < a • f x' + b • f y'
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₂
h : affineSpan k (⇑e '' s) = ⊤
this : s = ⇑e.symm '' ⇑e '' s
⊢ affineSpan k (⇑e.symm '' ⇑e '' s) = ⊤

Tactic:
exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h

Goal state after:
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
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
univ_fin2

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
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
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
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ (s2.weightedVSubOfPoint p (p i1)) f = 0

Tactic:
Finset.weightedVSubOfPoint_insert,

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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
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
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ((map (Embedding.subtype fun x ↦ x ≠ i1) s).weightedVSubOfPoint p (p i1)) f = 0
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
p₁ : P
p : ι → P
s : Set ι
h : p₁ ∈ affineSpan k (p '' s)
⊢ ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w

Tactic:
by
  classical
  rw [Set.image_eq_range] at h
  obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
  refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
  simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
  exact fs'.affineCombination_congr (by simp) (by simp)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)

Tactic:
ext j

Goal state after:
ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
j : { j // j ≠ i }
⊢ ((b.reindex e).basisOf i) j = ((b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)) j
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
p : ι → P
j : ι
q : P
⊢ q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j

Tactic:
by
  constructor
  · intro hq
    obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
    exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
  · rintro ⟨s, w, rfl⟩
    classical
      let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
      have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
      have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
      rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
      exact affineCombination_mem_affineSpan h₁ p

Goal state after:
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 : ι
q : P
hp : (range ⇑b).Subsingleton
⊢ (b.coord i) q = 1 q

Tactic:
have := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot

Goal state after:
ι : 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 : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
⊢ (b.coord i) q = 1 q
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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
s : Finset ι
i j : ι
e : ι ≃ ι'
t : k
v : V
⊢ (fun i ↦ -(b.basisOf i).sumCoords (t • v)) = (RingHom.id k) t • fun i ↦ -(b.basisOf i).sumCoords v

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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
s : Finset ι
i j : ι
e : ι ≃ ι'
p : P
v : V
⊢ (fun i ↦ (b.coord i) (v +ᵥ p)) =
    { toFun := fun v i ↦ -(b.basisOf i).sumCoords v, map_add' := ⋯, map_smul' := ⋯ } v +ᵥ fun i ↦ (b.coord i) p

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).basisOf i = a • b.basisOf i

Tactic:
ext j

Goal state after:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
j : { j // j ≠ i }
⊢ ((a • b).basisOf i) j = (a • b.basisOf i) j
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a : E
⊢ Path.segment a a = refl a

Tactic:
by ext; simp

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

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : Fintype ι
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial 𝕜
⊢ ∀ (x : ι → 𝕜), x ∉ stdSimplex 𝕜 ι

Tactic:
by rintro f ⟨-, hf⟩; simp at hf

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)
⊢ ∀ b ∈ Finset.univ, b ≠ i → u b = 0

Tactic:
intro j _ 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.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✝³ : 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, w j = 0

Tactic:
obtain ⟨i, hi | hi⟩ := h
      · exact ⟨i, le_antisymm hi (hp i).1⟩
      · have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1
        exact ⟨i + 1, hw1 _ (by simp)⟩

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

Goal state before:
pp: case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
eventually_sup

Goal state after:
case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: 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
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : ¬(i ∈ s ∧ w i ≠ 0)
⊢ ∀ i ∈ s, w i = 0

Tactic:
rw [not_and_or, Classical.not_not] at his

Goal state after:
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
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
⊢ ∀ i ∈ s, w i = 0
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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
hs : (affineCombination k s p) w ∈ line[k, (affineCombination k s p) w₁, (affineCombination k s p) w₂]
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
⊢ SignType.sign (w i) = SignType.sign (w j)

Tactic:
rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs
  rcases hs with ⟨r, hr⟩
  rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]

Goal state after: