mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ
⊢ (p.comp f).closedBall x r = ⇑f ⁻¹' p.closedBall (f x) r

Tactic:
ext

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
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ p.ball x r = ∅

Tactic:
ext

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ x✝ ∈ p.ball x r ↔ x✝ ∈ ∅
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
x : E
r : ℝ
hr : r < 0
⊢ p.closedBall x r = ∅

Tactic:
ext

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ p.closedBall x r ↔ x✝ ∈ ∅
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₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b < r₂
⊢ 0 < r₁

Tactic:
exact hr₁.lt_or_gt.resolve_left <| ((norm_nonneg a).trans ha).not_gt

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₂₁ : (r₂ - ↑r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ r₂ - ↑r₁ ≠ 0

Tactic:
by rwa [sub_ne_zero, ne_comm]

Goal state after:
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
⊢ -p.ball x r = p.ball (-x) r

Tactic:
ext

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.ball x r ↔ x✝ ∈ p.ball (-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
⊢ -p.closedBall x r = p.closedBall (-x) r

Tactic:
ext

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.closedBall x r ↔ x✝ ∈ p.closedBall (-x) 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
⊢ v +ᵥ ⊥ = ⊥

Tactic:
ext

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
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
⊢ v +ᵥ ⊤ = ⊤

Tactic:
ext

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
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊤ ↔ x✝ ∈ ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: case e_f
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₁
⊢ f.comp ↑(AffineEquiv.constVAdd k P₁ v) = (↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f

Tactic:
ext

Goal state after:
case e_f
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₁
p✝ : P₁
⊢ (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) p✝ = ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) p✝
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:
ext

Goal state after:
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
x✝ : V
⊢ x✝ ∈ a • ⊥ ↔ x✝ ∈ ⊥
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ DistribSMul.toLinearMap k V a = a • LinearMap.id

Tactic:
ext

Goal state after:
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
x✝ : V
⊢ (DistribSMul.toLinearMap k V a) x✝ = (a • LinearMap.id) x✝
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
⊢ k • p.ball 0 r = p.ball 0 (‖k‖ * r)

Tactic:
ext

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ x✝ ∈ k • p.ball 0 r ↔ x✝ ∈ p.ball 0 (‖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
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
constructor

Goal state after:
case mp
ι : 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
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

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
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)
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:
constructor

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

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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v) →
    LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
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
p : ι → P
j : ι
q : P
⊢ q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j

Tactic:
constructor

Goal state after:
case mp
ι : 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 : ι
q : P
⊢ q ∈ affineSpan k (Set.range p) → ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j

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 : ι
q : P
⊢ (∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j) → q ∈ affineSpan k (Set.range p)
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
⊢ AffineIndependent k 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

Tactic:
constructor

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
p : ι → P
⊢ AffineIndependent k 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

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
⊢ (∀ (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) →
    AffineIndependent k p
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).coord i = b.coord (e.symm i)

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ((b.reindex e).coord i) p✝ = (b.coord (e.symm i)) p✝
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 (Set.range fun q ↦ (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)

Tactic:
apply le_antisymm
    <;> intro q hq

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.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 : ι ≃ ι'
v w : V
⊢ (fun i ↦ -(b.basisOf i).sumCoords (v + w)) = (fun i ↦ -(b.basisOf i).sumCoords v) + fun i ↦ -(b.basisOf i).sumCoords w

Tactic:
ext

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 : ι ≃ ι'
v w : V
x✝ : ι
⊢ -(b.basisOf x✝).sumCoords (v + w) = ((fun i ↦ -(b.basisOf i).sumCoords v) + fun i ↦ -(b.basisOf i).sumCoords w) 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 : ι ≃ ι'
t : k
v : V
⊢ (fun i ↦ -(b.basisOf i).sumCoords (t • v)) = (RingHom.id k) t • fun i ↦ -(b.basisOf i).sumCoords v

Tactic:
ext

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 : ι ≃ ι'
t : k
v : V
x✝ : ι
⊢ -(b.basisOf x✝).sumCoords (t • v) = ((RingHom.id k) t • fun i ↦ -(b.basisOf i).sumCoords v) 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 : ι ≃ ι'
p : P
v : V
⊢ (fun i ↦ (b.coord i) (v +ᵥ p)) =
    { toFun := fun v i ↦ -(b.basisOf i).sumCoords v, map_add' := ⋯, map_smul' := ⋯ } v +ᵥ fun i ↦ (b.coord i) p

Tactic:
ext

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 : ι ≃ ι'
p : P
v : V
x✝ : ι
⊢ (b.coord x✝) (v +ᵥ p) =
    ({ toFun := fun v i ↦ -(b.basisOf i).sumCoords v, map_add' := ⋯, map_smul' := ⋯ } v +ᵥ fun i ↦ (b.coord i) p) x✝
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
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).basisOf = b.basisOf

Tactic:
ext

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
v : V
b : AffineBasis ι k P
x✝ : ι
i✝ : { j // j ≠ x✝ }
⊢ ((v +ᵥ b).basisOf x✝) i✝ = (b.basisOf x✝) 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:
constructor

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
⊢ (∀ (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

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
⊢ (∀ (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),
      ∑ 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
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ 0 < ‖c‖ ^ (n + 1)

Tactic:
exact xεpos.trans hn.2

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 : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
x✝ : ↑(Set.range p)
⊢ Subtype.val = p ∘ ⇑fe

Tactic:
ext

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 : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
x✝¹ : ↑(Set.range p)
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ⇑fe) 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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ⇑e)
⊢ p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding

Tactic:
ext

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)
x✝ : ι'
⊢ p x✝ = (p ∘ ⇑e ∘ ⇑e.symm.toEmbedding) 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x

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: 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₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x

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, ⋯⟩)
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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x

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 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 0 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 0 2)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.face ⋯ = mkOfPoint k (s.points i)

Tactic:
ext

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ (s.face ⋯).points i✝ = (mkOfPoint k (s.points i)).points i✝
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a : E
⊢ Path.segment a a = refl a

Tactic:
ext

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a : E
x✝ : ↑I
⊢ (Path.segment a a) x✝ = (refl a) x✝
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b : E
⊢ (Path.segment a b).symm = Path.segment b a

Tactic:
ext

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b : E
x✝ : ↑I
⊢ (Path.segment a b).symm x✝ = (Path.segment b a) x✝