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

Goal state before:
pp: case inl
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

pp: case inr
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
· exact H b c h

Goal state after:
case inr
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ m⁻¹ * n ∈ S

Tactic:
by simpa [eq_comm, QuotientGroup.eq] using hn

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ S.topologicalClosure

Tactic:
← SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ ↑S.topologicalClosure
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0

Tactic:
have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring

Goal state after:
this : cos (3 * (π / 3)) = cos π
⊢ (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (π - 2 * θ) = sin (2 * θ + θ)

Tactic:
congr; linarith

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

Goal state before:
pp: ⊢ cexp (-↑π / 2 * I) = -I

Tactic:
rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]

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.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_add]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
this : n + 1 + k - 1 = n + k
⊢ (n + k).descFactorial k = Polynomial.eval n P

Tactic:
simp [P, ascPochhammer_nat_eq_descFactorial, this]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| Polynomial.eval n P

Tactic:
mP.as_sum,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| Polynomial.eval n (X ^ P.natDegree + ∑ i ∈ Finset.range P.natDegree, C (P.coeff i) * X ^ i)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
have : ∀ n ≥ N, u n = v n := by
    intro n hn
    simp [v, if_neg (not_lt.mpr hn)]

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ ∃ x, connectedComponent x = univ

Tactic:
use x

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ connectedComponent x = univ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ -∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i

Tactic:
refine CauchySeq.neg ?_

Goal state after:
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
by
  suffices ∀ x : ℝ, ‖(x : AddCircle (1 : ℝ))‖ = |x - round x| by
    rcases eq_or_ne p 0 with (rfl | hp)
    · simp
    have hx := norm_coe_mul p x p⁻¹
    rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
    rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
  clear! x p
  intro x
  simp only [le_antisymm_iff, le_norm_iff, Real.norm_eq_abs]
  refine ⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩
  · rw [abs_sub_round_eq_min, le_inf_iff]
    rw [le_norm_iff] at hr
    constructor
    · simpa [abs_of_nonneg] using hr (fract x)
    · simpa [abs_sub_comm (fract x)] using hr (fract x - 1) (by simp)
  · simpa [zmultiples, QuotientAddGroup.eq, zsmul_eq_mul, mul_one, mem_mk, mem_range, and_imp,
      forall_exists_index, eq_neg_add_iff_add_eq, ← eq_sub_iff_add_eq, forall_comm (α := ℕ)]
      using round_le _

Goal state after:
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:
inv_mul_lt_iff₀ hp,

Goal state after:
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
⊢ x < p * (1 / 2)
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₁
h₄ : 1 ≤ t₀
⊢ γ.extend t₀ = γ.extend t₁

Tactic:
simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]

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

Goal state before:
pp: x : ℝ
⊢ arccos x ≤ π

Tactic:
by
  unfold arccos; linarith [neg_pi_div_two_le_arcsin x]

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

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x / y)) = rexp (log x - log y)

Tactic:
rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]

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

Goal state before:
pp: case hg
α : 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₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖g x‖) l (𝓝 0)

Tactic:
← tendsto_zero_iff_norm_tendsto_zero

Goal state after:
case hg
α : 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₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto g l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable

Tactic:
← Set.biUnion_preimage_singleton

Goal state after:
case refine_2
s : Set ℂ
hs : s.Countable
⊢ (⋃ y ∈ s, cexp ⁻¹' {y}).Countable
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (0 < ↑n / ↑d) = true
h₂ : decide (↑n / ↑d < 1) = true
⊢ Real.log e ≠ 0

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : 0 < (n : ℝ) / d := by
      simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)
    have h₂' : (n : ℝ) / d < 1 := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)
    exact ne_of_lt <| Real.log_neg h₁' h₂'

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

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑(n * 2) + ↑1 = ↑0
⊢ ↑θ = ↑ψ

Tactic:
← Int.cast_add,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑(n * 2 + 1) = ↑0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑π).cos = -1

Tactic:
rw [cos_coe, Real.cos_pi]

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

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

Tactic:
by
  simp_rw [sign, sin_neg, Left.sign_neg]

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

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

Tactic:
simp only [SignType.neg_eq_self_iff] at h_sign'

Goal state after:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
h' : a = b + ↑π
h_sign' : b.sign = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by
  rcases hx.eq_or_lt with (rfl | pos)
  · rw [zero_rpow h, zero_eq_mul]
    have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
    exact this.imp zero_rpow zero_rpow
  · exact rpow_add pos _ _

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

Goal state before:
pp: s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x ↦ rexp x / x ^ s) atTop atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)

Goal state after:
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x ↦ rexp x / x ^ n) ≤ᶠ[atTop] fun x ↦ rexp x / x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]

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

Goal state before:
pp: case inl
θ ψ : 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
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr
θ ψ : 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
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
· obtain rfl : k = -1 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos <| by
      grind [toReal_mem_Ioc]
    grind [abs_of_nonpos]

Goal state after:
case inr
θ ψ : 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
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]
    norm_cast
    rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
      Real.exp_log]
    rwa [norm_pos_iff]

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

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

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ h

Goal state after:
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
a✝ : ℕ
h : a✝ ≠ 0
⊢ ↑a✝ ^ r = 0 → ‖g a✝‖ = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
⊢ (fun x ↦ ‖log x ^ r‖) ≤ᶠ[atTop] fun x ↦ log x ^ r'

Tactic:
filter_upwards [tendsto_log_atTop.eventually_ge_atTop 1] with x hx
        rw [Real.norm_of_nonneg (by positivity)]
        gcongr
        exact le_max_left _ _

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

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

Tactic:
by simpa only [coe_rpow, coe_pow] using Real.rpow_natCast x n

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

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

Tactic:
ext; exact Real.rpow_add_intCast' (mod_cast x.2) h

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:
repeat' rw [rpow_def_of_pos hx0]
  rw [exp_lt_exp]; exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)

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
p₁ p₂ : P
⊢ p₂ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₂ -ᵥ p₁)

Tactic:
by
  rw [midpoint_comm, left_vsub_midpoint]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
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 : M
hv : v ≠ 0
⊢ u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u

Tactic:
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

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

Goal state before:
pp: case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ f p✝ = (const k P1 (f (Classical.arbitrary P1))) p✝

Tactic:
coe_const,

Goal state after:
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ f p✝ = Function.const P1 (f (Classical.arbitrary P1)) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddRightMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x y : k
hxy : x ≤ y
this : x • (p₁ - p₀) ≤ y • (p₁ - p₀)
⊢ (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) y

Tactic:
by simpa [lineMap]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
this : y • (p₁ - p₀) ≤ x • (p₁ - p₀)
⊢ (lineMap p₀ p₁) y ≤ (lineMap p₀ p₁) x

Tactic:
by simpa [lineMap]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}

Tactic:
exact hyz.antisymm hxz

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x -[𝕜] y]

Tactic:
rw [← sub_nonneg] at hxz hyz

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x -[𝕜] y]
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
v : V
⊢ v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
← SetLike.mem_coe,

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
v : V
⊢ v ∈ ↑s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
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
p : P
hp : p ∈ s
v : V
⊢ -v ∈ s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑s

Tactic:
← SetLike.mem_coe,

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
p : P
hp : p ∈ s
v : V
⊢ -v ∈ ↑s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑s
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
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
← SetLike.mem_coe,

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
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
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
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
← SetLike.mem_coe,

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
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Tactic:
lt_iff_le_not_ge,

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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ a ∈ [x -[{ t // 0 ≤ t }] y]

Tactic:
refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_le, ?_, ?_⟩ <;>
  ext

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ ↑(⟨t₁, t₁_nonneg⟩ + ⟨t₂, t₂_nonneg⟩) = ↑1

case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ ↑(⟨t₁, t₁_nonneg⟩ • x + ⟨t₂, t₂_nonneg⟩ • y) = ↑a
Module: Mathlib.Analysis.Convex.Hull

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
y : E
hx : y ∉ (convexHull 𝕜) (s \ {y})
hy : y ∈ (convexHull 𝕜) (s \ {y})
⊢ False

Tactic:
exact hx hy

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
x : α
⊢ Absorbs G₀ s {x} ↔ ∀ᶠ (c : G₀) in cobounded G₀, c⁻¹ • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]

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
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
⊢ (sInf t).direction = ⨅ s ∈ t, s.direction

Tactic:
apply (direction_sInf t).antisymm
  intro v hv
  rw [← vadd_mem_iff_mem_direction v ((mem_sInf_iff p t).mpr h), mem_sInf_iff]
  intro s hs
  rw [vadd_mem_iff_mem_direction v (h s hs)]
  simp only [Submodule.mem_iInf] at hv
  exact hv s hs

Goal state after:
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 : Convex R s
⊢ Convex A s

Tactic:
by
  simp only [Convex, StarConvex] at hs ⊢
  intro u hu v hv a b ha hb hab
  obtain ⟨c, hc1, hc2⟩ := halg ha
  obtain ⟨d, hd1, hd2⟩ := halg hb
  convert hs hu hv hc1 hd1 _
  · rw [← hc2, algebraMap_smul]
  · rw [← hd2, algebraMap_smul]
  rw [← hc2, ← hd2, ← algebraMap.coe_add] at hab
  exact (FaithfulSMul.algebraMap_eq_one_iff R A).mp hab

Goal state after: