mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ |x / 2| ≤ 1

Tactic:
by rwa [abs_of_nonneg (le_of_lt (half_pos hx0))]

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-↑(x / 2) * I)‖ * ‖1 - cexp (↑x * I)‖

Tactic:
show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (↑(-x / 2) * I)‖ * ‖1 - cexp (↑x * I)‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE

Tactic:
have A : Ico 0 R ⊆ Ioo (-R) R :=
    fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩

Goal state after:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin π = 0

Tactic:
rw [← mul_div_cancel_left₀ π two_ne_zero, two_mul, add_div, sin_add, cos_pi_div_two]; simp

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

Goal state before:
pp: x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (-r * ↑n)

Tactic:
by
  simp_rw [mul_comm (-r), exp_nat_mul]
  apply summable_pow_mul_geometric_of_norm_lt_one
  rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]

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

Goal state before:
pp: n : ℤ
h : cos (↑n * (2 * π)) = 1
hx₁ : -n < 1
hx₂ : n < 1
⊢ ↑n * (2 * π) = 0

Tactic:
obtain rfl : n = 0 := le_antisymm (by lia) (by lia)

Goal state after:
h : cos (↑0 * (2 * π)) = 1
hx₁ : -0 < 1
hx₂ : 0 < 1
⊢ ↑0 * (2 * π) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2

Tactic:
by
  rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
    sin_sq_pi_over_two_pow_succ, sub_mul]
  · congr <;> norm_num
  · rw [sub_nonneg]
    exact (sqrtTwoAddSeries_lt_two _).le
  refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two
  · positivity
  · exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
← one_smul ℝ x

Goal state after:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (1 • x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
s : Set E
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
obtain rfl | hδ := hδ.eq_or_lt

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ 𝓝 f ↔
    ∃ S,
      S.Finite ∧
        (∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) ∧
          {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s

Tactic:
simp [f.hasBasis_nhds.mem_iff, ← ofPred_forall, and_assoc]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
x : X
hx : x ∈ F
y : X
hy : y ∈ F
⊢ JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)

Tactic:
rw [hf.joinedIn_image hx hy]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) ↔ ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

Tactic:
by
  constructor
  · rintro ⟨f, hf⟩ s _
    exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
  · intro h
    choose f hf using h
    -- By uniqueness of limits in a `T2Space`, since `fun i ↦ F i x` tends to both `f s₁ hs₁ x` and
    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
    have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      have := isCompact_iff_compactSpace.mp hs₁
      have := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂
    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
    -- compact set `s`
    refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
    rw [tendsto_compactOpen_iff_forall]
    intro s hs
    rw [liftCover_restrict']
    exact hf s hs

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑(γ₁.trans γ₂).extend '' univ = range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
← Iic_union_Ici (a := 1 / 2),

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑(γ₁.trans γ₂).extend '' (Iic (1 / 2) ∪ Ici (1 / 2)) = range ⇑γ₁ ∪ range ⇑γ₂
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
⊢ CompactSpace (AddCircle p)

Tactic:
← isCompact_univ_iff,

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
⊢ IsCompact univ
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}

Tactic:
simp [eq_iff_sub_mem, sub_eq_zero]

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

Goal state before:
pp: case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ |1| / 2

Tactic:
abs_one

Goal state after:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
by
    rw [sin_neg, sin_pi_div_two]

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

Goal state before:
pp: x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith

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

Goal state before:
pp: case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Tactic:
· rw [Real.cos_sub_pi, Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
    field

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)

Goal state after:
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos ↑(z.arg + ↑N * (2 * π)) + sin ↑(z.arg + ↑N * (2 * π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
push_cast at this

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
← neg_neg x,

Goal state after:
x : ℝ
hx : x < -1
⊢ 0 < log (- -x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log x < 0

Tactic:
← neg_neg x,

Goal state after:
x : ℝ
h0 : x < 0
h1 : -1 < x
⊢ log (- -x) < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]

Goal state after:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre, arg_of_re_nonneg hre, Real.neg_pi_div_two_le_arcsin, true_or]

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

Goal state before:
pp: x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg + π

Tactic:
arg_of_im_neg hi,

Goal state after:
x : ℂ
hi : x.im < 0
⊢ (-x).arg = -Real.arccos (x.re / ‖x‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π / 2 ∨ θ.toReal = -π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
toReal_eq_pi_div_two_iff,

Goal state after:
θ : Angle
⊢ θ = ↑(π / 2) ∨ θ.toReal = -π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
rw [arg, if_neg hre.not_ge, if_pos him]

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

Goal state before:
pp: case inr.inl
⊢ -↑|toReal 0| = 0

Tactic:
simp [abs_of_pos Real.pi_pos]

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

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

Tactic:
simp [abs_of_pos Real.pi_pos]

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

Goal state before:
pp: x : ℝ
⊢ rexp 1 ^ x = rexp x

Tactic:
← exp_mul,

Goal state after:
x : ℝ
⊢ rexp (1 * x) = rexp x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp

Goal state after:
case neg
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (fun x ↦ x ^ (a / (b * x + c))) atTop (𝓝 1)

Tactic:
refine
    Tendsto.congr' ?_
      ((tendsto_exp_nhds_zero_nhds_one.comp
            (by
              simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
        tendsto_log_atTop)

Goal state after:
a b c : ℝ
hb : 0 ≠ b
⊢ (rexp ∘ fun x ↦ a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun x ↦ x ^ (a / (b * x + c))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: r : ℝ
l : List ℝ≥0
this : ↑(List.map (fun x ↦ x ^ r) l).prod = ↑(l.prod ^ r)
⊢ (List.map (fun x ↦ x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Tactic:
push_cast at this

Goal state after:
r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun x ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r
⊢ (List.map (fun x ↦ x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ x ^ y = x ↔ x = 1 ∨ y = 1 ∨ x = 0 ∧ y ≠ 0

Tactic:
simpa [or_left_comm] using rpow_eq_rpow_right_iff (x := x) (y := y) (z := 1)

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

Goal state before:
pp: z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : x < y
⊢ (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) y

Tactic:
by simp only [NNReal.rpow_lt_rpow hxy h]

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

Goal state before:
pp: case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun x1 x2 ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))

Tactic:
refine
      (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_

Goal state after:
case refine_2
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg * z.2.im| ≤ π * C
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
rw [← one_rpow z]
  exact rpow_lt_rpow hx1 hx2 hz

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
by
  by_cases hx : x = ⊤
  · rw [hx, ContinuousAt]
    convert! ENNReal.tendsto_rpow_at_top h
    simp [h]
  lift x to ℝ≥0 using hx
  rw [continuousAt_coe_iff]
  convert! continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1
  ext1 x
  simp [← coe_rpow_of_nonneg _ h.le]

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x ↦ rexp (log b * x)

Tactic:
exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
      <| Real.log_neg hb₀ hb₁

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

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ‖↑↑p ^ (-s)‖ ≤ 1 / 2

Tactic:
norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ↑↑p ^ (-s).re ≤ 1 / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
rw [← zero_rpow_of_pos hp_pos]

Goal state after:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z

pp: case inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ SameRay R (x + y) z

Tactic:
· rwa [add_zero]

Goal state after:
case inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ SameRay R (x + y) z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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
u : Rˣ
v : Ray R M
⊢ -u • v = v ↔ ↑u < 0

Tactic:
units_smul_eq_self_iff,

Goal state after:
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
u : Rˣ
v : Ray R M
⊢ 0 < ↑(-u) ↔ ↑u < 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
⊢ (pi fun x ↦ 0) = 0

Tactic:
by
  ext; rfl

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
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ c + q • (y - c) = c + p • (x - c)

Tactic:
convert! H using 1

Goal state after:
case e'_2
𝕜 : 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]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ c + q • (y - c) = (1 - q) • c + (q • (y - c) + q • c)

case e'_3
𝕜 : 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]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ c + p • (x - c) = (1 - p) • c + (p • (x - c) + p • c)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]

Tactic:
convert! H using 1

Goal state after:
case e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-1 • x + t • y, -1 • x + s • y]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
⊢ f = g

Tactic:
apply pi_ext_zero h
  inhabit ι
  rw [← Pi.single_zero default]
  apply h

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
⊢ x = midpoint 𝕜 (x + y) (x - y)

Tactic:
rw [midpoint_add_sub]

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

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s -ᵥ ↑s → x ∈ ↑s

Tactic:
rintro ⟨a, ha, b, hb, rfl⟩
    simpa using s.smul_vsub_vadd_mem 1 ha hb hs

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ↑x - ↑x ∈ ↑s -ᵥ ↑s

Tactic:
mem_vsub

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ∃ x_1 ∈ ↑s, ∃ y ∈ ↑s, x_1 -ᵥ y = ↑x - ↑x
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ∈ s

Tactic:
Convex.combo_affine_apply hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Tactic:
by
    rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
    exact hs hx hy ha hb hab

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
⊢ spanPoints k s ⊆ ↑s₁

Tactic:
rintro p ⟨p₁, hp₁, v, hv, hp⟩
  rw [hp]
  have hp₁s₁ : p₁ ∈ (s₁ : Set P) := Set.mem_of_mem_of_subset hp₁ h
  refine vadd_mem_of_mem_direction ?_ hp₁s₁
  have hs : vectorSpan k s ≤ s₁.direction := vectorSpan_mono k h
  rw [SetLike.le_def] at hs
  rw [← SetLike.mem_coe]
  exact Set.mem_of_mem_of_subset hv hs

Goal state after: