mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ 0 ∉ Ioo a b

Tactic:
simp [ha.not_gt]

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

Goal state before:
pp: ⊢ StrictMonoOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
rintro x hx y hy hlt

Goal state after:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ tan x < tan y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ tan (π / 2 - x) = (tan x)⁻¹

Tactic:
by
  rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

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

Goal state before:
pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0

Tactic:
filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx

Goal state after:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ cos x ∈ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℂ
⊢ tan (↑π / 2 - x) = (tan x)⁻¹

Tactic:
by
  rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V

Tactic:
· refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)
      exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
this : γ 0 ∈ F ∧ γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F

Tactic:
simpa using this

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

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ min (fract x) (1 - fract x)

Tactic:
le_inf_iff

Goal state after:
case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
      simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]

Goal state after:
case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
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
⊢ Real.arcsin (-Real.sin θ) - π = θ

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:
← Real.sin_add_pi,

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

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.Complex.Arg

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 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 θ) - π) =
    θ

pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 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 θ) - π) =
    θ

Tactic:
· replace hθ := hθ.1
      have hcos : Real.cos θ < 0 := by
        rw [← neg_pos, ← Real.cos_add_pi]
        refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
      have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
      rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right] <;> [linarith;
        linarith; exact hsin.not_ge; exact hcos.not_ge]

Goal state after:
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 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.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
⊢ Tendsto g l (𝓝 0)

Tactic:
obtain ⟨c, hc⟩ := hmul.eventually_le

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
⊢ Tendsto g l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]

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

Goal state before:
pp: x : ℝ
⊢ log x⁻¹ = -log x

Tactic:
by_cases hx : x = 0; · simp [hx]
  rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]

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

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log (‖↑r‖ * ‖x‖)) + ↑(↑r * x).arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
norm_real,

Goal state after:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log (‖r‖ * ‖x‖)) + ↑(↑r * x).arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1

Tactic:
replace := log_le_sub_one_of_pos this

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
rintro h rfl

Goal state after:
h : ContinuousAt log 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
grind [mem_mulSupport, mem_support, log_eq_zero]

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

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
n : ℤ
| 2 * ↑π * I * (↑k / ↑N) = 2 * ↑π * I * ↑n

Tactic:
mul_right_inj' (by simp)

Goal state after:
k N : ℕ
hN : N ≠ 0
n : ℤ
| ↑k / ↑N = ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < ↑n * x.arg
hle : ↑n * x.arg ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
by
  rw [mul_comm] at hlt hle
  rw [cpow_mul, cpow_intCast] <;> simpa [log_im]

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

Goal state before:
pp: z : ℂ
θ : Real.Angle
⊢ ↑z.arg = θ ↔ z.arg = θ.toReal

Tactic:
by
  rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
induction θ using Real.Angle.induction_on
  induction ψ using Real.Angle.induction_on
  rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h
  rcases h with ⟨k, h⟩
  rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add,
    mul_right_inj' (two_ne_zero' ℝ), ← eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π,
    inv_mul_eq_div, mul_comm] at h
  rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]
  exact Real.tan_periodic.int_mul _ _

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

Goal state before:
pp: θ : Angle
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ Tendsto (fun x ↦ rexp (log b * x)) atBot (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id

Goal state after:
b : ℝ
hb : 1 < b
⊢ 0 < log b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
this : (↑(θ.toReal + ψ.toReal)).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
simpa using this

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

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

Tactic:
by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

Goal state after:
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
x : ℝ
hx : x ∈ Set.Iio 0
⊢ x ∈ {0}ᶜ

Tactic:
push _ ∈ _ at 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 < 0
⊢ x ∈ {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsClosed {x | x.1 = 0}

Tactic:
exact isClosed_eq continuous_fst continuous_const

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

Goal state before:
pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x

Tactic:
· simp_rw [rpow_zero]; exact continuousAt_const

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun a ↦ f a ^ 0) l (𝓝 (x ^ 0))

Tactic:
simp [tendsto_const_nhds]

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

Goal state before:
pp: case top.inl
y z : ℝ
Hy : y < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inl.inl
y z : ℝ
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inl.inr.inl
y z : ℝ
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inl.inr.inr
y z : ℝ
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl
y z : ℝ
Hy : y = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inr.inl.inl
y z : ℝ
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl.inr.inl
y z : ℝ
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl.inr.inr
y z : ℝ
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inr
y z : ℝ
Hy : 0 < y
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr.inr.inr
y z : ℝ
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inr.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

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

Tactic:
· exact (hx0 (bot_unique hxy)).elim

Goal state after:
case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 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∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

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

Goal state before:
pp: x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
⊢ log x ≤ x ^ ε / ε

Tactic:
rcases hx.eq_or_lt with rfl | h
  · rw [log_zero, zero_rpow hε.ne', zero_div]
  rw [le_div_iff₀' hε]
  exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
    (sub_one_lt _).le

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

Goal state before:
pp: case top.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ 1 ≤ ↑n

Tactic:
by exact_mod_cast hn

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

Goal state before:
pp: case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖↑(Real.log ↑n)‖ ≤ ↑n ^ ε / ε

Tactic:
norm_real,

Goal state after:
case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖Real.log ↑n‖ ≤ ↑n ^ ε / ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inr.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Goal state after:
case pos.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (↑na ^ b) nr
hden : IsNat (↑da ^ b) dr
⊢ IsNNRat (a ^ b) nr dr

Tactic:
by
  suffices IsNNRat (nr / dr : ℝ) nr dr by
    simpa [ha.to_eq, Real.div_rpow, hnum.1, hden.1]
  apply IsNNRat.of_raw
  rw [← hden.1]
  apply (Real.rpow_pos_of_pos _ _).ne'
  exact lt_of_le_of_ne' da.cast_nonneg ha.den_nz

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R y x = y ↔ x = y

Tactic:
midpoint_eq_left_iff,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ y = x ↔ x = y
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 : k
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Tactic:
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
    ext x
    change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
    rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
    simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]

Goal state after:
k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
this : ⇑f = (fun x ↦ x + f 0) ∘ fun x ↦ x * (f 1 - f 0)
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ a_1 ∈ Icc 0 1, f ((AffineMap.lineMap a b) a_1) = x) ↔ ∃ x_1 ∈ Icc 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x

Tactic:
AffineMap.apply_lineMap

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ a_1 ∈ Ioo 0 1, f ((AffineMap.lineMap a b) a_1) = x) ↔ ∃ x_1 ∈ Ioo 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x

Tactic:
AffineMap.apply_lineMap

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
inst✝ : ZeroLEOneClass 𝕜
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] = {c}

Tactic:
by
  refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_
  simp [singleton_subset_iff, left_mem_segment]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 (z +ᵥ s)

Tactic:
← image_vadd,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x ↦ z +ᵥ x) '' s)