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

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

Tactic:
gcongr

Goal state after:
case hab
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ≤ ↑⌈x⌉₊
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
gcongr

Goal state after:
case a
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ ↑⌈x⌉₊ ≤ x + 1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atTop l ↔ Tendsto f atTop l

Tactic:
by
  simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]

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

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

Tactic:
cos_sub_pi_div_two

Goal state after:
x : ℝ
⊢ sin x = sin x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ Isometry ⇑quotientBot

Tactic:
MonoidHomClass.isometry_iff_norm

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ∀ (x : M ⧸ ⊥), ‖quotientBot x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ Isometry ⇑(quotientQuotientEquivQuotient S T h)

Tactic:
MonoidHomClass.isometry_iff_norm

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T), ‖(quotientQuotientEquivQuotient S T h) x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * sphere y δ = sphere (x * y) δ

Tactic:
simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_sphere]

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

Goal state before:
pp: x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Tactic:
gcongr

Goal state after:
case h₂
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * dist y x ≤ (1 - 0) * dist y x

Tactic:
gcongr

Goal state after:
case h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r
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 : 𝕜
x : Set E
⊢ ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal

Tactic:
NNReal.smul_def,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ ↑‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
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 : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal

Tactic:
NNReal.smul_def,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ↑‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r‖ * ‖z‖ ≤ ε / R * R

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r‖ ≤ ε / R

case h₂
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖z‖ ≤ R
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n

Tactic:
gcongr

Goal state after:
case h₁
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ ≤ ↑(u n) * ‖1‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
cos_sub_pi_div_two

Goal state after:
x : ℂ
⊢ sin x = sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
simp [Complex.exp_neg]

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)
⊢ 𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
compactOpen_eq,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}
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
⊢ f x ⤳ γ 0

Tactic:
γ.source

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
⊢ f x ⤳ f x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
gcongr

Goal state after:
case hbc
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ ≤ C / ‖w‖ ^ n
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
this : 0 < ↑N
⊢ x = y

Tactic:
rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico,
    div_left_inj' this.ne', Nat.cast_inj, (val_injective N).eq_iff] at hxy <;>
  exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n + 1)

Tactic:
gcongr

Goal state after:
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)
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 : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i

Tactic:
exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1 + 1)

Tactic:
gcongr

Goal state after:
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)
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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n + 1) ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)

Tactic:
gcongr

Goal state after:
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)
hfa : Antitone f
k n : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n)
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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + f (2 * n + 1)

Tactic:
gcongr

Goal state after:
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)
hfa : Antitone f
k n : ℕ
⊢ f (2 * n + 2) ≤ f (2 * n + 1)
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 : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i

Tactic:
exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

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

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
by_cases hx₂ : x ≤ 1

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
by_cases hx₂ : x ≤ 1

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ π / 2 - arcsin y < π / 2 - arcsin x

Tactic:
gcongr

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

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

Tactic:
gcongr

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

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by_cases hx₂ : x ≤ 1

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

Tactic:
exact hsin.not_ge

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

Tactic:
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:
gcongr

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

Goal state before:
pp: ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
← natCast_zsmul,

Goal state after:
ψ θ : Angle
⊢ ↑2 • ψ = ↑2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by rw [mul_comm, cpow_int_mul]

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

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Goal state after:
case inl
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0

case inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ↑(x ^ n).arg = n • ↑x.arg

Tactic:
obtain rfl | x0 := eq_or_ne x 0

Goal state after:
case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * (2 * (2⁻¹ * π) * ↑k) + 2 * (2⁻¹ * π)
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
← mul_add,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * (2 * (2⁻¹ * π) * ↑k + 2⁻¹ * π)
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
apply exp_pos

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

Goal state before:
pp: case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1

Tactic:
gcongr

Goal state after:
case a
x : ℝ
hx : 0 < |x|
⊢ log |x| * (log |x|)⁻¹ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ rexp x / x ^ n ≤ rexp x / x ^ s

Tactic:
gcongr

Goal state after:
case hdb
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1 * 1

Tactic:
gcongr

Goal state after:
case c0
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ≤ 0 ^ z

case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y ≤ 1

case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ z ≤ 1
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‖
⊢ |f x| ^ r ≤ (c * |g x|) ^ r

Tactic:
gcongr

Goal state after:
case h₁
α : 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‖
⊢ |f x| ≤ c * |g x|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
a✝ : ℕ
h : a✝ ≠ 0
⊢ ↑a✝ ^ r = 0 → ‖g a✝‖ = 0

Tactic:
simp [Real.rpow_eq_zero_iff_of_nonneg, h]

Goal state after:
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'
x : ℝ
hx : 1 ≤ log x
⊢ log x ^ r ≤ log x ^ r'

Tactic:
gcongr

Goal state after:
case hyz
s r : ℝ
hs : 0 < s
r' : ℝ := ⋯
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ r ≤ r'
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
ext; exact Real.rpow_add_of_nonneg x.2 hy hz

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

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ (1 / y) = x

Tactic:
rw [← rpow_mul]

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (y * (1 / y)) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
rw [← rpow_mul]

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (1 / y * y) = x
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:
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:
gcongr

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

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z

Tactic:
gcongr

Goal state after:
case ha
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ 0 ≤ log x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
    log_rpow x_pos, mul_le_mul_iff_left₀ (log_pos hx)]

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

Goal state before:
pp: case top
⊢ ∞ ^ 1 = ∞

Tactic:
exact dif_pos zero_lt_one

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

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1 ^ z

Tactic:
gcongr

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

Goal state before:
pp: x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z

Tactic:
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 : x ≤ y
⊢ x ^ p ≤ y ^ p

Tactic:
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:
gcongr

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

Goal state before:
pp: c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ c * x ^ y) (𝓝 0) (𝓝 0)

Tactic:
convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _

Goal state after:
case e'_5
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y

case convert_3
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]
  rfl

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

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)

Tactic:
← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _),

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ √x * √x = x ^ (1 / 2) * x ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

pp: case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

pp: case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
· cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]

Goal state after:
case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p

Tactic:
gcongr

Goal state after:
case h₁
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ a ≤ max a b

case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ b ≤ max a b
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 2 ^ p * max (a ^ p) (b ^ p) ≤ 2 ^ p * (a ^ p + b ^ p)

Tactic:
gcongr

Goal state after:
case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p