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

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

Tactic:
rw [set_smul_sphere_zero (by simp [ha.not_gt]), ← image_image (· * r), this.image_eq, image_id,
    image_mul_right_Ioo _ _ hr]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
simp only [tsum_eq_zero_of_not_summable hx, norm_zero]
    nontriviality R
    have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R
    have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
    linarith

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

Goal state before:
pp: ⊢ tan (π / 4) = 1

Tactic:
tan_eq_sin_div_cos,

Goal state after:
⊢ sin (π / 4) / cos (π / 4) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 6) = 1 / √3

Tactic:
tan_eq_sin_div_cos,

Goal state after:
⊢ sin (π / 6) / cos (π / 6) = 1 / √3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 3) = √3

Tactic:
tan_eq_sin_div_cos,

Goal state after:
⊢ sin (π / 3) / cos (π / 3) = √3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ tan x < tan y

Tactic:
tan_eq_sin_div_cos,

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ sin x / cos x < tan y

Tactic:
tan_eq_sin_div_cos,

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

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

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℝ
⊢ sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℝ
⊢ sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]

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

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

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℂ
⊢ sin (↑π / 2 - x) / cos (↑π / 2 - x) = (tan x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℂ
⊢ sin (↑π / 2 - x) / cos (↑π / 2 - x) = (sin x / cos x)⁻¹
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp [zero_smul_set, Set.singleton_zero, hr]
  · exact smul_sphere' hc x r

Goal state after:
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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
⊢ {r} ×ˢ (⇑f '' K) ⊆ U

Tactic:
by simpa [Set.subset_def, forall_comm (α := X)]

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

Goal state before:
pp: case h₂
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 : ℕ
⊢ f (2 * n) ≤ f (2 * n + 1)

Tactic:
exact hfm (by lia)

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ (⇑γ ∘ f) 0 = x

Tactic:
simp [hf₀]

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

Goal state before:
pp: case h₂
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 : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n + 1 + 1)

Tactic:
exact hfm (by lia)

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

Goal state before:
pp: x : ℝ
⊢ tan (arcsin x) = x / √(1 - x ^ 2)

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℝ
⊢ sin (arcsin x) / cos (arcsin x) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ 0 ≤ π / 2 - arcsin x

Tactic:
linarith [arcsin_le_pi_div_two x]

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos √(1 - x ^ 2)

Tactic:
rw [eq_comm, ← cos_arcsin]
  exact
    arccos_cos (arcsin_nonneg.2 h)
      ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))

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 / ↑(n + 1)‖ * ‖x ^ n / ↑n !‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
norm_div,

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

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

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ c / ‖f x‖ ≤ c / (c / ε)

Tactic:
by gcongr

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

Goal state before:
pp: case hf
α : 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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖)

Tactic:
change IsBoundedUnder _ _ fun _ ↦ _

Goal state after:
case hf
α : 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‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
by
  replace hx := norm_ne_zero_iff.mpr hx
  simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
    Real.log_mul hr.ne' hx, ofReal_add, add_assoc]

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

Goal state before:
pp: case ofNat
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
case ofNat
x : ℝ
a✝ : ℕ
⊢ log (x ^ ↑a✝) = ↑↑a✝ * log x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [← not_or, ← two_nsmul_eq_zero_iff]

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ -2 * sin ((θ + ψ) / 2) * sin (2 * (π * ↑k) / 2) = 0

Tactic:
mul_div_cancel_left₀ _ (two_ne_zero' ℝ),

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ -2 * sin ((θ + ψ) / 2) * sin (π * ↑k) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin (2 * (π * ↑k) / 2) * sin ((θ - ψ) / 2) = 0

Tactic:
mul_div_cancel_left₀ _ (two_ne_zero' ℝ),

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin (π * ↑k) * sin ((θ - ψ) / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 2 * sin (2 * (π * ↑k) / 2) * cos ((θ + ψ) / 2) = 0

Tactic:
mul_div_cancel_left₀ _ (two_ne_zero' ℝ),

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 2 * sin (π * ↑k) * cos ((θ + ψ) / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ 2 * sin ((θ - ψ) / 2) * cos (2 * (↑k * π) / 2 + π / 2) = 0

Tactic:
mul_div_cancel_left₀ _ (two_ne_zero' ℝ),

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ 2 * sin ((θ - ψ) / 2) * cos (↑k * π + π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [sin_coe, Real.sin_pi]

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

Goal state before:
pp: θ : Angle
⊢ θ.cos ^ 2 + θ.sin ^ 2 = 1

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

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

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

Tactic:
linarith [pi_pos, neg_pi_lt_toReal θ]

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

Goal state before:
pp: θ : Angle
| θ.cos

Tactic:
rw [← coe_toReal θ, cos_coe]

Goal state after:
θ : Angle
| Real.cos θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ ∀ (i : ℝ), 0 ≤ i → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici i

Tactic:
intro b hb

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hr : y < 0
⊢ Tendsto (fun x ↦ x ^ y) (𝓝[>] 0) atTop

Tactic:
by
  simp_rw +singlePass [← neg_neg y, Real.rpow_neg_eq_inv_rpow]
  exact (tendsto_rpow_atTop <| neg_pos.mpr hr).comp tendsto_inv_nhdsGT_zero

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:
Real.rpow_def_of_pos hb

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ rexp (log b * x)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ^ r * |g x| ^ r = c ^ r * |g x ^ r|

Tactic:
abs_rpow_of_nonneg hgx

Goal state after:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ^ r * |g x| ^ r = c ^ r * |g x| ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
h : y ≤ x
⊢ y ^ z ≤ x ^ z

Tactic:
by gcongr

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
h : x < y
⊢ x ^ z < y ^ z

Tactic:
by gcongr

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

Goal state before:
pp: case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

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

Goal state before:
pp: x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
⊢ x ^ p ≤ y ^ p

Tactic:
by gcongr

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

Goal state before:
pp: x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ y ^ p ≤ x ^ p

Tactic:
by gcongr

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

Goal state before:
pp: case top
y z : ℝ
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
        rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

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

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

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

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

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

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

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

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

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

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ (a ^ ↑n)⁻¹ = (a ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ (a ^ ↑n)⁻¹ = (a ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
simpa [ha.to_eq, NNReal.div_rpow, hnum.1, hden.1]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c d : k
⊢ (lineMap p₁ ((lineMap p₁ p₀) (1 - c))) (1 - d) = (lineMap p₁ p₀) ((1 - d) * (1 - c))

Tactic:
lineMap_lineMap_right

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

Goal state before:
pp: R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
⊢ (fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f) = f

Tactic:
ext
    rw [f.decomp]
    simp

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

Goal state before:
pp: case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
i : ι
⊢ ∀ (x : φv i), f.linear (Pi.single i x) = g.linear (Pi.single i x)

Tactic:
x

Goal state after:
case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
i : ι
x : φv i
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)
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 y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) (s + t)

Tactic:
by
  rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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

Goal state before:
pp: 𝕜 : 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 y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • x ≤ a • x + b • y

Tactic:
by gcongr

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

Goal state before:

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

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

Goal state before:
pp: 𝕜 : 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 y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ≤ a • y + b • y

Tactic:
by gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • x < a • x + b • y

Tactic:
by gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < a • y + b • y

Tactic:
by gcongr

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

Tactic:
x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
⊢ x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
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 t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)

Tactic:
by
  rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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✝³ : 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 • x ≤ a • x + b • y

Tactic:
by gcongr

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✝³ : 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 ≤ a • y + b • y

Tactic:
by gcongr

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✝³ : 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
hyx : y ≤ x
⊢ a • y + b • y ≤ a • x + b • y

Tactic:
by gcongr

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✝³ : 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
hyx : y ≤ x
⊢ a • x + b • y ≤ a • x + b • x

Tactic:
by gcongr

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
s : Set P
h : affineSpan k s = ⊤
⊢ s.Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty]

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 : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅