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

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

Tactic:
have hNMK : max N M + 1 < K :=
    lt_of_lt_of_le (by rw [two_mul]; exact lt_add_of_pos_left _ (Nat.succ_pos _)) hK

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

Goal state before:
pp: x : ℝ
⊢ 1 < rexp x ↔ 0 < x

Tactic:
rw [← exp_zero, exp_lt_exp]

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

Goal state before:
pp: x : ℝ
⊢ rexp x < 1 ↔ x < 0

Tactic:
rw [← exp_zero, exp_lt_exp]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ‖↑x_1.factorial‖) ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
norm_natCast

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ↑x_1.factorial) ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ Ico n j, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ‖↑x_1.factorial‖) ≤
    ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
norm_natCast

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ Ico n j, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ↑x_1.factorial) ≤
    ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)

Tactic:
zpow_add' (by simp [em'])

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case ha
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 ≤ 1 - t / ↑n

Tactic:
exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
⊢ ediam (c • s) = ‖c‖₊ • ediam s

Tactic:
refine le_antisymm (ediam_smul_le c s) ?_
  obtain rfl | hc := eq_or_ne c 0
  · obtain rfl | hs := s.eq_empty_or_nonempty
    · simp
    simp [zero_smul_set hs, ← Set.singleton_zero]
  · have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
    rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ‖r ^ n‖

Tactic:
by
  simpa using summable_norm_pow_mul_geometric_of_norm_lt_one 0 hr

Goal state after:
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 < δ
a b : E
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
by
  simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]

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

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ pathComponentIn F x = F

pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
· ext y
    exact ⟨fun hy => hy.mem.2, @h _⟩

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ ‖z‖ < ‖1‖

Tactic:
simp [hz]

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

Goal state before:
pp: p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|

Tactic:
rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]

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

Goal state before:
pp: x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x

Tactic:
rw [sin_zero]

Goal state after:
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 θ) - π) =
    θ

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:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
by grind [arccos_pos, arccos_lt_pi, arccos_cos]

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

Goal state before:
pp: z : ℂ
⊢ z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
not_iff_comm,

Goal state after:
z : ℂ
⊢ ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := y * 0, im := y * I.im }.arg

Tactic:
I_im,

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := y * 0, im := y * 1 }.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ cexp { re := x, im := y } ∈ slitPlane

Tactic:
simp [exp_mem_slitPlane, h₂.ne,
      (toIocMod_eq_self Real.two_pi_pos).mpr ⟨h₁, by simpa [two_mul] using h₂.le⟩]

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

Goal state before:
pp: case inl
z : ℂ
hz : z = 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp [hz]

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

Goal state before:
pp: θ : Angle
⊢ (-θ).cos = θ.cos

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact Real.cos_neg _

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

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

Tactic:
simp [toReal_neg_eq_neg_toReal_iff.2 h]

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

Goal state before:
pp: ⊢ (↑π).tan = 0

Tactic:
rw [tan_coe, Real.tan_pi]

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

Goal state before:
pp: θ : Angle
h : θ.sign ≤ 0
⊢ -↑|θ.toReal| = θ

Tactic:
by
  rw [SignType.nonpos_iff] at h
  rcases h with (h | h)
  · rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
  · rw [sign_eq_zero_iff] at h
    rcases h with (rfl | rfl) <;> simp [abs_of_pos Real.pi_pos]

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

Goal state before:
pp: case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
k : ℤ
hk : θ.toReal + ψ.toReal - π = 2 * π * ↑k
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
rw [sub_eq_iff_eq_add] at hk

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
k : ℤ
hk : θ.toReal + ψ.toReal = 2 * π * ↑k + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 / rexp (arg 0 * w.im)

Tactic:
zero_div,

Goal state after:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s : ℝ
⊢ (fun x ↦ x ^ s) =o[atTop] rexp

Tactic:
by
  simpa only [one_mul] using isLittleO_rpow_exp_pos_mul_atTop s one_pos

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

Goal state before:
pp: b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x ↦ 0 ^ x) x = 0 x

Tactic:
dsimp only

Goal state after:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = 0 x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x ↦ x ^ b) x = (fun x ↦ cexp (Complex.log x * b)) x

Tactic:
dsimp only

Goal state after:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = cexp (Complex.log x * b)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)

Tactic:
rw [log_rpow hx]

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

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

Tactic:
ext; exact Real.rpow_add_intCast (mod_cast hx) _ _

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

Goal state before:
pp: p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ (fun x ↦ x.1 ^ x.2) x = (fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) x

Tactic:
dsimp only

Goal state after:
p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2) * cos (x.2 * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ (fun x ↦ x.1 ^ x.2) x = (fun x ↦ rexp (log x.1 * x.2)) x

Tactic:
dsimp only

Goal state after:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2)
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_le_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.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
rw [ne_iff_lt_or_gt] at hp
  cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'

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

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

Tactic:
simp +contextual [hz]

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

Goal state before:
pp: x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
by
  rw [← NNReal.coe_inj, NNReal.coe_pow, coe_rpow]
  exact Real.rpow_inv_natCast_pow x.2 hn

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

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ rexp (log x * y) < rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [rpow_def_of_pos hx0]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]

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

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
    · simp [← coe_rpow_of_ne_zero h, h]

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
cases x with
  | top => exact (h'x rfl).elim
  | coe x =>
    have : x ≠ 0 := fun h => by simp [h] at hx
    simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

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

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
simp [hz]

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

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

Tactic:
nth_rw 1 [← ENNReal.rpow_one x]
  exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 = b → a • x + b • y = x

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ 0 = a → a • x + b • y = y

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
· rintro rfl
    rw [← add_zero a, hab, one_smul, zero_smul, add_zero]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ 0 = a → a • x + b • y = y

case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Tactic:
rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩
    exact h hy ha hb hab

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
x : E
s : Set E
inst✝ : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
h : s.Nonempty
⊢ x ∈ s

Tactic:
obtain ⟨y, hy⟩ := h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
x : E
s : Set E
inst✝ : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 ≤ b_1 ∧ 0 < a_1 + b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ [y -[𝕜] z]
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z → ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ s

Tactic:
apply hs.segment_subset hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ [x -[𝕜] y]
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
⊢ f (a • x) + f (b • y) ∈ s

Tactic:
LinearMap.map_smul_of_tower,

Goal state after:
𝕜 : 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 • f x + f (b • y) ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ico x y

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * x + b * y ∈ Ico x y