mathlib-initiative/mathlib-tactics huggingface dataset:
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
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
⊢ i ∈ fs'

Tactic:
by

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
w : ι → R
z : ι → E
⊢ ∅.centerMass w z = 0

Tactic:
by

Goal state after:
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
I : Set k
n : ℕ
s : Simplex k P n
⊢ Simplex.setInterior I s ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
by

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 = Finset.univ.centerMass (fun x ↦ 1) fun i ↦ Pi.single i 1

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
⊢ j ∈ fs'

Tactic:
by

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
i j : ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
hne : i ≠ j
⊢ {i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
by

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
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (insert i t).centerMass w z =
    (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj✝ : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
⊢ ∑ t ∈ fs', w''' t = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 * p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
⊢ Continuous[inst✝³, inst✝³] fun a ↦ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
α : Type u_3
inst✝⁵ : Group V
inst✝⁴ : TopologicalSpace V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace P
inst✝¹ : IsTopologicalTorsor P
inst✝ : TopologicalSpace α
p : P
⊢ Continuous[inst✝⁴, inst✝²] (Equiv.constSDiv p).invFun

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj✝ : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : ∑ t ∈ fs', w''' t = 0
⊢ (fs'.weightedVSub p) w''' = 0

Tactic:
by

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
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ {i}.centerMass w z = z i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ x.1 /ₛ x.2

Tactic:
by

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
t : Finset ι
w : ι → R
z : ι → E
⊢ t.centerMass (-w) z = t.centerMass w z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
ι : Type u_5
inst✝⁹ : Field R
inst✝⁸ : Field R'
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module R E
t : Finset ι
w : ι → R
z : ι → E
c : R'
inst✝⁵ : Module R' R
inst✝⁴ : Module R' E
inst✝³ : SMulCommClass R' R R
inst✝² : IsScalarTower R' R R
inst✝¹ : SMulCommClass R R' E
inst✝ : IsScalarTower R' R E
hc : c ≠ 0
⊢ t.centerMass (c • w) z = t.centerMass w z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝⁶] fun p ↦ p.1.1 • p.2.1

Tactic:
by

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
t : Finset ι
w : ι → R
z : ι → E
hw : ∑ i ∈ t, w i = 1
⊢ t.centerMass w z = ∑ i ∈ t, w i • z i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1.2 • p.2.2

Tactic:
by

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
c : R
t : Finset ι
w : ι → R
z : ι → E
⊢ (t.centerMass w fun i ↦ c • z i) = c • t.centerMass w z

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
⊢ vectorSpan k (p '' s₁) ≠ vectorSpan k (p '' s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝⁸] fun x ↦ x.1.1 /ₛ x.2.1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun x ↦ x.1.2 /ₛ x.2.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst✝⁴ : (i : ι) → CommGroup (V i)
inst✝³ : (i : ι) → TopologicalSpace (V i)
inst✝² : (i : ι) → Torsor (V i) (P i)
inst✝¹ : (i : ι) → TopologicalSpace (P i)
inst✝ : ∀ (i : ι), IsTopologicalTorsor (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst✝¹ i] fun a ↦ (a.1 • a.2) i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst✝⁴ : (i : ι) → CommGroup (V i)
inst✝³ : (i : ι) → TopologicalSpace (V i)
inst✝² : (i : ι) → Torsor (V i) (P i)
inst✝¹ : (i : ι) → TopologicalSpace (P i)
inst✝ : ∀ (i : ι), IsTopologicalTorsor (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst✝³ i] fun a ↦ (a.1 /ₛ a.2) i

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)

Tactic:
by

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

Goal state before:
pp: k : Type u_1
V : Type u_2
V₂ : Type u_3
P : 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₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
⊢ Simplex.setInterior I (s.map f hf) = ⇑f '' Simplex.setInterior I s

Tactic:
by

Goal state after:
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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty ↥S := Nonempty.map (⇑(AffineSubspace.inclusion hS)) inferInstance
⊢ ↑(affineSpan k (Set.range s.points)) ⊆ Set.range ⇑S.subtype

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
⊢ Continuous ⇑f.linear ↔ Continuous ⇑f

Tactic:
by

Goal state after:
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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ Simplex.setInterior I (s.restrict S hS) = ⇑S.subtype ⁻¹' Simplex.setInterior I s

Tactic:
by

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 : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ ∑ i ∈ s, (a * w₁ i + b * w₂ i) = 1

Tactic:
by

Goal state after:
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
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ Pi.single i 1 i ∉ Set.Ioo 0 1

Tactic:
by

Goal state after:
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
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∉ s.interior

Tactic:
by

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) ↔ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
by

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 : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i ↦ a * w₁ i + b * w₂ i) z

Tactic:
by

Goal state after:
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
i : Fin (n + 1)
⊢ s.points i ∈ s.closedInterior

Tactic:
by

Goal state after:
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
⊢ s.interior ⊂ s.closedInterior

Tactic:
by

Goal state after:
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
n : ℕ
s : Simplex k P n
⊢ s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace P
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : Ring R
inst✝² : Module R V
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R V
⊢ Continuous fun pqt ↦ (lineMap pqt.1 pqt.2.1) pqt.2.2

Tactic:
by

Goal state after:
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
s : Simplex k P 0
⊢ s.interior = ∅

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace P
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : Ring R
inst✝² : Module R V
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R V
p q : P
⊢ Continuous ⇑(lineMap p q)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : AddTorsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalAddTorsor P
inst✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
x : X
h₁ : ContinuousAt f₁ x
h₂ : ContinuousAt f₂ x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : AddTorsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalAddTorsor P
inst✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
s : Set X
h₁ : ContinuousOn f₁ s
h₂ : ContinuousOn f₂ s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s

Tactic:
by

Goal state after:
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
s : Simplex k P 0
⊢ 1 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ 1 i ∧ 1 i ≤ 1) ∧ (affineCombination k {0} s.points) 1 = s.points 0

Tactic:
by

Goal state after:
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
s : Simplex k P 0
⊢ s.closedInterior = {s.points 0}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : AddTorsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalAddTorsor P
inst✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
h₁ : Continuous[inst✝, inst✝⁶] f₁
h₂ : Continuous[inst✝, inst✝⁶] f₂
hg : Continuous[inst✝, inst✝²] g
⊢ Continuous[inst✝, inst✝⁶] fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)

Tactic:
by

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
⊢ ∃ x ∈ t, (fun x ↦ if hx : x ∈ t then f x hx else 0) x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : CommRing R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
⊢ Continuous ⇑(homothety x t)

Tactic:
by

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
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ t.centerMass (fun j ↦ if i = j then 1 else 0) z = z i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
W : Type u_4
Q : Type u_5
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : AddTorsor W Q
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : IsTopologicalAddTorsor Q
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : Module R W
inst✝ : ContinuousSMul R W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst✝², inst✝⁵] fun δ ↦ (homothety x δ) y
⊢ (homothety x 1) y = y

Tactic:
by

Goal state after: