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
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
⊢ ∀ (x : { x // x ≠ i1 }), f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)

Tactic:
intro 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
ι : 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
x : { x // x ≠ i1 }
⊢ f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: 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
v : V
⊢ v +ᵥ ⊤ = ⊤

Tactic:
ext; simp [pointwise_vadd_eq_map, vadd_eq_iff_eq_neg_vadd]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
⊢ p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r

Tactic:
intro x

Goal state after:
case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
⊢ x ∈ p.ball 0 (‖k‖ * r) → x ∈ k • p.ball 0 r
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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w =
    (Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun x ↦ p ↑x) fun i ↦ w ↑i

Tactic:
rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]

Goal state after:
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w = (Finset.affineCombination k s p) ((↑({x ∈ s | x ∈ s'})).indicator w)
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
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r

Tactic:
intro x

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r
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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
intro x

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✝ : Nontrivial ι
i : ι
x : k
⊢ ∃ a, (b.coord i) a = x
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₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ⇑(φ.restrict hEF)

Tactic:
intro x

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₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x : ↥E
⊢ ∀ ⦃a₂ : ↥E⦄, (φ.restrict hEF) x = (φ.restrict hEF) a₂ → x = a₂
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst✝¹, _] ⇑q
hpq : p ≤ q
⊢ Continuous[inst✝¹, _] ⇑p

Tactic:
by
  refine Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
    (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))
  rw [ball_zero_eq]
  exact isOpen_lt hq continuous_const

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (range fun x_1 ↦ (p x_1) x)
⊢ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)

Tactic:
intro x

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (range fun x_1 ↦ (p x_1) x)
x : E
⊢ BddAbove (range fun i ↦ (p i) x)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : ∃ i_1, i_1 ∈ s ∩ {i}
⊢ i ∈ s

Tactic:
← Set.nonempty_def,

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : (s ∩ {i}).Nonempty
⊢ i ∈ s
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
⊢ (affineCombination k univ s.points) (w ∘ ⇑e) ∈ Simplex.setInterior I s

Tactic:
have hw' : ∑ i, (w ∘ e) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]

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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
hw' : ∑ i, (w ∘ ⇑e) i = 1
⊢ (affineCombination k univ s.points) (w ∘ ⇑e) ∈ Simplex.setInterior I s
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (0 b) ≤ 1

Tactic:
intro x

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (0 x) ≤ 1
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝³ : Semiring S
inst✝² : PartialOrder S
X : Type u_2
inst✝¹ : Fintype X
inst✝ : IsOrderedRing S
x : ↑(stdSimplex S X)
⊢ map id x = x

Tactic:
by
  aesop

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
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : IsOrderedRing S
inst✝¹ : DecidableEq X
inst✝ : DecidableEq Y
f : X → Y
x : X
⊢ map f (vertex x) = vertex (f x)

Tactic:
by
  aesop

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'
⊢ p i -ᵥ p j = (fs'.weightedVSub p) w''

Tactic:
hs'

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
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'
⊢ ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w' = (fs'.weightedVSub p) w''
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
⊢ Function.Injective vertex

Tactic:
intro x

Goal state after:
S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
x : X
⊢ ∀ ⦃a₂ : X⦄, vertex x = vertex a₂ → x = a₂
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:
simp only [Finset.centerMass, Finset.sum_const, Finset.card_univ]

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
⊢ ↑barycenter = (Fintype.card X • 1)⁻¹ • ∑ x, 1 • Pi.single x 1
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
⊢ s.Pairwise fun x y ↦ openSegment 𝕜 x y ⊆ interior s

Tactic:
intro x

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
x : E
⊢ x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → (fun x y ↦ openSegment 𝕜 x y ⊆ interior s) x y
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s = ∅ → nhdsKer s = ∅

Tactic:
by rintro rfl; exact nhdsKer_empty

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝¹] s ∧ x ∈ s ∧ IsPathConnected s) id

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩
  have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs
  exact ⟨pathComponentIn u x, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
    isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
⊢ ∀ (x : X ⊕ Y) (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
intro x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
x : X ⊕ Y
⊢ ∀ (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
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

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
⊢ 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.LinearAlgebra.AffineSpace.Independent

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
ι : 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
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})

Tactic:
let wm : ι → k := -(w i)⁻¹ • w

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
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
wm : ι → k := -(w i)⁻¹ • w
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
⊢ ∀ (x : (i : ι) × X i) (u : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
intro x

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
x✝ y z : X✝
ι : Type u_3
F : Set X✝
inst✝² : LocallyPathConnectedSpace X✝
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
⊢ ∀ (u : Set ((i : ι) × X i)), IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
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
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
hi' : i ∈ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Goal state after:
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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
hi' : i ∉ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

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

Goal state before:
pp: case pos
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
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
hi' : i ∈ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Goal state after:
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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
hi' : i ∉ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

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✝³ : 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})
⊢ AffineIndependent k p

Tactic:
by
  classical
    intro s w hw hs
    let s' : Finset { y // y ≠ i } := s.subtype (· ≠ i)
    let p' : { y // y ≠ i } → P := fun x => p x
    by_cases his : i ∈ s ∧ w i ≠ 0
    · refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'
    · rw [not_and_or, Classical.not_not] at his
      let w' : { y // y ≠ i } → k := fun x => w x
      have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      intro j hj
      by_cases hji : j = i
      · rw [hji] at hj
        exact hji.symm ▸ his.neg_resolve_left hj
      · exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ x ∈ {x | x ≠ 2}, ![p₁, p₂, p₃] x ∈ ↑s

Tactic:
intro 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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
x : Fin 3
⊢ x ∈ {x | x ≠ 2} → ![p₁, p₂, p₃] x ∈ ↑s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : AlexandrovDiscrete X
⊢ ∀ (x : X), ∃ x_1, x_1 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_1 y

Tactic:
intro x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : AlexandrovDiscrete X
x : X
⊢ ∃ x_1, x_1 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_1 y