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

Goal state before:
pp: case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : (v₁ +ᵥ p₁) -ᵥ p₂ + - -v₂ = 0
⊢ False

Tactic:
← sub_eq_add_neg,

Goal state after:
case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : (v₁ +ᵥ p₁) -ᵥ p₂ - -v₂ = 0
⊢ False
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✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (x +ᵥ s)

Tactic:
← singleton_vadd

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 ({x} +ᵥ s)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
by
  rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]

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
S : AffineSpace V P
p : P
⊢ ↑(affineSpan k {p}) = {p}

Tactic:
ext x

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
p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}
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
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s

Tactic:
simp [hp]

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
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : {p} = ↑⊤
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
AffineSubspace.top_coe,

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
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : {p} = univ
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
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
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
⊢ Subsingleton P

Tactic:
by
  obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
  have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
  rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂
  exact subsingleton_of_univ_subsingleton h₂

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (-f)

Tactic:
· rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
    rw [← neg_lt_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy hxy ha hb hab

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
⊢ s.sup (C • p) = C • s.sup p

Tactic:
ext x

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ (s.sup (C • p)) x = (C • s.sup p) x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)

Tactic:
simp [vectorSpan_def, f.image_vsub_image]

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 ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ (affineCombination k (s \ s₂) p) w -ᵥ (affineCombination k s₂ p) (-w) = (s.weightedVSub p) w

Tactic:
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
  exact s.weightedVSub_sdiff_sub 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
ι : 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 ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
⊢ map f'e univ = s

Tactic:
ext x

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 ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ map f'e univ ↔ x ∈ s
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ⇑p ⁻¹' Metric.ball 0 r = {x | p x < r}

Tactic:
ext x

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | p x < r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ⇑p ⁻¹' Metric.closedBall 0 r = {x | p x ≤ r}

Tactic:
ext x

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.closedBall 0 r ↔ x ∈ {x | p x ≤ r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r

Tactic:
closedBall_zero_eq,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ {y | p y ≤ r} = ⇑p ⁻¹' Metric.closedBall 0 r
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: 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
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ↑r₁ = r₂
⊢ p₆ -ᵥ p₄ = ↑r₁ • (p₃ -ᵥ p₁)

Tactic:
← vsub_add_vsub_cancel p₆ p₅ p₄,

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
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ↑r₁ = r₂
⊢ p₆ -ᵥ p₅ + (p₅ -ᵥ p₄) = ↑r₁ • (p₃ -ᵥ p₁)
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
ha : IsUnit a
⊢ a • ⊤ = ⊤

Tactic:
ext x

Goal state after:
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
ha : IsUnit a
x : V
⊢ x ∈ a • ⊤ ↔ x ∈ ⊤
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
𝕜 : 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✝ : Nonempty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
ext x

Goal state after:
case inr
𝕜 : 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✝ : Nonempty ι
x : E
⊢ x ∈ (⨆ i, p i).closedBall e r ↔ x ∈ ⋂ i, (p i).closedBall e r
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: case refine_2
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.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]

Goal state after:
case refine_2
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
⊢ (AffineSubspace.map φ E).direction ≤ F.direction
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₂
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]

Goal state after:
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₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction
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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
⊢ (fs'.weightedVSub p) w' = (fs.weightedVSub (p ∘ ⇑f)) w

Tactic:
Finset.weightedVSub_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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
⊢ (fs.weightedVSub (p ∘ ⇑f)) (w' ∘ ⇑f) = (fs.weightedVSub (p ∘ ⇑f)) w
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1) = ![p₁, p₂, p₃]

Tactic:
ext x

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) x = ![p₁, p₂, p₃] x
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2) = ![p₁, p₂, p₃]

Tactic:
ext x

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₂, p₃] x
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2) = ![p₁, p₂, p₃]

Tactic:
ext x

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) x = ![p₁, p₂, p₃] x
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)
i : ι
⊢ AffineIndependent k p

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k p i]

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 : ι
⊢ LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ IsClosed (stdSimplex 𝕜 ι)

Tactic:
rw [stdSimplex_eq_inter]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ IsClosed ((⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f 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
⊢ Injective fun s ↦ affineSpan k (p '' s)

Tactic:
by_contra hn
  rw [not_injective_iff] at hn
  obtain ⟨s₁, s₂, hs₁₂, hne⟩ := hn
  apply hne
  ext i
  simp_rw [← ha.mem_affineSpan_iff, hs₁₂]

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

Goal state before:
pp: X : Type u_2
inst✝⁵ : Fintype X
𝕜 : Type u_5
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : Nonempty X
inst✝ : DecidableEq X
⊢ ↑barycenter = (Fintype.card X • 1)⁻¹ • ∑ x, 1 • Pi.single x 1

Tactic:
ext x

Goal state after:
X : Type u_2
inst✝⁵ : Fintype X
𝕜 : Type u_5
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : Nonempty X
inst✝ : DecidableEq X
x : X
⊢ ↑barycenter x = ((Fintype.card X • 1)⁻¹ • ∑ x, 1 • Pi.single x 1) x
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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
⊢ ∑ x ∈ s, a • ws x • zs x + ∑ x ∈ t, b • wt x • zt x =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)

Tactic:
←
    Finset.sum_sumElim,

Goal state after:
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
⊢ ∑ x ∈ s.disjSum t, Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) x =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)
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
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ t.centerMass w z = t'.centerMass w' z'

Tactic:
rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • ∑ i ∈ t with w i ≠ 0, w i • z i =
    (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ • ∑ i ∈ t' with w' i ≠ 0, w' i • z' i
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case insert
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
⊢ (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    0 < ∑ i ∈ insert i t, w i → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s

Tactic:
intro h₀ hpos hmem

Goal state after:
case insert
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 < ∑ i ∈ insert i t, w i
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
⊢ (insert i t).centerMass w z ∈ s
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✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
hs : s.points a ∈ (s.face h).closedInterior
⊢ a ∈ fs

Tactic:
simpa using hs

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s

Tactic:
rw [isOpen_interior.add_closure (b • s)]

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
⊢ (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s

Tactic:
classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · 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.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✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
⊢ StrictConvex 𝕜 s

Tactic:
refine strictConvex_iff_openSegment_subset.2 ?_

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✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
⊢ s.Pairwise fun x y ↦ openSegment 𝕜 x y ⊆ interior s
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ∈ nhdsKer {y} ↔ x ⤳ y

Tactic:
by
  rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_ofPred]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Sort u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
⊢ nhdsKer (⋃ i, s i) = ⋃ i, nhdsKer (s i)

Tactic:
by
  simp only [nhdsKer, nhdsSet_iUnion, ker_iSup]

Goal state after: