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

Goal state before:
pp: x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x

Tactic:
exact
    closure_lt_subset_le continuous_const continuous_sin
      (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ ⨅ K, ⨅ j, ⨅ (_ : IsCompact K), ⨅ (_ : IsOpen[inst✝] j), ⨅ (_ : MapsTo (⇑f) K j), 𝓟 {g | MapsTo (⇑g) K j} ↔
    ∃ i,
      (i.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) ∧
        ⋂ KU ∈ i, {g | MapsTo (⇑g) KU.1 KU.2} ⊆ s

Tactic:
iInf_prod',

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ ⨅ x, ⨅ (_ : IsCompact x.1), ⨅ (_ : IsOpen[inst✝] x.2), ⨅ (_ : MapsTo (⇑f) x.1 x.2), 𝓟 {g | MapsTo (⇑g) x.1 x.2} ↔
    ∃ i,
      (i.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) ∧
        ⋂ KU ∈ i, {g | MapsTo (⇑g) KU.1 KU.2} ⊆ s
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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ γ 1 ⤳ f y

Tactic:
γ.target

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ f y ⤳ f y
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ∀ {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

Tactic:
rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x✝ y : X
x : ↑I → X
h11 : Continuous[_, inst✝] x
h12 : { toFun := x, continuous_toFun := h11 }.toFun 0 = x✝
h13 : { toFun := x, continuous_toFun := h11 }.toFun 1 = y
h21 : Continuous[_, inst✝] ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }
h22 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      0 =
    x✝
h23 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      1 =
    y
⊢ { toFun := x, continuous_toFun := h11, source' := h12, target' := h13 } =
    { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21,
      source' := h22, target' := h23 }
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : Unique X
f : C(X, Y)
⊢ const X ((fun f ↦ f default) f) = f

Tactic:
ext x
    rw [Unique.eq_default x]
    rfl

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i

Tactic:
refine monotone_nat_of_le_succ (fun n ↦ ?_)

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * (n + 1) + 1), (-1) ^ i * f i
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
refine monotone_nat_of_le_succ (fun n ↦ ?_)

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ arccos (-1) = π

Tactic:
simp [arccos, add_halves]

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

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x * x ^ n / ↑((n + 1) * n !)‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
Nat.cast_mul,

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x * x ^ n / (↑(n + 1) * ↑n !)‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑(rexp (Real.log ‖x‖)) * (↑(x.re / ‖x‖) + ↑(x.im / ‖x‖) * I) = x

Tactic:
Real.exp_log (norm_pos_iff.mpr hx),

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * (↑(x.re / ‖x‖) + ↑(x.im / ‖x‖) * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ log x < x - 1

Tactic:
have h : log x ≠ 0 := by
    rwa [← log_one, log_injOn_pos.ne_iff hx1]
    exact mem_Ioi.mpr zero_lt_one
  linarith [add_one_lt_exp h, exp_log hx1]

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

Goal state before:
pp: ⊢ ↑(-π / 2) + ↑(-π / 2) = ↑π

Tactic:
← two_nsmul,

Goal state after:
⊢ 2 • ↑(-π / 2) = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ ↑π + ↑π = 0

Tactic:
← two_nsmul,

Goal state after:
⊢ 2 • ↑π = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
h' : HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) =
    if h : HasFiniteSupport fun i ↦ log (f i) then ∑ i ∈ Finite.toFinset h, log (f i) else 0

pp: case neg
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
h' : ¬HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) =
    if h : HasFiniteSupport fun i ↦ log (f i) then ∑ i ∈ Finite.toFinset h, log (f i) else 0

Tactic:
· simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]

Goal state after:
case neg
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
h' : ¬HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) =
    if h : HasFiniteSupport fun i ↦ log (f i) then ∑ i ∈ Finite.toFinset h, log (f i) else 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ c) =o[atTop] log

Tactic:
by
  refine Asymptotics.isLittleO_of_tendsto' ?_
    <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop
  filter_upwards [eventually_gt_atTop 1] with x hx
  aesop (add safe forward log_pos)

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 ∨ False
⊢ ↑θ = ↑ψ

Tactic:
or_false,

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: case h
θ : Angle
x✝ : ℝ
⊢ θ.cos = (↑x✝).cos ↔ θ = ↑x✝ ∨ θ = -↑x✝

Tactic:
exact cos_eq_real_cos_iff_eq_or_eq_neg

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

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

Tactic:
or_false,

Goal state after:
case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 < z.re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -π < θ.toReal

Tactic:
induction θ using Real.Angle.induction_on
  exact left_lt_toIocMod _ _ _

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

Goal state before:
pp: θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2

Tactic:
refine
    ⟨fun h => by linarith, fun h =>
      ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff₀' (zero_lt_two' ℝ)).1 h⟩⟩

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

Goal state before:
pp: θ : Angle
⊢ (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ θ + θ = ψ + ψ ↔ θ = ψ

Tactic:
← two_nsmul,

Goal state after:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ 2 • θ = 2 • ψ ↔ θ = ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)

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

Goal state before:
pp: θ : Angle
⊢ (θ + θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
← two_nsmul,

Goal state after:
θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

Tactic:
by
  refine
    Tendsto.congr' ?_
      ((tendsto_exp_nhds_zero_nhds_one.comp
            (by
              simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
        tendsto_log_atTop)
  apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))
  intro x hx
  simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢
  rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]
  field_simp

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (-1 / x)) atTop (𝓝 1)

Tactic:
convert! tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one
  ring

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

Goal state before:
pp: s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun x ↦ x ^ b) ∘ fun x ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s

Tactic:
simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul,
    mul_comm x, hb.ne', *]

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

Goal state before:
pp: x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z

Tactic:
simp [Real.sin]

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

Goal state before:
pp: n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖↑↑n ^ s‖ = ↑n ^ s.re

Tactic:
norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs

Goal state after:
n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ↑n ^ s.re = ↑n ^ s.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
  rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]

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

Goal state before:
pp: x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z

Tactic:
rcases eq_or_lt_of_le h₁ with (rfl | h₁'); · rfl
  rcases eq_or_lt_of_le h₂ with (rfl | h₂'); · simp
  exact le_of_lt (rpow_lt_rpow h h₁' h₂')

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

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

Tactic:
simp [hz, top_unique hxy]

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

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

Tactic:
simp [hz, top_unique hxy]

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

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

Tactic:
rw [← natCast_log, norm_real, norm_of_nonneg <| Real.log_nonneg <| by
    exact_mod_cast Nat.one_le_of_lt h.lt]

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: a : ℝ≥0
b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (a ^ b) r

Tactic:
rcases ha with ⟨rfl⟩
  constructor
  have : d ≠ 0 := mod_cast hb.den_nz
  rw [hb.to_eq rfl rfl, div_eq_mul_inv, NNReal.rpow_natCast_mul, ← Nat.cast_pow, hm, ← hkl, ← hr,
    Nat.cast_pow, NNReal.pow_rpow_inv_natCast]
  positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommRing 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : x ∈ [y -[𝕜] z]
⊢ SameRay 𝕜 (x - y) (z - x)

Tactic:
by
  rw [segment_eq_image'] at h
  rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
  simpa only [add_sub_cancel_left, ← sub_sub, sub_smul, one_smul] using
    (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
a b : 𝕜
left✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y

Tactic:
refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
a b : 𝕜
left✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun x ↦ b • x) x = a • x + (fun x ↦ b • x) y
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 z : E
s : Set E
hs : StarConvex 𝕜 (x + z) s
⊢ StarConvex 𝕜 x ((fun x ↦ x + z) ⁻¹' s)

Tactic:
rw [add_comm] at hs

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
segment_symm,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ [y -[𝕜] x] = Icc (min x y) (max x y)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case inl.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x ≤ a • x + b • y

pp: case inl.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ y

Tactic:
· calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr

Goal state after:
case inl.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i ↦ p i₀ -ᵥ p ↑i)

Tactic:
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]
  congr with v
  simp only [Set.mem_range, Set.mem_image, Set.mem_sdiff, Set.mem_singleton_iff, Subtype.exists]
  constructor
  · rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
    exact ⟨i₁, hi₁, hv⟩
  · exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

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

Goal state before:
pp: case mp
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
p p₁ p₂ : P
h : p ∈ line[k, p₁, p₂]
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p

Tactic:
← vsub_vadd p p₁,

Goal state after:
case mp
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
p p₁ p₂ : P
h : (p -ᵥ p₁) +ᵥ p₁ ∈ line[k, p₁, p₂]
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mp
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
p p₁ p₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂) r = p

Tactic:
← vsub_vadd p p₁,

Goal state after:
case mp
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
p p₁ p₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂) r = (p -ᵥ p₁) +ᵥ p₁
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

Tactic:
by
  constructor
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    simpa [add_comm] using h hx hy ha hb hab
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    rw [← neg_le_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy ha hb hab

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

Goal state before:
pp: case right
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
← vsub_add_vsub_cancel p₃ p₂ p₁,

Goal state after:
case right
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₂ + (p₂ -ᵥ p₁) ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i =
    (affineCombination k (s.erase i) p) w -ᵥ (affineCombination k {i} p) (-w)

Tactic:
← filter_ne'

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
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i =
    (affineCombination k ({a ∈ s | a ≠ i}) p) w -ᵥ (affineCombination k {i} p) (-w)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ (∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁) + ∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) +ᵥ p₁ = (∑ i ∈ s ∩ s', w i) • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
vadd_right_cancel_iff,

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
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ ∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁) + ∑ x ∈ s \ s', w x • (p x -ᵥ p₁) = (∑ i ∈ s ∩ s', w i) • (p₂ -ᵥ p₁)