mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x ↦ x ^ m * x ^ p) =o[𝓝 0] fun x ↦ x ^ m * 1 ^ p

Tactic:
exact IsBigO.mul_isLittleO (isBigO_refl _ _)
    (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_

Goal state after:
case calc_1
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (sin ↑x).im = 0

Tactic:
← ofReal_sin_ofReal_re,

Goal state after:
x : ℝ
⊢ (↑(sin ↑x).re).im = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cexp x = cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)

Tactic:
rw [← exp_add_mul_I, re_add_im]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ ↑e) =O[𝓝 (↑e.symm b)] (g ∘ ↑e)

Tactic:
simp only [IsBigO_def]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ ⇑e) =O[𝓝 (e.symm b)] (g ∘ ⇑e)

Tactic:
simp only [IsBigO_def]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inl
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x

Tactic:
obtain rfl : f = 0 := by
        ext n
        simpa using H n

Goal state after:
case inl
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |0 n| ≤ C * a ^ n
H : ∀ (n : ℕ), |0 n| ≤ 0 * a ^ n
⊢ ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x ↦ a ^ x
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3.h₁
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ ≤ r

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ c < 1

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case c0
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 ≤ c

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case b0
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 < r

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ i = (1 - x)⁻¹ʳ

Tactic:
change (Units.oneSub x h)⁻¹ = (1 - x)⁻¹ʳ

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ↑(Units.oneSub x h)⁻¹ = (1 - x)⁻¹ʳ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
h✝ : t ∈ {1}
⊢ const (↑I) y t ∈ F

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
h✝ : t ∉ {1}
⊢ const (↑I) x t ∈ F

Tactic:
assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
by
    rw [← this, neg_one_mul]
    simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
hp : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
⊢ ‖↑x‖ = |x|

Tactic:
rcases hp.symm.lt_or_gt with (hp | hp)
    · rw [abs_eq_self.mpr hp.le] at hx
      exact this p hp hx
    · rw [← norm_neg_period]
      rw [abs_eq_neg_self.mpr hp.le] at hx
      exact this (-p) (neg_pos.mpr hp) hx

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ (⇑γ ∘ f) 0 = x

Tactic:
by simp [hf₀]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False

Tactic:
have : ↑z * p ≤ p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx0 : ¬x < 0
this : 1 + 1 ≤ rexp 1
⊢ 2 ≤ rexp 1

Tactic:
rwa [one_add_one_eq_two] at this

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

Goal state before:
pp: x y : ℂ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by
  rw [mul_comm, cpow_nat_mul]

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

Goal state before:
pp: x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n

Tactic:
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
  split_ifs with h
  · rfl
  · rw [inv_cpow _ _ h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ ↑π

pp: case mpr
θ : Angle
⊢ θ ≠ ↑π → -π < -θ.toReal ∧ -θ.toReal ≤ π

Tactic:
· rintro ⟨h, h'⟩ rfl
    simp at h

Goal state after:
case mpr
θ : Angle
⊢ θ ≠ ↑π → -π < -θ.toReal ∧ -θ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (↑(Real.cos (x.arg + y.arg)) + ↑(Real.sin (x.arg + y.arg)) * I)

Tactic:
ofReal_cos,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (cos ↑(x.arg + y.arg) + ↑(Real.sin (x.arg + y.arg)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
⊢ False

Tactic:
have h' : a = b + π := by
    simp [← h]

Goal state after:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
h' : a = b + ↑π
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y

Tactic:
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top

Goal state after:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case h₁
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ |f x| ≤ c * |g x|

Tactic:
assumption

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

Goal state before:
pp: x : ℝ≥0
⊢ x ^ (-1) = x⁻¹

Tactic:
simp [rpow_neg]

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

Goal state before:
pp: p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p

Tactic:
have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p := by
    intro p hp_pos
    rw [← zero_rpow hp_pos.ne']
    exact rpow_lt_rpow hx_pos hp_pos
  rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
  · exact rpow_pos_of_nonneg hp_pos
  · simp only [zero_lt_one, rpow_zero]
  · rw [← neg_neg p, rpow_neg, inv_pos]
    exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

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

Goal state before:
pp: x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z

Tactic:
rw [← one_rpow z]
  exact rpow_lt_rpow zero_le_one hx hz

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x ^ (-1) = x⁻¹

Tactic:
simp [rpow_neg]

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
e' : P₂ ≃ᵃ[k] P₃
p : P₁
v : V₁
⊢ (e.trans e'.toEquiv) (v +ᵥ p) = (e.linear ≪≫ₗ e'.linear) v +ᵥ (e.trans e'.toEquiv) p

Tactic:
simp only [LinearEquiv.trans_apply, coe_toEquiv, (· ∘ ·), Equiv.coe_trans, map_vadd]

Goal state after:
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
a x b c : E
⊢ a +ᵥ x ∈ openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) ↔ x ∈ openSegment 𝕜 b c

Tactic:
← vadd_openSegment,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ a +ᵥ openSegment 𝕜 b c ↔ x ∈ openSegment 𝕜 b c
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
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Tactic:
by
  simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]

Goal state after:
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
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ 1 = a * 1 + b * 1

Tactic:
simp [hab]

Goal state after:
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
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a * 1 = a * 1

Tactic:
simp [hab]

Goal state after:
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
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ b * 1 = b * 1

Tactic:
simp [hab]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]

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

Goal state before:
pp: case hb
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ f x ≤ B

Tactic:
assumption

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

Goal state before:
pp: case hb
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ f y ≤ B

Tactic:
assumption

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
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ (↑Q).Nonempty

Tactic:
rw [nonempty_iff_ne_bot]
  apply eq_or_ne

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ (x • 1) • s
⊢ t ⊆ x • s

Tactic:
rwa [smul_one_smul N x s] at hx

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ x✝ ∈ K

Tactic:
assumption

Goal state after:
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
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
⊢ y✝ ∈ K

Tactic:
assumption

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
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
⊢ ↑(sInf (range s)) = ⋂ i, ↑(s i)

Tactic:
coe_sInf,

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
ι : Sort u_4
s : ι → AffineSubspace k P
⊢ ⋂ s_1 ∈ range s, ↑s_1 = ⋂ i, ↑(s i)
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ x ∈ ⋃ i, ⋃ (_ : ‖i‖ ≤ 1), a • i • s, x ∈ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s

Tactic:
mem_iUnion₂

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
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:
by
  refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩
  rw [Real.norm_eq_abs, abs_le] at ha
  rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
  exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
    (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
· intro ε hε
    exact H _ (dist_mem_uniformity hε)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
⊢ StrictConvex 𝕜 ((fun z ↦ c • z) ⁻¹' s)

Tactic:
obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _

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✝⁴ : PartialOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • p + b • q ∈ {p | p.1 ∈ s ∧ f p.1 < p.2}

Tactic:
refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).1 < (a • p + b • q).2
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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x ↦ p i -ᵥ x) '' p '' (s \ {i}))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_sdiff_singleton, Set.image_insert_eq, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ι : Type u_4
G : Type u_6
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → V
a : G
⊢ (s.weightedVSub (a • p)) w = a • (s.weightedVSub p) w

Tactic:
rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
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₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective ⇑f
s₁ s₂ : AffineSubspace k P₁
⊢ map f (s₁ ⊓ s₂) = map f s₁ ⊓ map f s₂

Tactic:
by
  ext p
  simp [mem_inf_iff]
  grind

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Tactic:
by
  simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
  simp [hi, hj, ← mul_sum]

Goal state after: