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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddRightMono 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
⊢ z ∈ openSegment 𝕜 x x

Tactic:
by
      obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
      refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
      rw [← add_smul, add_sub_cancel, one_smul, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Tactic:
· have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
    refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
    · rw [← add_div, add_comm, div_self h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

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

Goal state before:
pp: 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

Tactic:
rw [add_zero] at hab

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 = 1
⊢ a • x + 0 • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : 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
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
  intro h y hy a b ha hb hab
  obtain rfl | ha := ha.eq_or_lt
  · rw [zero_add] at hab
    rwa [hab, one_smul, zero_smul, zero_add]
  obtain rfl | hb := hb.eq_or_lt
  · rw [add_zero] at hab
    rwa [hab, one_smul, zero_smul, add_zero]
  exact h hy ha hb hab

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

Goal state before:
pp: 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 → x ≠ y → ∀ ⦃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

Tactic:
rw [add_zero] at hab

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 → x ≠ y → ∀ ⦃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 = 1
⊢ a • x + 0 • y ∈ s
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 • a • (z - y)) + a • b • (z - y) = 0

Tactic:
smul_comm,

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)
⊢ -(a • b • (z - y)) + a • b • (z - y) = 0
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
rw [add_zero] at hab

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)

Tactic:
· match_scalars <;> noncomm_ring

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
s : AffineSubspace k P
h : (↑s).Nonempty
v : V
⊢ v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]

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 : AffineSubspace k P
h : (↑s).Nonempty
v : V
⊢ (∃ x ∈ ↑s, ∃ y ∈ ↑s, x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ Convex 𝕜 (openSegment 𝕜 a b)

Tactic:
rw [convex_iff_openSegment_subset]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ ∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
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
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ a * x + 0 * y ∈ Ico x y

Tactic:
rw [add_zero] at hab

Goal state after:
case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ a * x + 0 * y ∈ Ico x y
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
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s ⊆ (convexHull 𝕜) s

pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s.Nonempty

Tactic:
· exact subset_convexHull ..

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s.Nonempty
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
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
h : s \ {x} = (convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 (s \ {x})

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
h : s \ {x} = (convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 ((convexHull 𝕜) (s \ {x}))
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K

Tactic:
refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_) <;> assumption

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
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x = b • x

Tactic:
smul_comm,

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
⊢ a • (a⁻¹ • b) • x = b • x
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
⊢ vectorSpan k (insert p ps) = vectorSpan k ps

Tactic:
by
  simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
isBounded_iff_forall_norm_le

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ C, ∀ x ∈ s, ‖x‖ ≤ C) ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
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:
by
  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.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ interior s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
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 : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : 0 ≤ 0
hab : a + 0 = 1
⊢ f (a • x + 0 • y) ≤ a • f x + 0 • f y

Tactic:
rw [add_zero] at hab

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
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 : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ f (a • x + 0 • y) ≤ a • f x + 0 • f 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 : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x ↦ x -ᵥ p) '' s)

Tactic:
rw [vectorSpan_def]
  refine le_antisymm ?_ (Submodule.span_mono ?_)
  · rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_right p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₁, hp₁, rfl⟩) (hm ⟨p₂, hp₂, rfl⟩)
  · rintro v ⟨p₂, hp₂, hv⟩
    exact ⟨p₂, hp₂, p, hp, hv⟩

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 ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w

Tactic:
rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff 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 q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
x : E
⊢ (a • p) x ≤ (b • q) x

Tactic:
exact mul_le_mul hab (hpq x) (apply_nonneg p x) (NNReal.coe_nonneg b)

Goal state after:
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 ι
C : ℝ≥0
x : E
⊢ (s.sup (C • p)) x = (C • s.sup p) x

Tactic:
rw [smul_apply, finset_sup_apply, finset_sup_apply]

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 ι
C : ℝ≥0
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk (((C • p) i) x) ⋯) = C • ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
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
y : E
r : ℝ
⊢ y ∈ p.ball 0 r ↔ p y < r

Tactic:
by rw [mem_ball, sub_zero]

Goal state after:
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
x : E
r : ℝ
⊢ p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
ext y; simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]

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

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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
⊢ f' x = f' y → x = y

Tactic:
h

Goal state after:
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ p (f' x) = p (f' y)

Tactic:
h

Goal state after:
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ p (f' y) = p (f' y)
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: case mp
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := ⋯
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := ⋯
x : ι
⊢ (∃ a ∈ univ, f'e a = x) → x ∈ s

Tactic:
rintro ⟨i, _, rfl⟩

Goal state after:
case mp
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
i : ↑ps
left✝ : i ∈ univ
⊢ f'e i ∈ s
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 : ι
⊢ v ∈ Submodule.span k ((fun i ↦ p i -ᵥ p i0) '' Set.univ) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
Finsupp.mem_span_image_iff_linearCombination

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 ∈ 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
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: case mp
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := ⋯
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := ⋯
x : ι
⊢ (∃ a ∈ univ, f'e a = x) → x ∈ s

pp: case mpr
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := ⋯
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := ⋯
x : ι
⊢ x ∈ s → ∃ a ∈ univ, f'e a = x

Tactic:
· rintro ⟨i, _, rfl⟩
      exact (hf' i).1

Goal state after:
case mpr
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := ⋯
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := ⋯
x : ι
⊢ x ∈ s → ∃ a ∈ univ, f'e a = x
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: case mpr
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ∃ a ∈ univ, f'e a = x

Tactic:
use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _

Goal state after:
case right
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := ⋯
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := ⋯
x : ι
hx : x ∈ s
⊢ f'e ⟨p x, ⋯⟩ = x