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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ (affineCombination k (s \ s₂) p) w -ᵥ (affineCombination k s₂ p) (-w) = (s.weightedVSub p) w

Tactic:
[

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ (affineCombination k (s \ s₂) p) w -ᵥ (affineCombination k s₂ p) (-w) = (s.weightedVSub p) w
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) b) w

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
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) b) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
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
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)

Tactic:
[

Goal state after:
case inr
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
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝

Tactic:
[

Goal state after:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i ↦ p ↑i) w

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
S : AffineSpace V P
ι : Type u_4
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i ↦ p ↑i) w
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
r : k
p : ι → P
⊢ (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) r =
    (affineCombination k s p) ((AffineMap.lineMap w₁ w₂) r)

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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
r : k
p : ι → P
⊢ (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) r =
    (affineCombination k s p) ((AffineMap.lineMap w₁ w₂) r)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (⇑e '' s) = ⊤
this : s = ⇑e.symm '' ⇑e '' s
⊢ affineSpan k s = ⊤

Tactic:
this

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✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (⇑e '' s) = ⊤
this : s = ⇑e.symm '' ⇑e '' s
⊢ affineSpan k (⇑e.symm '' ⇑e '' s) = ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0

Tactic:
[

Goal state after:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ t ∈ s, weightedVSubVSubWeights k i j t = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Tactic:
[

Goal state after:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ vectorSpan k s₁ = vectorSpan k s₂

Tactic:
[

Goal state after:
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
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ vectorSpan k s₁ = vectorSpan k s₂
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).ball e r = p.ball e r ∩ q.ball e 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, (⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)) i = 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, (⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)) i = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case right
ι : 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : w i0 • (p i0 -ᵥ p i0) = 0
⊢ v = ((insert i0 l.support).weightedVSub p) w

Tactic:
change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz

Goal state after:
case right
ι : 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
⊢ v = ((insert i0 l.support).weightedVSub p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r
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
ι : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
p : ι → V
a : G
⊢ AffineIndependent k (a • p) ↔ AffineIndependent k p

Tactic:
by
  simp +contextual [AffineIndependent,
    ← smul_comm (α := V) a, ← smul_sum, smul_eq_zero_iff_eq]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).ball x r ↔ x✝ ∈ ⇑f ⁻¹' p.ball (f x) r

Tactic:
[

Goal state after:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).ball x r ↔ x✝ ∈ ⇑f ⁻¹' p.ball (f x) r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).closedBall x r ↔ x✝ ∈ ⇑f ⁻¹' p.closedBall (f x) r

Tactic:
[

Goal state after:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).closedBall x r ↔ x✝ ∈ ⇑f ⁻¹' p.closedBall (f x) r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ (s.sup p).ball x ↑r = ⋂ i ∈ s, (p i).ball x ↑r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ (s.sup p).ball x ↑r = ⋂ i ∈ s, (p i).ball x ↑r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ (s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r

Tactic:
[

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ (s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = s.inf fun i ↦ (p i).ball x r

Tactic:
Finset.inf_eq_iInf

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = ⨅ a ∈ s, (p a).ball x r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = s.inf fun i ↦ (p i).closedBall x r

Tactic:
Finset.inf_eq_iInf

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -x ∈ p.closedBall 0 r ↔ x ∈ p.closedBall 0 r

Tactic:
simp only [mem_closedBall_zero, map_neg_eq_map]

Goal state after:
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
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
hs2 : ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), w ↑i = 0
⊢ 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
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
hs2 : ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), w ↑i = 0
⊢ w i = 0
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
⊢ (fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}) = s

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
⊢ (fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}) = s
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case neg
ι : 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)
hj : j ∉ s
⊢ (insert j s).sum w' = 1

Tactic:
[

Goal state after:
case neg
ι : 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)
hj : j ∉ s
⊢ (insert j s).sum w' = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
| affineSpan k s

Tactic:
this

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
| affineSpan k (Set.range Subtype.val)
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.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

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.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0
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✝ : Fintype ι
p : ι → P
h :
  ∀ (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
hw1 : ∑ i, w1 i = 1
hw2 : ∑ i, w2 i = 1
⊢ (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2

Tactic:
hweq

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

Tactic:
hweq

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 s1 p) w1 = (affineCombination k s2 p) w2
⊢ (↑s1).indicator w1 = (↑s2).indicator w2
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
ι : Type u_11
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
s : Finset ι
hp : ∀ i ∈ s, Continuous[inst✝, _] ⇑(p i)
⊢ Continuous[inst✝, _] fun x ↦ (FunLike.coeAddMonoidHom (Seminorm 𝕝 E) E ℝ) (∑ i ∈ s, p i) x

Tactic:
[

Goal state after:
𝕝 : Type u_6
E : Type u_7
ι : Type u_11
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
s : Finset ι
hp : ∀ i ∈ s, Continuous[inst✝, _] ⇑(p i)
⊢ Continuous[inst✝, _] fun x ↦ (FunLike.coeAddMonoidHom (Seminorm 𝕝 E) E ℝ) (∑ i ∈ s, p i) 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
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs✝ : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
i2 : ι2
h : ∃ i, f i = f i2
hs : h.choose = i2
⊢ w' (f i2) = w i2

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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs✝ : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
i2 : ι2
h : ∃ i, f i = f i2
hs : h.choose = i2
⊢ w' (f i2) = w i2
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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ⇑e)
this : p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding
⊢ AffineIndependent k p

Tactic:
this

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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ⇑e)
this : p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding
⊢ AffineIndependent k (p ∘ ⇑e ∘ ⇑e.symm.toEmbedding)