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

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
m : ℕ
hmJ : m ∈ range (max N M + 1)
⊢ abv (∑ k ∈ range (K - m), g k - ∑ k ∈ range K, g k) ≤ ε / (2 * P)

Tactic:
refine le_of_lt <| hN (K - m) (le_tsub_of_add_le_left <| hK.trans' ?_) K hKN.le

Goal state after:
case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
m : ℕ
hmJ : m ∈ range (max N M + 1)
⊢ m + N ≤ 2 * (max N M + 1)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * cos y = sin (x - y) + sin (x + y)

Tactic:
simp [sin_add, sin_sub]

Goal state after:
x y : ℝ
⊢ 2 * sin x * cos y = sin x * cos y + sin x * cos y
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)

Tactic:
simp [sin_three_mul]

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

Goal state before:
pp: case hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1

Tactic:
rw [sq, ← abs_mul_self, abs_mul]
                    exact mul_le_one₀ hx (abs_nonneg _) hx

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Tactic:
have :=
    summable_sum_mul_antidiagonal_of_summable_mul
      (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
  refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)
  calc
    ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ :=
      norm_sum_le _ _
    _ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
hC₁ : C₁ ≤ max C₀ C₁
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
← hC₁

Goal state after:
case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
hC₁ : C₁ ≤ max C₀ C₁
⊢ ‖f m‖ ≤ C₁ * ‖g m‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq abs fun m ↦ ∑ n ∈ range m, a * x ^ n

Tactic:
by
  simpa [mul_sum, Pi.mul_def] using (const a).mul (geo_series x hx1)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ)

Tactic:
exact ih _ h _ (by simp) rfl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Filter.map Subtype.val atBot = 𝓝[>] 0

Tactic:
← map_coe_Ioi_atBot

Goal state after:
⊢ Filter.map Subtype.val atBot = Filter.map Subtype.val atBot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = √(1 - cos x ^ 2)

Tactic:
by
  rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]

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

Goal state before:
pp: x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) = -√((1 - cos x) / 2)

Tactic:
rw [← abs_sin_half, abs_of_nonpos, neg_neg]
  apply sin_nonpos_of_nonpos_of_neg_pi_le <;> linarith

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

Goal state before:
pp: ⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2

Tactic:
trans cos (π / 2 ^ 4)

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

⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ HasSum (fun b ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)

Tactic:
convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)

Goal state after:
case e'_6
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ 1 = ∑ i ∈ Finset.range 1, ‖x‖ ^ i
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
U : Set Y
inst✝ : CompactSpace X
hU : IsOpen[inst✝¹] U
⊢ IsOpen {f | range ⇑f ⊆ U}

Tactic:
simp_rw [← mapsTo_univ_iff_range_subset]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
U : Set Y
inst✝ : CompactSpace X
hU : IsOpen[inst✝¹] U
⊢ IsOpen {f | MapsTo (⇑f) univ U}
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
⊢ ∀ (x : X × C(Y, Z)), Tendsto (fun p ↦ (const Y p.1).prodMk p.2) (𝓝 x) (𝓝 ((const Y x.1).prodMk x.2))

Tactic:
ContinuousMap.tendsto_nhds_compactOpen

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ ∀ (x : X × C(Y, Z)) (K : Set Y),
    IsCompact K →
      ∀ (U : Set (X × Z)),
        IsOpen[instTopologicalSpaceProd] U →
          MapsTo (⇑((const Y x.1).prodMk x.2)) K U →
            ∀ᶠ (a : X × C(Y, Z)) in 𝓝 x, MapsTo (⇑((const Y a.1).prodMk a.2)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z

Tactic:
obtain ⟨hx, hy⟩ := hyz.mem

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx✝ : x ∈ F
hy✝ hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ¬Summable f

Tactic:
refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
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
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst✝²] (Function.uncurry fun x y ↦ x.uncurry y)

Tactic:
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst✝²]
    ((Function.uncurry fun x y ↦ x.uncurry y) ∘ ⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y))
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ ⇑(γ.map h) = f ∘ ⇑γ

Tactic:
ext t
  rfl

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
by
  rcases h.lt_or_gt with (h_neg | h_pos)
  · exact continuousAt_sign_of_neg h_neg
  · exact continuousAt_sign_of_pos h_pos

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

Goal state before:
pp: x : ℝ
⊢ arccos x ≤ π / 4 ↔ √2 / 2 ≤ x

Tactic:
by
  rw [arccos, ← pi_div_four_le_arcsin]
  constructor <;>
    · intro
      linarith

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

Goal state before:
pp: x : ℝ
⊢ log |x| = log x

Tactic:
by_cases h : x = 0

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ log |x| = log x

case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y

Tactic:
by
  simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm,
    div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx), true_and]
  rw [← ofReal_div, arg_real_mul]
  exact div_pos (norm_pos_iff.mpr hy) (norm_pos_iff.mpr hx)

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

Goal state before:
pp: x : ℂ
⊢ Real.tan x.arg = x.im / x.re

Tactic:
by_cases h : x = 0

Goal state after:
case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℤ
hn : n < 0
⊢ 1 ≤ -↑n

Tactic:
rw [← neg_zero, ← lt_neg] at hn

Goal state after:
n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
by
  have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves]
  nth_rw 1 [h]
  rw [coe_nsmul, two_nsmul_eq_iff]
  apply iff_of_eq -- `congr` only works on `Eq`, so rewrite from `Iff` to `Eq`.
  congr
  rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]

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

Goal state before:
pp: x a : ℂ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_cpow_eq_iff, eq_comm]

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

Goal state before:
pp: case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

Tactic:
rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]

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

Goal state before:
pp: θ : Angle
⊢ (θ - ↑(π / 2)).sin = -θ.cos

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

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
by
  simp_rw [two_zsmul, ← two_nsmul] at h
  exact abs_cos_eq_of_two_nsmul_eq h

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

Goal state before:
pp: case mpr
θ : Angle
h : θ ≠ ↑π
h' : θ.toReal ≠ π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π

Tactic:
exact ⟨(toReal_le_pi θ).lt_of_ne h', by linarith [neg_pi_lt_toReal θ]⟩

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

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π

Tactic:
exact ⟨fun h => ⟨by linarith, by linarith⟩, fun h => ⟨by linarith, by linarith⟩⟩

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

Goal state before:
pp: case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ

Tactic:
simp [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr]

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).arg = ↑x.arg + ↑y.arg

Tactic:
by
  convert!
    arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy))
      (arg x + arg y : Real.Angle) using 3
  simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin,
    cos_add_sin_I, ofReal_add, add_mul, exp_add, ofReal_mul]
  rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]

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

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ (-↑θ).sign ≤ 0

Tactic:
rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]
  exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

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

Goal state before:
pp: case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
by_cases h : x = 0

Goal state after:
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by_cases h : x = 0

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ 0 ^ x ≤ 1

case neg
x : ℝ
h : ¬x = 0
⊢ 0 ^ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ 0 ≤ 0 ^ x

Tactic:
by_cases h : x = 0

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ 0 ≤ 0 ^ x

case neg
x : ℝ
h : ¬x = 0
⊢ 0 ≤ 0 ^ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
· rcases eq_or_ne y 0 with (rfl | hy) <;> simp [*]

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ).sign ≠ (-(θ + ψ)).sign

Tactic:
sign_neg,

Goal state after:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ -θ.sign ≠ (-(θ + ψ)).sign
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ -θ.sign ≠ (-(θ + ψ)).sign

Tactic:
sign_neg,

Goal state after:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ -θ.sign ≠ -(θ + ψ).sign
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖↑t ^ c‖ = t ^ c.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ht]

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

Goal state before:
pp: p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ cexp (Complex.log x.1 * x.2)

Tactic:
suffices IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ from
    mem_nhds_iff.mpr ⟨_, fun x hx ↦ by simp_all [cpow_def_of_ne_zero], this, hp_fst⟩

Goal state after:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen {x | x.1 = 0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
ha,

Goal state after:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ 0 ^ x) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
have := hx.trans_le hxy

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ y ^ z ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
simp only [← not_le, le_rpow_inv_iff hz]

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

Goal state before:
pp: case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
· simp +contextual [hz]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

pp: case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
· simp [H, zero_rpow_of_pos]

Goal state after:
case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
by_cases h : x = 0

Goal state after:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
by_cases h : x = 0

Goal state after:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
by_cases h : x = 0

Goal state after:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
y z : ℝ
x : ℝ≥0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
by_cases h : x = 0

Goal state after:
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
simp only [← not_le, le_rpow_inv_iff hz]

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

Goal state before:
pp: y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
by_cases h : x = 0

Goal state after:
case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
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
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
⊢ p ∈ s₁ ↔ p ∈ s₂

Tactic:
have hq1 := Set.mem_of_mem_inter_left hn.some_mem

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
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
⊢ p ∈ s₁ ↔ p ∈ s₂
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ a * x + 0 * y ∈ Ico x y

Tactic:
rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]

Goal state after: