mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ 0 • p.ball 0 r

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ 0 • p.ball 0 r
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
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction

Tactic:
]

Goal state after:
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
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s

Tactic:
]

Goal state after:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s
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
⊢ ∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x = 0

Tactic:
]

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
⊢ ∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x = 0
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
x : E
⊢ p x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x

Tactic:
]

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
⊢ p x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x
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
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0

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
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_1
𝕜 : 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
hx : p x < ‖k‖ * r
⊢ p x < ‖k‖ * r

Tactic:
]

Goal state after:
case inr.refine_1
𝕜 : 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
hx : p x < ‖k‖ * r
⊢ p x < ‖k‖ * 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 ∈ affineSpan k (Set.range fun x ↦ p ↑x)

Tactic:
]

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 ∈ affineSpan k (Set.range fun x ↦ p ↑x)
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✝ e : ι ≃ ι'
⊢ affineSpan k (range ⇑b) = ⊤

Tactic:
]

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✝ e : ι ≃ ι'
⊢ affineSpan k (range ⇑b) = ⊤
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_2
𝕜 : 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
hx : p x < ‖k‖ * r
⊢ x = x

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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)

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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)
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 : k ≠ 0
x✝ : E
⊢ p x✝ < ‖k‖ * r ↔ p x✝ < ‖k‖ * r

Tactic:
]

Goal state after:
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 s p) ((↑({x ∈ s | x ∈ s'})).indicator w)

Tactic:
]

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.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 : ι ≃ ι'
i : ι
this : Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = vectorSpan k (range ⇑b)
⊢ ⊤ ≤ ⊤

Tactic:
]

Goal state after:
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 : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x ↦ k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x ↦ k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r
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 : ℝ
x y : E
hy : p y ≤ r
h : (fun x ↦ k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : p y ≤ r
h : (fun x ↦ k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r
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 : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = Submodule.span k ((fun x ↦ x -ᵥ b i) '' ⇑b '' (univ \ {i}))

Tactic:
]

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 : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = Submodule.span k ((fun x ↦ x -ᵥ b i) '' ⇑b '' (univ \ {i}))
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‖
x : E
⊢ p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Tactic:
]

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
⊢ p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = 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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v

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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : 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
hx : p x ≤ ‖k‖ * r
⊢ p x ≤ ‖k‖ * r

Tactic:
]

Goal state after:
case refine_1
𝕜 : 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
hx : p x ≤ ‖k‖ * r
⊢ p x ≤ ‖k‖ * 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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}))) ↦ ↑v

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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}))) ↦ ↑v
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : 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
hx : p x ≤ ‖k‖ * r
⊢ x = x

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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
h : (fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}) = s
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔ LinearIndependent k fun (v : ↑s) ↦ ↑v

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 : ι ≃ ι'
i : ι
q : P
v : V
⊢ 1 - (b.basisOf i).sumCoords (q -ᵥ b i) + -(b.basisOf i).sumCoords v =
    1 - (b.basisOf i).sumCoords (q -ᵥ b i) + -(b.basisOf i).sumCoords v

Tactic:
]

Goal state after:
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
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ p x < ‖a‖ * r₁

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ p x < ‖a‖ * r₁
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
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ p x < ‖a‖ * r₁

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ p x < ‖a‖ * 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
i j : ι
h : i ≠ j
⊢ 0 = 0

Tactic:
]

Goal state after:
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
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y < r - p x
⊢ y ∈ p.ball x r

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y < r - p x
⊢ y ∈ p.ball x r
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
]

Goal state after:
case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y ≤ r - p x
⊢ y ∈ p.closedBall x r

Tactic:
]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y ≤ r - p x
⊢ y ∈ p.closedBall x r
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
]

Goal state after:
case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
]

Goal state after:
case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) < r ↔ p (a • x✝ - y) < r

Tactic:
]

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

Goal state before:
pp: case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (Finset.affineCombination k (insert j s) p) w' ∈ affineSpan k (Set.range p)

Tactic:
]

Goal state after:
case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (Finset.affineCombination k (insert j s) p) w' ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : ((s1 ∪ s2).weightedVSub p) ((↑s1).indicator w1 - (↑s2).indicator w2) = 0
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
]

Goal state after:
case pos
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 : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : ((s1 ∪ s2).weightedVSub p) ((↑s1).indicator w1 - (↑s2).indicator w2) = 0
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) ≤ r ↔ p (a • x✝ - y) ≤ r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : 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✝ : IsEmpty ι
⊢ ⊥.closedBall e r = univ

Tactic:
]

Goal state after:
case inl
𝕜 : 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✝ : IsEmpty ι
⊢ ⊥.closedBall e r = univ
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✝ : Fintype ι
q : P
⊢ q ∈ ⊤

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✝ : Fintype ι
q : P
⊢ q ∈ ⊤