mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case succ.inl
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ (n + 1)) = ↑(n + 1) * log 0

pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
· simp

Goal state after:
case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0

pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x

Tactic:
· simp

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 < 1 + x

Tactic:
by grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < 1 + x

Tactic:
by grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < log (1 + x)

Tactic:
by
  rw [lt_log_iff_exp_lt (by grind)]
  convert exp_lt_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
  all_goals field_simp; grind

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

Goal state before:
pp: x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_log⟩

Goal state after:
x : ℝ
⊢ ContinuousAt log x → x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * -I) - ↑(Real.log (‖x‖ ^ 2)) =
    if x.arg = π then -(↑(Real.log ‖x‖) + ↑x.arg * -I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
Real.log_pow,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * -I) - ↑(↑2 * Real.log ‖x‖) =
    if x.arg = π then -(↑(Real.log ‖x‖) + ↑x.arg * -I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
⊢ log ↑0 = (Nat.factorization 0).sum fun p t ↦ ↑t * log ↑p

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → cexp x = 1

Tactic:
rintro ⟨n, rfl⟩

Goal state after:
case mpr
n : ℤ
⊢ cexp (↑n * (2 * ↑π * I)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0

Tactic:
by
  rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]

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

Goal state before:
pp: case inl.inl
y : ℂ
⊢ 0 ^ (↑0 * y) = (0 ^ y) ^ 0

pp: case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
· simp

Goal state after:
case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ + ψ - π = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
sub_eq_iff_eq_add,

Goal state after:
θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * π * ↑k + π
⊢ θ + ψ = 2 * ↑k * π + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ ¬z.im < 0 ∧ z.im < 0 ↔ 0 < z.re

Tactic:
not_and_self_iff,

Goal state after:
case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ False ↔ 0 < z.re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
⊢ |(-↑π).toReal| = |(↑π).toReal|

pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|

Tactic:
· simp

Goal state after:
case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
· exact tan_add_pi _

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

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
sub_eq_iff_eq_add,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * π * ↑k + π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
⊢ (↑π).toReal ∈ Set.Ioo 0 π ↔ (↑π).sign = 1

pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
· simp

Goal state after:
case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Tactic:
have ha :
      Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z =>
        (arg z : Real.Angle) + π := by
      rw [Function.update_eq_iff]
      exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
have h1 := Real.Angle.two_zsmul_eq_iff.mp h

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ cos (x * π)) =O[atTop] fun _x ↦ 1

Tactic:
rw [isBigO_iff]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * ‖1‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (1 / x)) atTop (𝓝 1)

Tactic:
convert! tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one
  ring

Goal state after:
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
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y

Tactic:
by_cases ha' : a = ⊤

Goal state after:
case pos
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∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ∞
⊢ ↑x < a ^ y

case neg
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∞
ha : a ∈ Set.Ioi ↑c
ha' : ¬a = ∞
⊢ ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
k : ℤ
hk : π - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ 2 * π * ↑k ∈ Set.Ioo (2 * π * ↑(0 - 1)) (2 * π * ↑(0 + 1))

Tactic:
by grind

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ g =O[atTop] fun n ↦ ↑n ^ r

Tactic:
refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left

Goal state after:
case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg hx _),
      Complex.ofReal_cpow hx, Complex.ofReal_mul, Complex.cpow_mul, Complex.ofReal_cpow hx]

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ 𝓝[<] 0 ≤ 𝓝[≠] 0

Tactic:
refine nhdsWithin_mono 0 (fun x hx ↦ ?_)

Goal state after:
h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
x : ℝ
hx : x ∈ Set.Iio 0
⊢ x ∈ {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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:
· simp

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ y ^ z < x ^ z

Tactic:
← inv_lt_inv₀,

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ (x ^ z)⁻¹ < (y ^ z)⁻¹

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
  · rfl
  simpa using hl

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

Goal state before:
pp: case inr.inl
y z : ℝ
hx₀ : 1 ≠ 0
⊢ 1 ^ y = 1 ^ z ↔ y = z ∨ 1 = 1 ∨ 1 = 0 ∧ (y = 0 ↔ z = 0)

pp: case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
· simp

Goal state after:
case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
· simp

Goal state after:
case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (0, y)

Tactic:
apply continuousAt_cpow_zero_of_re_pos

Goal state after:
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ 0 < 0 then ∞ else x ^ 0 * y ^ 0

pp: case inr
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
· simp

Goal state after:
case inr
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ ↑2⁻¹).im = √((‖x‖ - x.re) / 2)

Tactic:
cpow_ofReal_im,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹) = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
by
  nth_rw 2 [← ENNReal.rpow_one x]
  exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

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

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ (x ^ ↑2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
cpow_ofReal_im,

Goal state after:
x : ℂ
hx : x.im < 0
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹) = -√((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
cpow_ofReal_im,

Goal state after:
x : ℂ
⊢ |‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

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

Goal state before:
pp: case h
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 : f.linear = 0
p✝ : P1
⊢ f p✝ -ᵥ f (Classical.arbitrary P1) = 0

Tactic:
← f.linearMap_vsub,

Goal state after:
case h
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 : f.linear = 0
p✝ : P1
⊢ f.linear (p✝ -ᵥ Classical.arbitrary P1) = 0
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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ f (g.linear v +ᵥ g p) = (f.linear ∘ₗ g.linear) v +ᵥ (⇑f ∘ ⇑g) p

Tactic:
f.map_vadd

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ f.linear (g.linear v) +ᵥ f (g p) = (f.linear ∘ₗ g.linear) v +ᵥ (⇑f ∘ ⇑g) p
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 = x • (f 1 -ᵥ f 0) +ᵥ f 0

Tactic:
← f.linearMap_vsub,

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 = x • f.linear (1 -ᵥ 0) +ᵥ f 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Tactic:
by
  obtain rfl | hy := eq_or_ne y 0
  · exact ⟨0, le_rfl, zero_smul _ _⟩
  · exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

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

Goal state before:

Tactic:
a • x + b • y ≤ a • x + b • x := by gcongr
      _ = x := Convex.combo_self hab _

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ Convex 𝕜 (s \ {x}) → x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
rintro hsx hx
    rw [hsx.convexHull_eq] at hx
    exact hx.2 (mem_singleton _)

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
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹‖ * ‖r‖

Tactic:
norm_inv

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a‖⁻¹ * ‖r‖
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r⁻¹‖ ≤ 1

Tactic:
norm_inv

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1

Tactic:
norm_inv

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
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 : Set P
⊢ (↑(affineSpan k s)).Nonempty ↔ s ≠ ∅

Tactic:
affineSpan_nonempty,

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 : Set P
⊢ s.Nonempty ↔ 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
⊢ ∀ (i : 𝕜), ‖i‖ ≤ 1 ∧ i ≠ 0 → ∃ i', ∃ (_ : ‖i'‖ ≤ 1), i • s ⊆ i' • s

Tactic:
by grind

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

Goal state before:
pp: E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : map (⇑σ) (𝓝 0) = 𝓝 0
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)

Goal state after:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

pp: case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
· simp

Goal state after:
case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
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
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ Bornology.IsBounded s

Tactic:
specialize hρball a ha.le

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
hρball : s ⊆ a • Metric.ball 0 1
ha : ρ < ‖a‖
⊢ Bornology.IsBounded s
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✝² : 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
⊢ ConvexOn 𝕜 s f

Tactic:
refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
  wlog h : x < y
  · 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)
  exact hf hx hy h ha hb hab

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
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)

Tactic:
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]

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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k (insert (p i -ᵥ p i) ((fun x ↦ p i -ᵥ x) '' p '' (s \ {i})))