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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
intro n _
    rw [← one_mul (abv x ^ n), pow_succ']
    gcongr

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

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ rexp x / C

Tactic:
calc
    x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
    _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
    _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
    _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

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

Goal state before:
pp: n : ℕ
⊢ Tendsto (fun x ↦ rexp x / x ^ n) atTop atTop

Tactic:
refine (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_
  have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
  have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
    eventually_atTop.1
      ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually
        (gt_mem_nhds this))
  simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN
  refine ⟨N, trivial, fun x hx => ?_⟩
  rw [Set.mem_Ioi] at hx
  have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
  rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]
  calc
    x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
    _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
    _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
    _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

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

Goal state before:
pp: ⊢ Continuous cos

Tactic:
by
  change Continuous fun z => (exp (z * I) + exp (-z * I)) / 2
  fun_prop

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

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

Tactic:
mul_lt_iff_lt_one_left two_pi_pos

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

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

Tactic:
mul_lt_iff_lt_one_left two_pi_pos

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

Goal state before:
pp: x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y - x) / 2)

Tactic:
apply sin_pos_of_pos_of_lt_pi

Goal state after:
case h0x
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < (y - x) / 2

case hxp
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ (y - x) / 2 < π
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖(lift S f.toAddMonoidHom hf) ↑x‖ / ‖f‖
⊢ False

Tactic:
exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s

Tactic:
simp [eq_comm]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst✝¹] U
⊢ MapsTo (⇑((f, g).2.comp (f, g).1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
(hKU : MapsTo (g ∘ f) K U)

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x ≤ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
replace hx₂ := Ne.lt_of_le hx' hx₂

Goal state after:
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2

Tactic:
· rwa [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]

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

Goal state before:
pp: case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x

Tactic:
refine arcsin_eq_of_sin_eq ?_ ?_

Goal state after:
case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x

case inr.inr.refine_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ Real.cos x.arg = x.re / ‖x‖

Tactic:
by
  rw [arg]
  split_ifs with h₁ h₂
  · rw [Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]
    field
  · rw [Real.cos_add_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
  · 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 (-π) π
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = θ

Tactic:
by
  simp only [arg, norm_mul, norm_cos_add_sin_mul_I, Complex.norm_of_nonneg hr.le, mul_one]
  simp only [re_ofReal_mul, im_ofReal_mul, neg_im, ← ofReal_cos, ← ofReal_sin, ←
    mk_eq_add_mul_I, neg_div, mul_div_cancel_left₀ _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr]
  by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
  · rw [if_pos]
    exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]
  · rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁
    rcases h₁ with h₁ | h₁
    · 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]
    · replace hθ := hθ.2
      have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
      have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
      rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

Tactic:
toIocMod

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
rcases hx.eq_or_lt with (rfl | hx)
  · simp [zero_le_one]
  rw [← log_one]
  exact log_lt_log_iff zero_lt_one hx

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

Goal state before:
pp: θ : Angle
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
by
  rw [← not_or, ← eq_neg_self_iff.not]

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him.not_gt]
    rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
      Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
      abs_of_nonneg him, abs_im_lt_norm]
    exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

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

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      (if x = 0 then if n = 0 then (starRingEnd ℂ) 1 else (starRingEnd ℂ) 0
        else (starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
apply_ite Inv.inv,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      if x = 0 then if n = 0 then ((starRingEnd ℂ) 1)⁻¹ else ((starRingEnd ℂ) 0)⁻¹
      else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
  · simp [hi, arg_neg_eq_arg_add_pi_of_im_neg]
  · rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]
    · simp [hr, Real.pi_ne_zero.symm]
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr]
  · simp [hi, hi.ne.symm, hi.not_gt, arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, ←
      add_eq_zero_iff_neg_eq, Real.pi_ne_zero]

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

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg

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

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

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

Tactic:
case =>

Goal state after:
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:
case =>

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
case =>

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

Goal state before:
pp: hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

Tactic:
case =>

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
case =>

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

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
by
  refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_
  filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

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

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
by
  obtain h | h | h := θ.sign.trichotomy
  · obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]
    have hsa' : (-θ + -ψ).sign ≠ 1 := by
      rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
    convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1
    all_goals simp [-neg_add_rev, ← neg_add, abs_toReal_neg]
  · grind [sign_eq_zero_iff, coe_pi_add_coe_pi]
  · exact abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux h (hs ▸ h) (h ▸ hsa.symm)

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
  · filter_upwards [eventually_ne_atTop 0] with _ h
    simp [Real.rpow_eq_zero_iff_of_nonneg, h]
  · exact hlim.norm.congr fun n ↦ by simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

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

Goal state before:
pp: case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
convert! this y x z hz (le_of_not_ge hxy) using 2

Goal state after:
case e'_2
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ x * y = y * x

case e'_3.h₁
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0

case e'_3.h₃
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
a✝ : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0)
⊢ x ^ z * y ^ z = y ^ z * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ∞
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
by
  lift x to ℝ≥0 using hx'
  rw [one_lt_coe_iff] at hx
  simp [← coe_rpow_of_ne_zero (lt_trans zero_lt_one hx).ne',
    NNReal.rpow_lt_rpow_of_exponent_lt hx hyz]

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

Goal state before:
pp: b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone fun x ↦ b ^ x

Tactic:
case =>

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

Goal state before:
pp: hb : 1 ≤ 1
⊢ Monotone fun x ↦ 1 ^ x

Tactic:
case =>

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone fun x ↦ b ^ x

Tactic:
case =>

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

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x ↦ 1 ^ x

Tactic:
case =>

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] N
v : Ray R M
⊢ (map f) (-v) = -(map f) v

Tactic:
induction v using Module.Ray.ind with | h g hg => simp

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✝ : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Tactic:
by
      rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
      exact hA hu hv ha hb hab

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
by
  rcases hxy.lt_or_gt with h | h
  · rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
  · rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

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
⊢ Convex 𝕜 s ↔ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
by
  refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩
  intro h x hx y hy a b ha hb hab
  obtain rfl | hxy := eq_or_ne x y
  · rwa [Convex.combo_self hab]
  · exact h hx hy hxy 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 : AffineSubspace k P
h : (↑s).Nonempty
⊢ directionOfNonempty h ≤ s.direction

Tactic:
rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk,
    AddSubmonoid.coe_set_mk]

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 : AffineSubspace k P
h : (↑s).Nonempty
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
⊢ a • u + b • v ∈ s

Tactic:
obtain ⟨d, hd1, hd2⟩ := halg hb

Goal state after:
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ a • u + b • v ∈ s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ a • a⁻¹ • b • x = b • x

Tactic:
smul_inv_smul₀ ha₀

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ b • x = b • x
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h }
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
totallyBounded_iff_subset_finite_iUnion_nhds_zero

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h }
⊢ Bornology.IsVonNBounded 𝕜 s
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
⊢ swap (DFunLike.coe ∘ F) (a * b) = swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b

Tactic:
by dsimp [UniformFun]; ext; exact map_mul _ _ _

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → Bornology.IsVonNBounded 𝕜 s

Tactic:
rintro ⟨a, ha⟩
    exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

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

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
⊢ swap (DFunLike.coe ∘ F) (a * b) = swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b

Tactic:
by dsimp [UniformFun]; ext; exact map_mul _ _ _

Goal state after: