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

Goal state before:
pp: case refine_1
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
h1 : (homothety c r₁) p = q
⊢ (homothety c r₂) q = p

pp: case refine_2
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
h1 : (homothety c r₂) q = p
⊢ (homothety c r₁) p = q

Tactic:
all_goals
    rw [← h1, ← homothety_mul_apply]
    simp [h, h']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
Q : AffineSubspace 𝕜 E
x : E
hx : x ∈ ↑Q
y : E
hy : y ∈ ↑Q
a b : 𝕜
x✝¹ : 0 ≤ a
x✝ : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑Q

Tactic:
by simpa [Convex.combo_eq_smul_sub_add hab] using! Q.2 _ hy hx hx

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s = ∅

Tactic:
rw [← Set.subset_empty_iff, ← h]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s

Tactic:
exact (segment_subset_Icc hyx).trans (hs.out hy hx)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : 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
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b‖⁻¹ * ‖a‖ ≤ 1

Tactic:
← div_eq_inv_mul

Goal state after:
𝕜 : 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
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖a‖ / ‖b‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : 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
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a‖⁻¹ * ‖b‖ ≤ 1

Tactic:
← div_eq_inv_mul

Goal state after:
𝕜 : 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
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖b‖ / ‖a‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddZeroClass E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : U ∈ 𝓝 0
V : Set E
hVo : IsOpen[inst✝²] V
hV : 0 ∈ V
hVU : V + V ⊆ U
⊢ Absorbs 𝕜 U (s + t)

Tactic:
exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

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

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_5
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
⊢ ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → _root_.id (a • x + b • y) ≤ a • _root_.id x + b • _root_.id y

Tactic:
intros

Goal state after:
𝕜 : Type u_1
β : Type u_5
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ _root_.id (a✝³ • x✝ + b✝ • y✝) ≤ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_5
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
⊢ ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • _root_.id x + b • _root_.id y ≤ _root_.id (a • x + b • y)

Tactic:
intros

Goal state after:
𝕜 : Type u_1
β : Type u_5
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝ ≤ _root_.id (a✝³ • x✝ + b✝ • y✝)
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
s : AffineSubspace k P
inst✝ : Nonempty ↥s
a b : ↥s
⊢ ↑(⟨↑a -ᵥ ↑b, ⋯⟩ +ᵥ b) = ↑a

Tactic:
apply AddTorsor.vsub_vadd'

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

Goal state before:
pp: case h
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun x ↦ x -ᵥ p₁) p₃

Tactic:
rw [and_comm, zero_add]

Goal state after:
case h
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ = (fun x ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
⊢ a • p ≤ b • q

Tactic:
le_def

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
⊢ ∀ (x : E), (a • p) x ≤ (b • q) x
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
V₃ : Type u_6
P₃ : Type u_7
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₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s ∧ f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (f p₁ -ᵥ f p₂) +ᵥ f p₃

Tactic:
by
    { simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }

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

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : #s ≠ 0
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Goal state after:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : #s ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Goal state after:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i ∈ s, centroidWeights k s i = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Goal state after:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i ∈ s, centroidWeights k s i = 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
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ (fun x1 x2 ↦ x1 + x2) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_ball, add_sub_add_comm]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.ball x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.ball x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) < r₁ + 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
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
⊢ AffineIndependent k p ↔ ∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0

Tactic:
by
  constructor
  · exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)
  · intro h s w hw hs i hi
    rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs
    rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw
    replace h := h ((↑s : Set ι).indicator w) hw hs i
    simpa [hi] using h

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.closedBall x r = p.closedBall (-x) r

Tactic:
ext
  rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
this : Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = vectorSpan k (range ⇑b)
⊢ ⊤ ≤ Submodule.span k (range fun i_1 ↦ b ↑i_1 -ᵥ b i)

Tactic:
rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]

Goal state after:
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⟩

Tactic:
obtain ⟨t, μ, rfl⟩ := 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
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⟩
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, 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:
obtain ⟨t, μ, rfl⟩ := 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
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.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
⊢ (b.coord i) q = 1 q

Tactic:
have hi : i ∈ s := by simp [s]

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ (b.coord i) q = 1 q
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ a, (b.coord i) a = x

Tactic:
have hi : i ∈ s := by simp [s]

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
⊢ ∃ a, (b.coord i) a = x
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:
rw [(@NormedAddGroup.nhds_zero_basis_norm_lt E
      p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb]

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
⊢ ∀ (i' : ι), p' i' → ∃ i, 0 < i ∧ {y | ‖y‖ < i} ⊆ s i'
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_4
𝕜 : 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‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖
⊢ ‖c‖ ^ n * ‖c‖ ≤ ε⁻¹ * p x * ‖c‖

Tactic:
← div_eq_inv_mul

Goal state after:
case refine_4
𝕜 : 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‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖
⊢ ‖c‖ ^ n * ‖c‖ ≤ p x / ε * ‖c‖
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
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ (↑q)ᶜ = ⇑(p.prodEquivOfIsCompl q hpq) '' {0}ᶜ ×ˢ univ

Tactic:
rw [prod_univ, LinearEquiv.image_eq_preimage_symm]

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ (↑q)ᶜ = ⇑(p.prodEquivOfIsCompl q hpq).symm ⁻¹' Prod.fst ⁻¹' {0}ᶜ
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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points = Set.range s.points

Tactic:
reindex,

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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range { points := s.points ∘ ⇑e.symm, independent := ⋯ }.points = Set.range s.points
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
u : ↑(stdSimplex S X)
⊢ u i = 1

Tactic:
rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]

Goal state after:
S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
u : ↑(stdSimplex S X)
⊢ ∀ b ∈ Finset.univ, b ≠ i → u b = 0
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✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)

Tactic:
rcases h with rfl | ⟨h₁, h₂⟩

Goal state after:
case mpr.inl
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₁ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₁)

case mpr.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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h₁ : s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case a
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
⊢ (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:
by_cases hx : x ∈ t

Goal state after:
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

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
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
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi) <;>
    simpa [sub_mul, sub_smul, sub_eq_zero]

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

Goal state before:
pp: case insert
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < ∑ i ∈ insert i t, w i
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
⊢ (insert i t).centerMass w z ∈ s

Tactic:
sum_insert hi

Goal state after:
case insert
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
⊢ (insert i t).centerMass w z ∈ s
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
p : (i : ι) → X i
⊢ nhdsKer {p} = univ.pi fun i ↦ nhdsKer {p i}

Tactic:
by
  simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ ∀ (S : Set (Set α)),
    (∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s) → ∀ (a : α), (nhdsKer {a} ∩ ⋃₀ S).Nonempty → a ∈ ⋃₀ S

Tactic:
intro S

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
⊢ (∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s) → ∀ (a : α), (nhdsKer {a} ∩ ⋃₀ S).Nonempty → a ∈ ⋃₀ S
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent x = connectedComponent y ↔ Joined x y

Tactic:
← mem_pathComponent_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent x = connectedComponent y ↔ y ∈ pathComponent x