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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y

Tactic:
refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_pos_smul_right x hr

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
⊢ (homothety c r₁) p = q ↔ (homothety c r₂) q = p

Tactic:
obtain h' : r₂ * r₁ = 1 := mul_eq_one_comm.mp h

Goal state after:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
⊢ (homothety c r₁) p = q ↔ (homothety c r₂) q = p
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z → ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z

Tactic:
· rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    rw [hab, div_one, div_one]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ b • -(x - y) + a • (-x + z) = 0

Tactic:
hxy,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ b • -(a • (z - y)) + a • (-x + z) = 0
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
replace hpq : 0 < p + q :=
      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
    refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
    match_scalars <;> field

Goal state after:
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ {y} ⊆ segment 𝕜 x y

Tactic:
singleton_subset_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s

Tactic:
refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) ≤ affineSpan 𝕜 s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s

Tactic:
norm_zero,

Goal state after:
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ a • s ⊆ 0 • s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
⊢ (fun x ↦ a • x) y ∈ r • s

Tactic:
have h' := hy (a⁻¹ • r) h''

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
h' : y ∈ (a⁻¹ • r) • s
⊢ (fun x ↦ a • x) y ∈ r • s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ p x h

Tactic:
by
  suffices ∃ (hx : x ∈ affineSpan k s), p x hx from this.elim fun hx hc ↦ hc
  -- TODO: `induction h using affineSpan_induction` gives the error:
  -- extra targets for '@affineSpan_induction'
  -- It seems that the `induction` tactic has decided to ignore the clause
  -- `using affineSpan_induction` and use `Exists.rec` instead.
  refine affineSpan_induction h ?mem ?smul_vsub_vadd
  · exact fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩
  · exact fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩

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

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
ps : Set P
⊢ affineSpan k {p} ⊔ affineSpan k ↑(affineSpan k ps) = affineSpan k {p} ⊔ affineSpan k ps

Tactic:
affineSpan_coe

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
p : P
ps : Set P
⊢ affineSpan k {p} ⊔ affineSpan k ps = affineSpan k {p} ⊔ affineSpan k ps
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k ↑(affineSpan k ps) = affineSpan k ps

Tactic:
affineSpan_coe

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
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k ps = affineSpan k ps
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ (∀ (i : ι), Tendsto (fun x ↦ x • S) (𝓝 0) (comap (image (eval i)) (𝓝 (0 i)).smallSets)) ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets

Tactic:
tendsto_comap_iff,

Goal state after:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ (∀ (i : ι), Tendsto (image (eval i) ∘ fun x ↦ x • S) (𝓝 0) (𝓝 (0 i)).smallSets) ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_6
f : α → E
s : Set α
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ x ∈ s, ‖f x‖ ≤ r

Tactic:
simp_rw [isVonNBounded_iff', Set.forall_mem_image]

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✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤

Tactic:
rw [eq_top_iff]
  rintro ⟨x, hx⟩ -
  refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
  · exact subset_affineSpan _ _ hy
  · exact AffineSubspace.smul_vsub_vadd_mem _ _

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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
⊢ p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₂ p₁) r = p

Tactic:
Set.pair_comm,

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
p p₁ p₂ : P
⊢ p ∈ line[k, p₂, p₁] ↔ ∃ r, (AffineMap.lineMap p₂ p₁) r = p
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ ‖0‖ * f 0 = 0

Tactic:
norm_zero,

Goal state after:
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✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ 0 * f 0 = 0
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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
⊢ (s.weightedVSubOfPoint p (Classical.choice ⋯)) (w₂ +ᵥ w₁) +ᵥ Classical.choice ⋯ =
    (s.weightedVSub p) w₂ +ᵥ (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +ᵥ Classical.choice ⋯

Tactic:
vadd_vadd,

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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
⊢ (s.weightedVSubOfPoint p (Classical.choice ⋯)) (w₂ +ᵥ w₁) +ᵥ Classical.choice ⋯ =
    ((s.weightedVSub p) w₂ + (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁) +ᵥ Classical.choice ⋯
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
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
x : E
⊢ ⨅ u, p u + q (0 • x - u) = ‖0‖ * ⨅ u, p u + q (x - u)

Tactic:
norm_zero,

Goal state after:
case inl
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
x : E
⊢ ⨅ u, p u + q (0 • x - u) = 0 * ⨅ u, p u + q (x - u)
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 : ℝ
⊢ p.ball 0 (‖0‖ * r) ⊆ 0 • p.ball 0 r

Tactic:
norm_zero,

Goal state after:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 (0 * r) ⊆ 0 • p.ball 0 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 P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (AffineIndependent k fun p ↦ ↑p) ↔ LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k (fun p => p : s → P) ⟨p₁, hp₁⟩]

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: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • 1‖ * p x + ‖b • 1‖ * p y = a * p x + b * p y

Tactic:
by
      rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, p.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
by
  simp_rw [Seminorm.closedBall_zero_eq_preimage_closedBall] at hp
  rwa [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff, map_zero]

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

Tactic:
simpa only [Set.indicator_univ, Finset.coe_univ] using h _ _ w1 w2 hw1 hw2 hweq

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

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent k (⇑f ∘ p)
i : ι
⊢ AffineIndependent k p

Tactic:
affineIndependent_iff_linearIndependent_vsub k p i

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent k (⇑f ∘ p)
i : ι
⊢ LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
⊢ AffineIndependent k (⇑f ∘ p)

Tactic:
affineIndependent_iff_linearIndependent_vsub k p i

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
hai : LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
⊢ AffineIndependent k (⇑f ∘ p)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2
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 : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (Set.range (s.faceOpposite i).points)

Tactic:
rw [range_faceOpposite_points]
    rcases subsingleton_or_nontrivial k with hk | hk
    · have : Subsingleton V := Module.subsingleton k _
      have : Subsingleton P := (AddTorsor.subsingleton_iff V P).1 inferInstance
      rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (by simp)]
      simp
    · exact affineCombination_mem_affineSpan_image hw (by simpa using h) s.points

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
I : Set k
n : ℕ
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
w' : Fin (n + 1) → k
hw' : ∑ i, w' i = 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' : (affineCombination k univ s.points) w' = (affineCombination k univ s.points) w
⊢ ∀ (i : Fin (n + 1)), w i ∈ I

Tactic:
simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
    s.independent w' w hw' hw hww']

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
I : Set k
n : ℕ
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
w' : Fin (n + 1) → k
hw' : ∑ i, w' i = 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' : (affineCombination k univ s.points) w' = (affineCombination k univ s.points) w
⊢ ∀ (i : Fin (n + 1)), w' i ∈ 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✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
⊢ False

Tactic:
have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁)
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty ↥S := Nonempty.map (⇑(AffineSubspace.inclusion hS)) inferInstance
⊢ Simplex.setInterior I (s.restrict S hS) = ⇑S.subtype ⁻¹' Simplex.setInterior I s

Tactic:
← S.subtype_injective.image_injective.eq_iff,

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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty ↥S := Nonempty.map (⇑(AffineSubspace.inclusion hS)) inferInstance
⊢ ⇑S.subtype '' Simplex.setInterior I (s.restrict S hS) = ⇑S.subtype '' ⇑S.subtype ⁻¹' Simplex.setInterior I s
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✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) ↔ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
constructor
  · intro h
    by_cases he : s₁ = s₂
    · simp [he]
    simp only [he, false_or]
    by_cases h₁ : s₁.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩
    by_cases h₂ : s₂.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩
    simp only [h₁, h₂, false_and]
    have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁ := by grind
    rcases hi with ⟨i, his₁, his₂⟩ | ⟨i, his₂, his₁⟩
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm
  · intro h
    rcases h with rfl | ⟨h₁, h₂⟩
    · rfl
    · simp [h₁.image p, h₂.image p, vectorSpan_of_subsingleton]

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

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ hx : x ∈ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ : x ∈ t
hx : x ∉ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0

Tactic:
simp [hx]

Goal state after: