mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) < ε / (2 * P) * P

Tactic:
exact lt_of_le_of_lt hsumlesum
        (by rw [← sum_mul, mul_comm]; gcongr)

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

Goal state before:
pp: x : ℝ
⊢ ‖1‖₊ = 1

Tactic:
← NNReal.coe_eq_one

Goal state after:
x : ℝ
⊢ ↑‖1‖₊ = 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ (∑ m ∈ range 3, (x / 2) ^ m / ↑m.factorial + (x / 2) ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3)) ^ 2 <
    (2 + x) / (2 - x)

Tactic:
rw [lt_div_iff₀ (by linarith), ← sub_pos]

Goal state after:
x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 <
    2 + x -
      (∑ m ∈ range 3, (x / 2) ^ m / ↑m.factorial + (x / 2) ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3)) ^ 2 * (2 - x)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
by
  rw [← eventually_forall_ge_atTop] at h
  obtain ⟨n₀, h, hrec⟩ := h.and hrec |>.exists
  obtain ⟨C₀, hrec⟩ := hrec
  rw [isBigO_iff]
  rw [← eventually_forall_ge_atTop] at hrec
  obtain ⟨n₁, H₁, H₂⟩ := (eventually_ge_atTop n₀).and hrec |>.exists
  let ubounds := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
  let C₁ := (Finset.Icc n₀ n₁).sup' (Finset.nonempty_Icc.mpr H₁) fun n => ‖f n‖ / ‖g n‖
  have C₁_mem : C₁ ∈ ubounds := by
    rw [Set.mem_ofPred]
    intro m hm
    calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)
  refine ⟨max C₀ C₁, ?_⟩
  filter_upwards [eventually_ge_atTop n₁] with n hn
  induction n using Nat.strongRecOn with
  | ind n h_ind =>
    refine H₂ _ (by grind) _ (by grind) fun m hm => ?_
    by_cases hbase : m < n₁
    · have hC₁ : C₁ ≤ max C₀ C₁ := by grind
      grw [← hC₁]
      grind
    · grind

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - (l.pred • ε + ε - ε)

Tactic:
add_sub_cancel_right

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred • ε
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ s⁻¹ = infEDist x s

Tactic:
by
  rw [← image_inv_eq_inv, infEDist_image isometry_inv]

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries (n + 1)) = (√(2 + x)).sqrtTwoAddSeries (n + 1)

Tactic:
sqrtTwoAddSeries_succ _ _,

Goal state after:
x : ℝ
n : ℕ
⊢ √(2 + (√(2 + x)).sqrtTwoAddSeries n) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n

Tactic:
obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ :=
    ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F

Tactic:
rcases h with ⟨γ, γ_in⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ x ∈ F ∧ y ∈ F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace ↑F

Tactic:
isPathConnected_iff_pathConnectedSpace

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : PathConnectedSpace ↑F
⊢ ConnectedSpace ↑F
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ toAddCircle ↑j = ↑(↑j / ↑N)

Tactic:
simp [toAddCircle]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ Injective ⇑toAddCircle

Tactic:
intro x y hxy
  have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)
  rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico,
    div_left_inj' this.ne', Nat.cast_inj, (val_injective N).eq_iff] at hxy <;>
  exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Interval

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
r : R
hr : 0 < r
k m n : ℤ
h : m - 1 < k ∧ k < n + 1
⊢ k ∈ Finset.Icc m n

Tactic:
grind [Int.lt_iff_add_one_le]

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

Goal state before:
pp: x : ℝ
⊢ x < sin (π / 2) ↔ x < 1

Tactic:
by
    rw [sin_pi_div_two]

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

Goal state before:
pp: case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).re = x.re

Tactic:
simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

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

Goal state before:
pp: case inr.a
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ (↑‖x‖ * cexp (↑x.arg * I)).im = x.im

Tactic:
simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

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

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π - π = θ

pp: case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π

pp: case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2

pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ

Tactic:
add_sub_cancel_right

Goal state after:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ = θ

case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π

case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2

case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
⊢ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-(π / 2)) (π / 2) → sin x ∈ Ioo (-1) 1

Tactic:
by grind [arcsin_lt_pi_div_two, neg_pi_div_two_lt_arcsin, arcsin_sin]

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

Goal state before:
pp: case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x

Tactic:
· rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]

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

Goal state before:
pp: z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0

case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝).toReal ≤ π

Tactic:
convert! toIocMod_le_right two_pi_pos _ _

Goal state after:
case e'_4
x✝ : ℝ
⊢ π = -π + 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal

Tactic:
rw [toReal_coe]

Goal state after:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a : Angle
h : 2 • a = 2 • a
h_ne : a.sign ≠ 0
h1 : a = a ∨ a = a + ↑π
h_sign : a.sign = 0
⊢ False

Tactic:
rw [h_sign] at h_ne

Goal state after:
a : Angle
h : 2 • a = 2 • a
h_ne : 0 ≠ 0
h1 : a = a ∨ a = a + ↑π
h_sign : a.sign = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
⊢ rexp 1 ^ ↑n = rexp ↑n

Tactic:
exp_one_rpow

Goal state after:
n : ℕ
⊢ rexp ↑n = rexp ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑x ^ (↑y + ↑↑n)).re = (↑x ^ ↑y).re * x ^ n

Tactic:
Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx),

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑x ^ ↑y * ↑x ^ ↑↑n).re = (↑x ^ ↑y).re * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_natCast' (mod_cast x.2) h

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

Goal state before:
pp: case inr.inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Tactic:
exact le_of_lt (rpow_lt_rpow h h₁' h₂')

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

Goal state before:
pp: case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p ↦ (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)

Tactic:
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop

Goal state after:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - ↑p ^ (-s) ≠ 0

Tactic:
refine sub_ne_zero_of_ne fun H ↦ ?_

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ (x ^ 2⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]

Goal state after:
case hx
x : ℂ
⊢ 0 ≤ ‖x‖

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by_cases hp_zero : p = 0
  · simp [hp_zero, zero_lt_one]
  · rw [← Ne] at hp_zero
    have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
    rw [← zero_rpow_of_pos hp_pos]
    exact rpow_lt_rpow hx_pos hp_pos

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

Goal state before:
pp: case inr.inr.top
z : ℝ
H : 0 < z
⊢ (∞ ^ z).toNNReal = ∞.toNNReal ^ z

pp: case inr.inr.coe
z : ℝ
H : 0 < z
x✝ : ℝ≥0
⊢ (↑x✝ ^ z).toNNReal = (↑x✝).toNNReal ^ z

Tactic:
· simp [H, ne_of_gt]

Goal state after:
case inr.inr.coe
z : ℝ
H : 0 < z
x✝ : ℝ≥0
⊢ (↑x✝ ^ z).toNNReal = (↑x✝).toNNReal ^ z
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p1 p2 : P1
⊢ f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

Tactic:
conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

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

Goal state before:
pp: case refine_2
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
h : ∃ q, f = const k P1 q
⊢ f.linear = 0

Tactic:
rcases h with ⟨q, rfl⟩
    exact const_linear k P1 q

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

Goal state before:
pp: k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : k
⊢ f x = f.linear (x • (1 -ᵥ 0)) +ᵥ f 0

Tactic:
← f.map_vadd

Goal state after:
k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : k
⊢ f x = f (x • (1 -ᵥ 0) +ᵥ 0)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ s

Tactic:
rw [zero_add] at hab

Goal state after:
case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ s

Tactic:
rw [zero_add] at hab

Goal state after:
case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ s
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
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)

Tactic:
by
  rw [sUnion_eq_iUnion]
  exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2

Goal state after:
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
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 * x + b * y ∈ Ioc x y

Tactic:
rw [zero_add] at hab

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

Goal state before:
pp: case inl
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r

Tactic:
rw [zero_add] at hab

Goal state after:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r
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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

Tactic:
rw [zero_add] at hab

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * 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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : vectorSpan k s = ⊤
p : P
hp : p ∈ affineSpan k s
⊢ affineSpan k s = ⊤

Tactic:
eq_iff_direction_eq_of_mem hp (mem_top k V p),

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
s : Set P
hs : s.Nonempty
h : vectorSpan k s = ⊤
p : P
hp : p ∈ affineSpan k s
⊢ (affineSpan k s).direction = ⊤.direction
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.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
by
  refine ⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩
  rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, hρ, hρball⟩
  rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
  specialize hρball a ha.le
  rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
    ball_normSeminorm] at hρball
  exact Metric.isBounded_ball.subset hρball

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x) + f (b • y) = a • f x + b • f y

Tactic:
f.map_smul_of_tower a,

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + f (b • y) = a • f x + b • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ f (0 • x + b • y) ≤ 0 • f x + b • f y

Tactic:
rw [zero_add] at hab

Goal state after:
case 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
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ f (0 • x + b • y) ≤ 0 • f x + b • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case inr
𝕜 : 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 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
    [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E]
    [inst_6 : Module 𝕜 β] [inst_7 : LinearOrder E] {s : Set E} {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃x : E⦄,
          x ∈ s →
            ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) →
        ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → x < y → f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [add_comm (a • x), add_comm (a • f x)]
    rw [add_comm] at hab
    exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)

Goal state after: