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

Goal state before:
pp: case inr.refine_1
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun x ≤ q x

pp: case inr.refine_2
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun y ≤ q y

Tactic:
<;>

Goal state after:
case inr.refine_1
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun x ≤ q x

case inr.refine_2
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun y ≤ q y
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
⊢ (sSup s) x ≤ p x

Tactic:
<;>

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
⊢ (sSup s) x ≤ p x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ (sSup s) x

pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (sSup s) x ≤ p x

Tactic:
<;>

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ (sSup s) x

case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (sSup s) x ≤ p x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty

Tactic:
· obtain ⟨x, hx⟩ := hs
    obtain ⟨y, hy⟩ := ht
    use ⟨x, y⟩
    simp [mem_affineSpan, hx, hy]

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
⊢ p (f (x✝ - x)) < r ↔ p (f x✝ - f x) < r

Tactic:
map_sub

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
⊢ p (f (x✝ - x)) ≤ r ↔ p (f x✝ - f x) ≤ r

Tactic:
map_sub

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

Goal state before:
pp: M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : DistribSMul M V
inst✝ : SMulCommClass M k V
a : M
⊢ a • ⊥ = ⊥

Tactic:
by
  ext; simp [smul_eq_map, map_bot]

Goal state after:
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
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:
intro h
    have hv : ∀ v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁ ∈ s \ {p₁} := fun v =>
      (vsub_left_injective p₁).mem_set_image.1 ((vadd_vsub (v : V) p₁).symm ▸ v.property)
    let f : (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → { x : s // x ≠ ⟨p₁, hp₁⟩ } := fun x =>
      ⟨⟨(x : V) +ᵥ p₁, Set.mem_of_mem_sdiff (hv x)⟩, fun hx =>
        Set.notMem_of_mem_sdiff (hv x) (Subtype.ext_iff.1 hx)⟩
    convert!
      h.comp f fun x1 x2 hx =>
        Subtype.ext (vadd_right_cancel p₁ (Subtype.ext_iff.1 (Subtype.ext_iff.1 hx)))
    ext v
    exact (vadd_vsub (v : V) p₁).symm

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

Goal state before:
pp: case inl
ι : 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✝ : DecidableEq ι
i j : ι
h : i = j
⊢ (b.coord i) (b j) = if i = j then 1 else 0

pp: case inr
ι : 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✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ (b.coord i) (b j) = if i = j then 1 else 0

Tactic:
<;>

Goal state after:
case inl
ι : 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✝ : DecidableEq ι
i j : ι
h : i = j
⊢ (b.coord i) (b j) = if i = j then 1 else 0

case inr
ι : 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✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ (b.coord i) (b j) = if i = j then 1 else 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 (x✝ - a⁻¹ • y) ≤ r / ‖a‖

Tactic:
le_div_iff₀ (norm_pos_iff.mpr ha),

Goal state after:
𝕜 : 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 (x✝ - a⁻¹ • y) * ‖a‖ ≤ r
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
⊢ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ≤ affineSpan k (Set.range Subtype.val)

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
⊢ affineSpan k (Set.range Subtype.val) ≤ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))

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
⊢ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ≤ affineSpan k (Set.range Subtype.val)

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
⊢ affineSpan k (Set.range Subtype.val) ≤ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))
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 : q ∈ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))
⊢ q ∈ affineSpan k (Set.range Subtype.val)

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 : q ∈ affineSpan k (Set.range Subtype.val)
⊢ q ∈ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))

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 : q ∈ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))
⊢ q ∈ affineSpan k (Set.range Subtype.val)

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 : q ∈ affineSpan k (Set.range Subtype.val)
⊢ q ∈ affineSpan k (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q))
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⟩

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_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⟩

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.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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    (t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩))) μ +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩) =
      (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w_1 +ᵥ ↑⟨p, hp⟩

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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    (t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) μ +ᵥ ↑⟨p, hp⟩ =
      (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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    (t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩))) μ +ᵥ
        (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩) =
      (s_1.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) w_1 +ᵥ ↑⟨p, hp⟩

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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    (t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) μ +ᵥ ↑⟨p, hp⟩ =
      (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.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case h
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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ (t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩))) μ +ᵥ
      (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩) =
    ((t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) fun x ↦ μ x * ↑(w x)) +ᵥ ↑⟨p, hp⟩

pp: case h
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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ (t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) μ +ᵥ ↑⟨p, hp⟩ =
    ((t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
        fun x ↦ μ x * ↑(w x)⁻¹) +ᵥ
      (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)

Tactic:
<;>

Goal state after:
case h
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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ (t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩))) μ +ᵥ
      (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩) =
    ((t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) fun x ↦ μ x * ↑(w x)) +ᵥ ↑⟨p, hp⟩

case h
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
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ (t.weightedVSubOfPoint Subtype.val ↑⟨p, hp⟩) μ +ᵥ ↑⟨p, hp⟩ =
    ((t.weightedVSubOfPoint (fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) ((AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)))
        fun x ↦ μ x * ↑(w x)⁻¹) +ᵥ
      (AffineMap.lineMap p ↑⟨p, hp⟩) ↑(w ⟨p, hp⟩)
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
⊢ ContinuousAt (⇑p) 0

Tactic:
ContinuousAt,

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
⊢ Tendsto (⇑p) (𝓝 0) (𝓝 (p 0))
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓝 0 ≤ 𝓝 0

Tactic:
← @comap_norm_nhds_zero E p.toAddGroupSeminorm.toSeminormedAddGroup,

Goal state after:
case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓝 0 ≤ comap norm (𝓝 0)
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
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}

Tactic:
rw [uniformSpace_eq_of_hasBasis p hb h₁ h₂]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case «0»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case «0»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)