mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
this :
  |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| +
      |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| <
    ε / 2 + ε / 2
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε

Tactic:
rw [abs_sub_comm (∑ k ∈ range (max n i), a k), add_halves ε] at this

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
this :
  |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| +
      |(fun n ↦ ∑ i ∈ range n, a i) i - ∑ k ∈ range (max n i), a k| <
    ε
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ (fun _x ↦ c) =O[l] f'

Tactic:
refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)

Goal state after:
case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
← ih (by simp)

Goal state after:
case succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh (-x) = -sinh x

Tactic:
simp [sinh, exp_neg, (neg_div _ _).symm]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) (cexp x) - (starRingEnd ℂ) (cexp (-x))) / 2 = (starRingEnd ℂ) (sinh x)

Tactic:
← map_sub,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x * cos x ≤ 1

Tactic:
by simp only [← sq, cos_sq_le_one]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
have h3 : |x| = x := by simpa

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 5 / 100

Tactic:
simpa [← ofReal_sin, ← norm_eq_abs, ← norm_real] using Complex.sin_bound (x := x) (by simpa)

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
grw [abs_sub_le, h]

Goal state after:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
⊢ IsCauSeq abv fun n ↦ ∑ m ∈ range n, x ^ m

Tactic:
have hx1' : abv x ≠ 1 := fun h ↦ by simp [h] at hx1
  refine of_abv ?_
  simp only [abv_pow abv, geom_sum_eq hx1']
  conv in _ / _ => rw [← neg_div_neg_eq, neg_sub, neg_sub]
  have : 0 < 1 - abv x := sub_pos.2 hx1
  refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_
  · intro n _
    rw [abs_of_nonneg]
    · gcongr
      exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)
    refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)
    exact pow_le_one₀ (by positivity) hx1.le
  · intro n _
    rw [← one_mul (abv x ^ n), pow_succ']
    gcongr

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

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2 * 2) * π = x

Tactic:
Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑n * π = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s

Tactic:
rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)

Tactic:
vadd_eq_add,

Goal state after:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall (b + a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)

Tactic:
· intro h
    choose f hf using h
    -- By uniqueness of limits in a `T2Space`, since `fun i ↦ F i x` tends to both `f s₁ hs₁ x` and
    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
    have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      have := isCompact_iff_compactSpace.mp hs₁
      have := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂
    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
    -- compact set `s`
    refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
    rw [tendsto_compactOpen_iff_forall]
    intro s hs
    rw [liftCover_restrict']
    exact hf s hs

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

Tactic:
have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Tactic:
unfold ZerothHomotopy
    rintro ⟨h, h'⟩
    exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ pathComponent (x, y) = pathComponent x ×ˢ pathComponent y

Tactic:
ext ⟨a, b⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
a : X
b : Y
⊢ (a, b) ∈ pathComponent (x, y) ↔ (a, b) ∈ pathComponent x ×ˢ pathComponent y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ PathConnectedSpace (X × Y)

Tactic:
by
  rw [pathConnectedSpace_iff_univ, ← Set.univ_prod_univ]
  exact isPathConnected_univ.prod isPathConnected_univ

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ IsConnected F

Tactic:
rw [isConnected_iff_connectedSpace]
  rw [isPathConnected_iff_pathConnectedSpace] at hF
  exact @PathConnectedSpace.connectedSpace _ _ hF

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Tactic:
by
  let n := addOrderOf u
  change ∃ k : ℕ, ‖u‖ = p * (k / n)
  obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
  refine ⟨min (m % n) (n - m % n), ?_⟩
  rw [← hm, norm_div_natCast]

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

Goal state before:
pp: ⊢ range (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)

Tactic:
range_comp Subtype.val

Goal state after:
⊢ Subtype.val '' range (IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)
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:
replace hx := norm_ne_zero_iff.mpr hx

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

Goal state before:
pp: x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
split_ifs with hx

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

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

Goal state before:
pp: ⊢ Tendsto log (𝓝[≠] 0) atBot

Tactic:
by
  simpa [comp_def] using tendsto_log_nhdsGT_zero.comp tendsto_abs_nhdsNE_zero

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
this : 0 ≤ ↑n * (2 * π)
⊢ 0 ≤ n

Tactic:
by exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)

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

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
⊢ (∃ n, 2 * ↑π * I * ↑k / ↑N = ↑n * (2 * ↑π * I)) ↔ N ∣ k

Tactic:
conv in _ = _ => rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]

Goal state after:
k N : ℕ
hN : N ≠ 0
⊢ (∃ n, ↑k / ↑N = ↑n) ↔ N ∣ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : cos θ - cos ψ = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
cos_sub_cos,

Goal state after:
case mp
θ ψ : ℝ
Hcos : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0

Tactic:
aesop (add safe forward log_pos)

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

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

Tactic:
cos_sub_cos,

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

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

Tactic:
simp only [cpow_def, ite_mul, mul_ite]
  simp_all [exp_add, mul_add]

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

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

Tactic:
cos_sub_cos,

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ False

Tactic:
rw [iff_false, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ←
      sub_eq_add_neg, sub_half, Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him,
      abs_im_lt_norm]

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
· simp [hr, Real.pi_ne_zero.symm]

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
have : 0 < π / 2 := by positivity
  have := toReal_mem_Ioc θ
  rw [← cos_toReal, ← cos_abs]
  grind [cos_neg_of_pi_div_two_lt_of_lt, cos_nonneg_of_mem_Icc]

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

Goal state before:
pp: ⊢ Real.tan 0 = 0

Tactic:
Real.tan_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
simp only [H.symm, h, rpow_zero]
      calc
        (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]
        _ = 1 := by simp

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

Goal state before:
pp: case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
· exact abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux h (hs ▸ h) (h ▸ hsa.symm)

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x ↦ √(f x)) =O[l] fun x ↦ √(g x)

Tactic:
by
  simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos.le hg

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

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x ^ ↑y‖ = ‖x‖ ^ y

Tactic:
rw [norm_cpow_of_imp]

Goal state after:
x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y).re / rexp (x.arg * (↑y).im) = ‖x‖ ^ y

x : ℂ
y : ℝ
⊢ x = 0 → (↑y).re = 0 → ↑y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_imp]

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x‖ ^ y.re / rexp ((↑x).arg * y.im) = x ^ y.re

x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑x = 0 → y.re = 0 → y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
by
  simpa using rpow_add_intCast hx y n

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by
  rw [rpow_sub' hx h, rpow_one]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
by
  rw [rpow_sub' hx h, rpow_one]

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

Goal state before:
pp: p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (fun x ↦ Complex.log x.1 * x.2) p

Tactic:
exact
    ContinuousAt.mul
      (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
      continuous_snd.continuousAt

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

Goal state before:
pp: p : ℝ × ℝ
hp : 0 < p.2
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
obtain ⟨x, y⟩ := p

Goal state after:
x y : ℝ
hp : 0 < (x, y).2
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
by
  rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
  · -- x > 0 : easy case
    have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
    refine (continuousAt_cpow (Or.inl ?_)).comp this
    rwa [ofReal_re]
  · -- x = 0 : reduce to continuousAt_cpow_zero_of_re_pos
    have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
      rw [ofReal_zero]
      apply continuousAt_cpow_zero_of_re_pos
      tauto
    have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
    exact A.comp_of_eq B rfl
  · -- x < 0 : difficult case
    suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
      refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
      exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
    have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
    apply ContinuousAt.mul
    · refine (continuousAt_cpow (Or.inl ?_)).comp A
      rwa [neg_re, ofReal_re, neg_pos]
    · fun_prop

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

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

Tactic:
refine this.congr (Eventually.of_forall fun n => ?_)

Goal state after:
case neg
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ -(x -ᵥ x') +ᵥ 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
vadd_eq_add,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ -(x -ᵥ x') + 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x +ᵥ y) (y +ᵥ x) = x + y

Tactic:
vadd_eq_add,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x + y) (y +ᵥ x) = x + y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x + y) (y +ᵥ x) = x + y

Tactic:
vadd_eq_add,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x + y) (y + x) = x + y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ (⅟2 • (x + y) - x) +ᵥ ⅟2 • (x + y) = y

Tactic:
vadd_eq_add,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ ⅟2 • (x + y) - x + ⅟2 • (x + y) = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

Tactic:
simpa [hr.ne] using h₀

Goal state after:
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
x : V1
⊢ f x = f (x +ᵥ 0)

Tactic:
vadd_eq_add,

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
x : V1
⊢ f x = f (x + 0)
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
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x +ᵥ 0) = f.linear (Pi.single i x) +ᵥ f 0
s₃ : g (Pi.single i x +ᵥ 0) = g.linear (Pi.single i x) +ᵥ g 0
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)

Tactic:
vadd_eq_add,

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
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x + 0) = f.linear (Pi.single i x) +ᵥ f 0
s₃ : g (Pi.single i x + 0) = g.linear (Pi.single i x) +ᵥ g 0
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)