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

Goal state before:
pp: ⊢ cos (π / 8) = cos (π / 2 ^ 3)

Tactic:
congr

Goal state after:
case e_a
⊢ 8 = 2 ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 8) = sin (π / 2 ^ 3)

Tactic:
congr

Goal state after:
case e_a
⊢ 8 = 2 ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 16) = cos (π / 2 ^ 4)

Tactic:
congr

Goal state after:
case e_a
⊢ 16 = 2 ^ 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 16) = sin (π / 2 ^ 4)

Tactic:
congr

Goal state after:
case e_a
⊢ 16 = 2 ^ 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 32) = cos (π / 2 ^ 5)

Tactic:
congr

Goal state after:
case e_a
⊢ 32 = 2 ^ 5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 32) = sin (π / 2 ^ 5)

Tactic:
congr

Goal state after:
case e_a
⊢ 32 = 2 ^ 5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 - π / 6) = cos (π / 3)

Tactic:
congr

Goal state after:
⊢ π / 2 - π / 6 = π / 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2

Tactic:
congr

Goal state after:
case e_a
⊢ π / 2 - π / 3 = π / 6
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 - π / 3) = cos (π / 6)

Tactic:
congr

Goal state after:
⊢ π / 2 - π / 3 = π / 6
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

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
cthickening_of_nonpos hδ,

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin (n + 1)), snoc p x i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p x i ∈ range ⇑γ

Tactic:
| _ p x =>

Goal state after:
case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin (n + 1)), snoc p x i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p x i ∈ range ⇑γ
Module: Mathlib.Topology.Path

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
toContinuousMap✝¹ : C(↑I, X)
source'✝¹ : toContinuousMap✝¹.toFun 0 = x
target'✝¹ : toContinuousMap✝¹.toFun 1 = y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ }.toContinuousMap =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝¹, source' := source'✝¹, target' := target'✝¹ } =
    { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }

Tactic:
congr

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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ (f ∘ ⇑(γ.trans γ')) t = if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩

Tactic:
Function.comp_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ f ((γ.trans γ') t) = if h_1 : ↑t ≤ 1 / 2 then (γ.map h) ⟨2 * ↑t, ⋯⟩ else (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x : ZMod N
⊢ ∀ ⦃a₂ : ZMod N⦄, toAddCircle x = toAddCircle a₂ → x = a₂

Tactic:
y

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
⊢ toAddCircle x = toAddCircle y → x = y
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 * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

Goal state after:
α : 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
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x

Tactic:
rw [le_norm_iff] at hr

Goal state after:
case refine_1
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case refine_2
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
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|

Tactic:
exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

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

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

Tactic:
congr

Goal state after:
case a
p : ℝ
hp : 0 < p
x : ℝ
| p

case a
p : ℝ
hp : 0 < p
x : ℝ
| |p⁻¹ * x - ↑(round (p⁻¹ * x))|
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
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
hg : Continuous[inst✝, _] g
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ (f t).trans (g t)

Tactic:
exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
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₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend ↑0 = γ.extend t₁

Tactic:
congr

Goal state after:
case neg.e_6
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₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ ↑0 = t₁
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
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₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend ↑0 = γ.extend t₁

Tactic:
congr
      linarith

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
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ γ.extend (min (max (↑0) t₀) t₁) = γ.extend (min t₀ t₁)

Tactic:
by
    simp only [min_def, max_def']
    split_ifs with h₁ h₂ h₃ h₄
    · simp [γ.extend_of_le_zero h₁]
    · congr
      linarith
    · have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
      simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]
    all_goals rfl

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

Goal state before:
pp: x : ℝ
⊢ (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) ↑(projIcc (-1) 1 ⋯ x) =
    (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x

Tactic:
Function.comp_apply,

Goal state after:
x : ℝ
⊢ ↑(IccExtend arcsin._proof_2 ⇑sinOrderIso.symm ↑(projIcc (-1) 1 ⋯ x)) =
    (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x

Tactic:
Function.comp_apply,

Goal state after:
x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = ↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm) x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩

Tactic:
congr

Goal state after:
case e_6
x : ℝ
hx : 0 < x
⊢ |x| = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ rexp (log 0)

Tactic:
log,

Goal state after:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ rexp (if hx : 0 = 0 then 0 else expOrderIso.symm ⟨|0|, ⋯⟩)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
have h := add_one_le_exp (log x)
    rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h

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

Goal state before:
pp: x y : ℂ
⊢ x.arg < y.arg + 2 * π

Tactic:
by
  grind [arg_le_pi x, neg_pi_lt_arg y]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑x).arg = 0

Tactic:
by simp [arg, hx]

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ cexp (log x) = x

Tactic:
log,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ cexp (↑(Real.log ‖x‖) + ↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (cexp x) = x

Tactic:
log,

Goal state after:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ ↑(Real.log ‖cexp x‖) + ↑(cexp x).arg * I = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ log (cexp x) = ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I

Tactic:
log,

Goal state after:
x : ℂ
⊢ ↑(Real.log ‖cexp x‖) + ↑(cexp x).arg * I = ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I
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:
log,

Goal state after:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log ‖↑r * x‖) + ↑(↑r * x).arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ log ((starRingEnd ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ) (log x)

Tactic:
log,

Goal state after:
x : ℂ
⊢ ↑(Real.log ‖(starRingEnd ℂ) x‖) + ↑((starRingEnd ℂ) x).arg * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case pos
x : ℂ
hx : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑π * I = ↑(Real.log ‖x‖) + ↑x.arg * I

pp: case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑(-x.arg) * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
· rw [hx]

Goal state after:
case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑(-x.arg) * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
log,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) (↑(Real.log ‖x‖) + ↑x.arg * I)) -
      ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (↑(Real.log ‖x‖) + ↑x.arg * I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ Tendsto (fun x ↦ log (rexp x)) atTop atTop

Tactic:
by simpa only [log_exp] using! tendsto_id

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

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

Tactic:
congr

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π / 2) + ↑π = ↑(-π / 2)
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 ↑n

Tactic:
apply Real.log_pos

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n

Tactic:
apply Real.log_pos

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case mp.refine_1
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

Tactic:
convert! toIocMod_mem_Ioc _ _ _
      ring

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

Goal state before:
pp: θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
refine ⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩

Goal state after:
θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]

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

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

Tactic:
rw [abs_eq pi_nonneg]

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
    rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
    refine IsLittleO.mul_isBigO ?exp ?cos
    case exp =>
      rw [isLittleO_const_iff one_ne_zero]
      refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
      rw [← log_neg_eq_log, log_neg_iff (by linarith)]
      linarith
    case cos =>
      rw [isBigO_iff]
      exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

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

Goal state before:
pp: case inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
rw [← neg_neg θ.sign, ← sign_neg] at hs
    have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm
    simpa [toReal_neg_eq_neg_toReal_iff.mpr, hθ, ← sub_eq_add_neg, eq_sub_iff_add_eq', eq_comm]

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp (log ↑x * y) = cexp ((log (-↑x) + ↑π * I) * y)

Tactic:
log,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((log (-↑x) + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((log (-↑x) + ↑π * I) * y)

Tactic:
log,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((↑(Real.log ‖-↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((fun x ↦ x ^ (-s)) ∘ fun x ↦ x⁻¹) x = (fun x ↦ x ^ s) x

Tactic:
Function.comp_apply,

Goal state after:
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ x⁻¹ ^ (-s) = (fun x ↦ x ^ s) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

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

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 1 < 0 then ∞ else ↑(x✝ ^ 1)) = ↑x✝

Tactic:
simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]

Goal state after:
case coe
x✝ : ℝ≥0
⊢ x✝ = 0 → 1 < 0 → False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Tactic:
lift y to ℝ≥0 using h

Goal state after:
case neg
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: z : ℝ
h : 0 < z
x : ℝ≥0∞
⊢ ∀ ⦃b : ℝ≥0∞⦄, x < b → (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) b

Tactic:
y

Goal state after:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
⊢ x < y → (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z

Tactic:
rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (inv_pos.2 hz)]

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

Goal state before:
pp: x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)

Tactic:
congr

Goal state after:
case e_a
x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

pp: case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
· linarith [pi_pos, neg_pi_lt_arg x]

Goal state after:
case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x : RayVector R M
⊢ ∀ {y z : RayVector R M},
    SameRay R ↑((equiv R M) x) ↑((equiv R M) y) →
      SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)

Tactic:
y

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y : RayVector R M
⊢ ∀ {z : RayVector R M},
    SameRay R ↑((equiv R M) x) ↑((equiv R M) y) →
      SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ (⇑f ∘ ⇑g) (v +ᵥ p) = (f.linear ∘ₗ g.linear) v +ᵥ (⇑f ∘ ⇑g) p

Tactic:
Function.comp_apply,

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ f (g (v +ᵥ p)) = (f.linear ∘ₗ g.linear) v +ᵥ (⇑f ∘ ⇑g) p
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 : k
⊢ (lineMap p₁ p₀) ((lineMap 1 0) (1 - c)) = (lineMap p₁ p₀) c

Tactic:
congr

Goal state after:
case e_6
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 : k
⊢ (lineMap 1 0) (1 - c) = c
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 : k
⊢ ∀ ⦃b : k⦄, x ≤ b → (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) b

Tactic:
y

Goal state after:
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
⊢ x ≤ y → (lineMap p₀ p₁) x ≤ (lineMap p₀ p₁) y
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 : k
⊢ ∀ ⦃b : k⦄, x ≤ b → (lineMap p₀ p₁) b ≤ (lineMap p₀ p₁) x

Tactic:
y

Goal state after:
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
⊢ x ≤ y → (lineMap p₀ p₁) y ≤ (lineMap p₀ p₁) x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inr.inr
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
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y

Tactic:
smul_neg

Goal state after:
case neg.refine_2.inr.inr.inr.inr
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
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = -(m 1 • y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = ⇑f - fun x ↦ f 0

Tactic:
decomp

Goal state after:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = (⇑f.linear + fun x ↦ f 0) - fun x ↦ (⇑f.linear + fun x ↦ f 0) 0