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

Goal state before:
pp: case a
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 : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq :
  ∃ s_1 w_1,
    q =
      (s_1.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
          w_1 +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)
⊢ ∃ s_1 w, q = (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w +ᵥ ↑⟨p, hp⟩

Tactic:
]

Goal state after:
case a
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 : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq :
  ∃ s_1 w_1,
    q =
      (s_1.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
          w_1 +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)
⊢ ∃ s_1 w, q = (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w +ᵥ ↑⟨p, hp⟩
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case a
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 : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq : ∃ s_1 w, q = (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w +ᵥ ↑⟨p, hp⟩
⊢ ∃ s_1 w_1,
    q =
      (s_1.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
          w_1 +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)

Tactic:
]

Goal state after:
case a
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 : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq : ∃ s_1 w, q = (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w +ᵥ ↑⟨p, hp⟩
⊢ ∃ s_1 w_1,
    q =
      (s_1.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
          w_1 +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x) + p (b • y) = p (a • x) + p (b • y)

Tactic:
]

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
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x ∈ s \ {i0}, const ι 0 x = 1

Tactic:
]

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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x ∈ s \ {i0}, const ι 0 x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ∑ i, (b.coord i) v • b i = v
⊢ ∑ i, (b.coord i) v • b i = v

Tactic:
]

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ∑ i, (b.coord i) v • b i = v
⊢ ∑ i, (b.coord i) v • b i = v
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: case intro
ι : 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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₂

Tactic:
]

Goal state after:
case intro
ι : 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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₂
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ a * p x + b * p y = a * p x + b * p y

Tactic:
]

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
⊢ (⇑b '' univ).Subsingleton

Tactic:
]

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
⊢ (⇑b '' univ).Subsingleton
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
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
]

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.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
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : s.sum (Function.const ι 1) = 1
hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ p (y + -x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z ↦ z + -x) x_1 < r}

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ p (y + -x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z ↦ z + -x) x_1 < r}
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
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w2 i0 - w1 i0 = 0

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w2 i0 - w1 i0 = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball 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₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
]

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
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
𝕜' : Type u_12
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedRing 𝕜'
inst✝⁶ : SMul 𝕜 𝕜'
inst✝⁵ : NormSMulClass 𝕜 𝕜'
inst✝⁴ : NormOneClass 𝕜'
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜' E
inst✝¹ : SMul 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜' E
p : Seminorm 𝕜' E
a : 𝕜
x : E
⊢ ‖a‖ * p.toFun x = ‖a‖ * p.toFun x

Tactic:
]

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 : ι ≃ ι'
x : V
b : AffineBasis ι k P
⊢ affineSpan k (x +ᵥ range ⇑b) = ⊤

Tactic:
← AffineSubspace.pointwise_vadd_span,

Goal state after:
ι : 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 : ι ≃ ι'
x : V
b : AffineBasis ι k P
⊢ x +ᵥ affineSpan k (range ⇑b) = ⊤
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 : ι ≃ ι'
x : V
b : AffineBasis ι k P
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
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
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : E) in 𝓝 0, p x ∈ Metric.closedBall 0 i

Tactic:
]

Goal state after:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : E) in 𝓝 0, p x ∈ Metric.closedBall 0 i
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✝ : Fintype ι
p : ι → P
⊢ (∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i ∈ s1, w1 i = 1 →
        ∑ i ∈ s2, w2 i = 1 →
          (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2) ↔
    ∀ (w1 w2 : ι → k),
      ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2

Tactic:
]

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✝ : Fintype ι
p : ι → P
⊢ (∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i ∈ s1, w1 i = 1 →
        ∑ i ∈ s2, w2 i = 1 →
          (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2) ↔
    ∀ (w1 w2 : ι → k),
      ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (b.basisOf i).repr (p -ᵥ b i - v) = (b.basisOf i).repr (p -ᵥ b i - v)

Tactic:
]

Goal state after:
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₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
h : AffineSubspace.map φ E = F
x : P₂
hx✝ : x ∈ F
hx : ∃ y ∈ E, φ y = x
⊢ ∃ a, (φ.restrict ⋯) a = ⟨x, hx✝⟩

Tactic:
]

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₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
h : AffineSubspace.map φ E = F
x : P₂
hx✝ : x ∈ F
hx : ∃ y ∈ E, φ y = x
⊢ ∃ a, (φ.restrict ⋯) a = ⟨x, hx✝⟩
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 : ι ≃ ι'
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : DistribMulAction G V
inst✝² : DistribMulAction G' V
inst✝¹ : SMulCommClass G k V
inst✝ : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
⊢ ⊤ = ⊤

Tactic:
]

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
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
ε : ℝ
hε : ε > 0
k : 𝕜
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
ε : ℝ
hε : ε > 0
k : 𝕜
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r ε : ℝ
hε : ε > 0
k : 𝕜
hp : p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r ε : ℝ
hε : ε > 0
k : 𝕜
hp : p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0
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✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (↑s.card)⁻¹ = (↑s.card)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ Tendsto ((fun p ↦ dist p.1 p.2) ∘ fun x ↦ (p x.1, p x.2)) (comap (fun x ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)

Tactic:
]

Goal state after:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ Tendsto ((fun p ↦ dist p.1 p.2) ∘ fun x ↦ (p x.1, p x.2)) (comap (fun x ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
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
r : ℝ
hr : r > 0
⊢ IsOpen[inst✝¹] {y | q y < r}

Tactic:
]

Goal state after:
𝕝 : 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
r : ℝ
hr : r > 0
⊢ IsOpen[inst✝¹] {y | q y < r}
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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
⊢ ∑ i ∈ s1, w1 i = 1

Tactic:
]

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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
⊢ ∑ i ∈ s1, w1 i = 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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
hw1' : ∑ i, (↑s1).indicator w1 i = 1
⊢ ∑ i ∈ s2, w2 i = 1

Tactic:
]

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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
hw1' : ∑ i, (↑s1).indicator w1 i = 1
⊢ ∑ i ∈ s2, w2 i = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mpr
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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k univ p) ((↑s1).indicator w1) = (affineCombination k univ p) ((↑s2).indicator w2)
hw1' : ∑ i, (↑s1).indicator w1 i = 1
hw2' : ∑ i, (↑s2).indicator w2 i = 1
⊢ (↑s1).indicator w1 = (↑s2).indicator w2

Tactic:
]

Goal state after:
case mpr
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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k univ p) ((↑s1).indicator w1) = (affineCombination k univ p) ((↑s2).indicator w2)
hw1' : ∑ i, (↑s1).indicator w1 i = 1
hw2' : ∑ i, (↑s2).indicator w2 i = 1
⊢ (↑s1).indicator w1 = (↑s2).indicator w2