mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y

Tactic:
← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)),

Goal state after:
case neg
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑(x ^ (1 / ↑n)) ≤ ↑y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.top
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

Tactic:
rcases hz with hz | hz <;> simp [hz, top_unique hxy]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
linarith [pi_pos, arg_le_pi x]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x z : E
x✝ : z ∈ [x -[𝕜] x]
a b : 𝕜
left✝¹ : 0 ≤ a
left✝ : 0 ≤ b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}

Tactic:
simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x z : E
x✝ : z ∈ [x -[𝕜] x]
a b : 𝕜
left✝¹ : 0 ≤ a
left✝ : 0 ≤ b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}

Tactic:
by
      simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))

Goal state after:
case neg.refine_2.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -m 1 • y
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
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ {c}

Tactic:
intro z ⟨hzt, hzs⟩
  rw [segment_eq_image, mem_image] at hzt hzs
  rcases hzt with ⟨p, ⟨p0, p1⟩, rfl⟩
  rcases hzs with ⟨q, ⟨q0, q1⟩, H⟩
  have Hx : x = (x - c) + c := by abel
  have Hy : y = (y - c) + c := by abel
  rw [Hx, Hy, smul_add, smul_add] at H
  have : c + q • (y - c) = c + p • (x - c) := by
    convert! H using 1 <;> simp [sub_smul]
  obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ openSegment 𝕜 x y

Tactic:
by
  rw [openSegment_eq_image_lineMap]
  exact ⟨⅟2, ⟨invOf_pos.mpr two_pos, invOf_lt_one one_lt_two⟩, rfl⟩

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

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / 1) • y + (b / 1) • z = a • y + b • z

Tactic:
div_one,

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + (b / 1) • z = a • y + b • z
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Tactic:
by
  simp_rw [convex_iff_segment_subset, segment_subset_iff]

Goal state after:
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
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ Convex 𝕜 [x -[𝕜] y]

Tactic:
rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab

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
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 • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]
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
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s

Tactic:
convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ 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 : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₂ = 1 • (p₁ -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Basic

Goal state before:

Tactic:
a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le
        (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
    _ = r := Convex.combo_self hab _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : 0 < 1 → (a / 1) • x + (b / 1) • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
div_one,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : 0 < 1 → a • x + (b / 1) • y ∈ s
⊢ a • x + b • y ∈ s
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 : 0 < p + q
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y

Tactic:
match_scalars <;> field

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

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
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s.direction = ⊤ → s = ⊤

Tactic:
intro hd

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤
⊢ s = ⊤
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
rintro x ⟨y, hy, rfl⟩
  rw [mem_balancedCore_iff] at hy
  rcases hy with ⟨t, ht1, ht2, hy⟩
  exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩

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

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s

Tactic:
refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩

Goal state after:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
⊢ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s = ⋃ r, ⋃ (_ : ‖r‖ ≤ 1 ∧ r ≠ 0), r • s

Tactic:
refine subset_antisymm (Set.iUnion₂_mono' fun r hr ↦ ?_) (Set.iUnion₂_mono' (by grind))

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
r : 𝕜
hr : ‖r‖ ≤ 1
⊢ ∃ i', ∃ (_ : ‖i'‖ ≤ 1 ∧ i' ≠ 0), r • s ⊆ i' • s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
⊢ IsOpen[inst✝¹] (balancedHull 𝕜 s)

Tactic:
have : (⋃ r : 𝕜, ⋃ (_ : ‖r‖ ≤ 1), r • s) = (⋃ r : 𝕜, ⋃ (_ : ‖r‖ ≤ 1 ∧ r ≠ 0), r • s) := by
    refine subset_antisymm (Set.iUnion₂_mono' fun r hr ↦ ?_) (Set.iUnion₂_mono' (by grind))
    obtain rfl | hr_ne := eq_or_ne r 0
    · exact ⟨1, by simp, by simpa [Set.zero_smul_set ⟨0, hzero⟩]⟩
    · use r
  rw [balancedHull, this]
  exact isOpen_biUnion (fun r hr ↦ hs.smul₀ hr.2)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
obtain ⟨r, V, hr, hV, hrVU⟩ : ∃ (r : ℝ) (V : Set E),
      0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U := by
    have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using!
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
  obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
    Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr
  have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
  -- It remains to show that `y • V ⊆ balancedCore 𝕜 U`
  refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)
  rw [smul_smul]
  rintro _ ⟨z, hz, rfl⟩
  refine hrVU _ _ ?_ hz
  rw [norm_mul, ← one_mul r]
  exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
⊢ Absorbs 𝕜 U s

Tactic:
rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U s
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 ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₂ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)

Tactic:
hp i hi

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 ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₂ i • (p₂ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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

Tactic:
rintro ⟨r, rfl⟩

Goal state after:
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
p₁ p₂ : P
r : k
⊢ (AffineMap.lineMap p₁ p₂) r ∈ line[k, p₁, 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✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ ↑(r • 1) * p (x✝¹ • x✝) = ‖x✝¹‖ * (↑(r • 1) * p x✝)

Tactic:
map_smul_eq_mul,

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✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ ↑(r • 1) * (‖x✝¹‖ * p x✝) = ‖x✝¹‖ * (↑(r • 1) * p x✝)
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 ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
⊢ (affineCombination k s p) w = p i

Tactic:
s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),

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 ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
⊢ (s.weightedVSubOfPoint p (p i)) w +ᵥ p i = p i
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 ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ i ∈ s, p i

Tactic:
Finset.sum_eq_sum_sdiff_singleton_add hi,

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 ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ x ∈ s \ {i}, p x + p i
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 ι
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁) w -ᵥ p₂

Tactic:
by
  rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

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 ι
w : ι → k
p₂ : ι → P
p₁ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂) w

Tactic:
by
  rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          x ≠ y →
            ∀ ⦃a b : 𝕜⦄,
              0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) < a • f x + b • f y

Tactic:
simpa [hab, zero_lt_one] using h hx hy hxy ha hb

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

Goal state before:
pp: case inr.inr.hn
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
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty

Tactic:
use ⟨x, y⟩

Goal state after:
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))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁.direction = s₂.direction

Tactic:
by
  rcases h with ⟨v, rfl⟩
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ vectorSpan k s₁ = vectorSpan k s₂

Tactic:
by
  simp_rw [← direction_affineSpan]
  exact h.direction_eq

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

Goal state before:
pp: case mp.inl
ι : 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
p : ι → P
hι : IsEmpty ι
⊢ ∃ s w, ∑ i ∈ s, w i = 0 ∧ 0 = (s.weightedVSub p) w

Tactic:
use ∅

Goal state after:
case h
ι : 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
p : ι → P
hι : IsEmpty ι
⊢ ∃ w, ∑ i ∈ ∅, w i = 0 ∧ 0 = (∅.weightedVSub p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : p x < ‖k‖ * r
⊢ p (k⁻¹ • x) < r

Tactic:
map_smul_eq_mul,

Goal state after:
case inr.refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : p x < ‖k‖ * r
⊢ ‖k⁻¹‖ * p x < r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ p (k⁻¹ • x✝) < r ↔ p x✝ < ‖k‖ * r

Tactic:
map_smul_eq_mul,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ ‖k⁻¹‖ * p x✝ < r ↔ p x✝ < ‖k‖ * r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ p (k⁻¹ • x) ≤ r

Tactic:
map_smul_eq_mul,

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ ‖k⁻¹‖ * p x ≤ r
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
i : ι
hij : i ≠ j
⊢ w i = w' i

Tactic:
simp [w', hij]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) v) = v
⊢ ∑ i, (b.coord i) v • b i = v

Tactic:
Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ∑ i, (b.coord i) v • b i = v
⊢ ∑ i, (b.coord i) v • b i = v
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
v : ι → V
b' : V
⊢ (s.weightedVSubOfPoint ((v, b') +ᵥ (p, b)).1 ((v, b') +ᵥ (p, b)).2) w =
    (∑ i ∈ s, w i • (LinearMap.proj i ∘ₗ LinearMap.fst k (ι → V) V - LinearMap.snd k (ι → V) V)) (v, b') +ᵥ
      (s.weightedVSubOfPoint (p, b).1 (p, b).2) w

Tactic:
simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub,
     vadd_vsub_assoc, ← sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib]

Goal state after: