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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha✝ : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha : 0 < a
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha✝ : 0 ≤ a
ha : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a • x + 0 • y ∈ s

case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha✝ : 0 ≤ a
hb✝ : 0 ≤ b
hab : a + b = 1
ha : 0 < a
hb : 0 < b
⊢ a • x + b • y ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ 0 ∈ s

Tactic:
suffices (x : V) - x ∈ (s : Set _) by aesop

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ↑x - ↑x ∈ ↑s
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 ⊆ (convexHull 𝕜) s

Tactic:
exact subset_convexHull 𝕜 _

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
h : p ∈ affineSpan k ps
⊢ (affineSpan k (insert p ps)).direction = (affineSpan k ps).direction

Tactic:
affineSpan_insert_eq_affineSpan _ h

Goal state after:
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ EquicontinuousAt F x₀

Tactic:
rw [Metric.equicontinuousAt_iff_right]
  intro ε ε0
  filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁

Goal state after:
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:

Tactic:
dist (F i x) (F i y) ≤ b (dist x y) := H x y i
    _ ≤ |b (dist x y)| := le_abs_self _
    _ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
    _ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
rw [add_comm] at hab hfx ⊢
  exact hf.le_left_of_right_le' hy hx hb ha hab hfx

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
simpa [add_comm] using h hx hy ha hb hab

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p) x = ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
⊢ (p a ⊔ s.sup p) x = ↑(max (NNReal.mk ((p a) x) ⋯) (s.sup fun i ↦ NNReal.mk ((p i) x) ⋯))

Tactic:
coe_sup,

Goal state after:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p) x = ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
⊢ (⇑(p a) ⊔ ⇑(s.sup p)) x = ↑(max (NNReal.mk ((p a) x) ⋯) (s.sup fun i ↦ NNReal.mk ((p i) x) ⋯))
Module: Mathlib.Analysis.Seminorm

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

Tactic:
ext
  simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
⊢ ConvexOn 𝕜 univ ⇑f.symm

Tactic:
by
  refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn 𝕜 univ ⇑f
⊢ ConcaveOn 𝕜 univ ⇑f.symm

Tactic:
by
  refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ ∀ i2 ∈ s, i2 ≠ i → Pi.single i 1 i2 = 0

Tactic:
rintro j - 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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
j : ι
hj : j ≠ i
⊢ Pi.single i 1 j = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case h
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
x : P
hx : x ∈ s
y : Q
hy : y ∈ t
⊢ (x, y) ∈ ↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))

Tactic:
simp [mem_affineSpan, hx, hy]

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

Goal state before:
pp: case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
⊢ (∃ l ∈ Finsupp.supported k k Set.univ, (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v) →
    ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
rintro ⟨l, _, hv⟩

Goal state after:
case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
⊢ ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ {y | (p ⊔ q) (y - e) < r} = {a | p (a - e) < r ∧ q (a - e) < r}

Tactic:
coe_sup,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ {y | (⇑p ⊔ ⇑q) (y - e) < r} = {a | p (a - e) < r ∧ q (a - e) < r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ {y | (p ⊔ q) (y - e) ≤ r} = {a | p (a - e) ≤ r ∧ q (a - e) ≤ r}

Tactic:
coe_sup,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ {y | (⇑p ⊔ ⇑q) (y - e) ≤ r} = {a | p (a - e) ≤ r ∧ q (a - e) ≤ r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ {y | (s.sup fun i ↦ NNReal.mk ((p i) (y - x)) ⋯) < r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) < ↑r}

Tactic:
Finset.sup_lt_iff (show ⊥ < r from hr),

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
hr : 0 < ↑r
⊢ {y | ∀ b ∈ s, NNReal.mk ((p b) (y - x)) ⋯ < r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) < ↑r}
Module: Mathlib.Analysis.Seminorm

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

Tactic:
by
  simp only [mem_ball_zero, map_neg_eq_map]

Goal state after:
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:
by
  ext; simp [pointwise_vadd_eq_map, vadd_eq_iff_eq_neg_vadd]

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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)

Tactic:
convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase

Goal state after:
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✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | (⇑p ∘ fun z ↦ z + -x) x_1 < r}

Tactic:
p.mem_ball,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ p (y - x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z ↦ z + -x) x_1 < 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
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)
⊢ AffineIndependent k p

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Goal state after:
case 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
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)
h : IsEmpty ι
⊢ AffineIndependent k p

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)
h : Nonempty ι
⊢ AffineIndependent k 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
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
⊢ AffineIndependent k (⇑f ∘ p)

Tactic:
rcases isEmpty_or_nonempty ι with h | h

Goal state after:
case 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
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
h : IsEmpty ι
⊢ AffineIndependent k (⇑f ∘ p)

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
h : Nonempty ι
⊢ AffineIndependent k (⇑f ∘ p)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ {i}.centerMass w z = z i

Tactic:
by
  rw [centerMass, sum_singleton, sum_singleton]
  match_scalars
  field

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

Goal state before:
pp: case pos
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 : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h

Goal state after:
case pos
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 : (p '' s₂).Subsingleton
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ i ∈ s.disjSum t, Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) i = 1

Tactic:
sum_sumElim,

Goal state after:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ ∑ x ∈ s, a * ws x + ∑ x ∈ t, b * wt x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inl
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
h : AffineIndependent k fun p ↦ ↑p
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
have p₁ : P := AddTorsor.nonempty.some

Goal state after:
case inl
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
hx : x ∈ (convexHull R) s
hy : y ∈ (convexHull R) t
⊢ (x, y) ∈ (convexHull R) (s ×ˢ t)

Tactic:
rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢
  obtain ⟨ι, _, w, f, hw₀, hw₁, hfs, hf⟩ := hx
  obtain ⟨κ, _, v, g, hv₀, hv₁, hgt, hg⟩ := hy
  have h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1 := by
    rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
  refine ⟨ι × κ, inferInstance, fun p => w p.1 * v p.2, fun p ↦ (f p.1, g p.2),
    fun p ↦ mul_nonneg (hw₀ _) (hv₀ _), h_sum, fun p ↦ ⟨hfs _, hgt _⟩, ?_⟩
  ext
  · simp_rw [Prod.fst_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_comm (w _), mul_smul,
      sum_comm (γ := ι), ← Fintype.sum_smul_sum, hv₁, one_smul, hf]
  · simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ x ⤳ 0

Tactic:
rw [hp.hasBasis_zero_ball.specializes_iff]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ ∀ (i : Finset ι × ℝ), 0 < i.2 → x ∈ (i.1.sup p).ball 0 i.2
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ Tendsto u atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds u y₀]

Goal state after:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace

Tactic:
rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]; rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
⊢ T2Space (E →SLᵤ[σ, 𝔖] F)

Tactic:
let : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  have : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
  exact (isEmbedding_coeFn σ F 𝔖).t2Space

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
x : E
hx : x ∈ s
g : E →SLᵤ[σ, 𝔖] F
hg : g ∈ {x | MapsTo (⇑x) s U}
hf : (fun x ↦ c • x) g ∈ S
⊢ ((fun x ↦ c • x) g) x ∈ c • U

Tactic:
exact smul_mem_smul_set (hg hx)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}}

Tactic:
← NNReal.coe_le_coe,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} =
    sInf {x | ∃ (h : 0 ≤ x), NNReal.mk x ⋯ ∈ {c | ∀ (x : E), ↑‖f x‖₊ ≤ ↑(c * ‖x‖₊)}}
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ

Tactic:
dsimp [enorm]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ↑‖f x‖₊ ≤ ↑‖f‖₊ * ↑‖x‖₊