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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ 0 < re z ∧ im z = 0

Tactic:
by
  simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
z : K
h : I = 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
simp [h, im_eq_zero]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          I =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        z

Tactic:
exact h.mul_im_I_ax

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁷ : RCLike K
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] W
x✝ : V
⊢ ‖(Unitary.toUnits α • e.toLinearEquiv) x✝‖ = ‖x✝‖

Tactic:
by simp [norm_smul]

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ IsNat (n.descFactorial l) 0

Tactic:
by
  constructor
  simp [h₁.out, h₂.out, h₃]

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

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Tactic:
simp only [IsLittleO_def]
    rintro ⟨φ, hφ, huvφ⟩ c hpos
    rw [NormedAddGroup.tendsto_nhds_zero] at hφ
    exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
norm_add_le

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0

Tactic:
refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 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‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ ≤ C₁ * ‖g m‖

Tactic:
calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)

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

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
hnrec : ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
obtain ⟨C₀, hnrec⟩ := hnrec

Goal state after:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun n ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
refine (IsLittleO.of_norm_left ?_).of_norm_right
  exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded (image2 (fun a x ↦ x * a) t s)

Tactic:
image2_swap

Goal state after:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded (image2 (fun a b ↦ a * b) s t)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖(lift S f.toAddMonoidHom hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖

Tactic:
simpa [h] using le_opNorm f x

Goal state after:
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‖ * ‖x - y‖ = (1 - r) * dist y x

Tactic:
by
      rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 2 * c = 4 * c ^ 2 - 1
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z < ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le)
    (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
      rw [← add_div, div_self (add_pos hε hδ).ne']).imp
    fun y hy => ?_
  rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
  rw [← div_lt_one (add_pos hε hδ)] at h
  exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩

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

Goal state before:
pp: x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < tan x

Tactic:
rw [tan_eq_sin_div_cos]
  exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Tactic:
refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩
  rw [add_comm] at hxy
  obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
  rw [dist_comm] at hxz
  exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n

Tactic:
rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ]

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x

Tactic:
· intro h'
    rw [pathComponent_symm]
    exact (h.trans h').symm

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
Module: Mathlib.Topology.Instances.ZMultiples

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

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)

case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ toAddCircle ↑j = ↑(↑j / ↑N)

Tactic:
by
  simp [toAddCircle]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ ‖z‖ < ‖1‖

Tactic:
by simp [hz]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ y ∈ t, -1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

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 (↑1) t₀) t₁) = γ.extend t₁

Tactic:
simp only [min_def, max_def']
    split_ifs with h₁ h₂ h₃
    · simp [γ.extend_of_one_le h₂]
    · rfl
    · have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
      simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]
    · rfl

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-1) 1
⊢ sin (arcsin x) = x

Tactic:
by
  simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
    Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)

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

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

Tactic:
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp

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

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

Tactic:
have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp

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

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

Tactic:
linarith [neg_pi_div_two_le_arcsin x]

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

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
Set.mem_Icc,

Goal state after:
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : ¬(-(π / 2) ≤ θ ∧ θ ≤ π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arccos x < π ↔ -1 < x

Tactic:
grind [arccos_le_pi, arccos_eq_pi]

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

Goal state before:
pp: θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (1 * (cos ↑θ + sin ↑θ * I)).arg = θ

Tactic:
← ofReal_one,

Goal state after:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (↑1 * (cos ↑θ + sin ↑θ * I)).arg = θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ rexp (log x) = |x|

Tactic:
by
  rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]

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
⊢ ‖g x‖ ≤ c / ‖f x‖

Tactic:
rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin ↑z.arg * I)).arg ∈ Ioc (-π) π

Tactic:
← sin_add_int_mul_two_pi _ N

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
· obtain ⟨x, y⟩ := z
    rintro ⟨rfl : x = 0, hy : 0 < y⟩
    rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

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

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

Tactic:
NormNum.IsNat.to_eq h rfl

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

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

Tactic:
NormNum.IsNat.to_eq h rfl

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ

Tactic:
rw [coe_sub, coe_sub] at h

Goal state after:
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n

Tactic:
rw [inv_cpow _ _ h]

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

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

Tactic:
· intro h
    rw [neg_lt_neg_iff]
    have h' : θ.toReal ≠ π := by simp [h]
    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: θ : Angle
h : π / 2 < θ.toReal
⊢ 2 * θ.toReal ≤ 3 * π

Tactic:
by linarith [pi_pos, toReal_le_pi θ]

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

Goal state before:
pp: θ : ℝ
⊢ (1 * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
← ofReal_one,

Goal state after:
θ : ℝ
⊢ (↑1 * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : ℝ
⊢ (1 * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
← ofReal_one,

Goal state after:
θ : ℝ
⊢ (↑1 * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : Real.Angle
⊢ ↑(1 * (↑θ.cos + ↑θ.sin * I)).arg = θ

Tactic:
← ofReal_one,

Goal state after:
θ : Real.Angle
⊢ ↑(↑1 * (↑θ.cos + ↑θ.sin * I)).arg = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
by grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]

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

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

Tactic:
exp_log (rpow_pos_of_pos hx y),

Goal state after:
x : ℝ
hx : 0 < x
y : ℝ
⊢ x ^ y = rexp (y * log x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by
  rw [← rpow_le_rpow_iff hx _ hz, rpow_inv_rpow] <;> positivity

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

Goal state before:
pp: p : ℂ × ℂ
h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0
h₂ : 0 < p.2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) p

Tactic:
by
  obtain ⟨z, w⟩ := p
  rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
    not_le_zero_iff] at h₁
  rcases h₁ with (h₁ | (rfl : z = 0))
  exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
hx : x ≠ 0
hx' : x ≠ ∞
⊢ x ^ y ≠ ∞

Tactic:
by
  simp [rpow_eq_top_iff, hx, hx']

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

Goal state before:
pp: case inr.inr.top
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

pp: case inr.inr.coe
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x✝ : ℝ≥0
hxy : ↑x✝ ≤ y
hx0 : ↑x✝ ≠ 0
⊢ (↑x✝ * y) ^ z = if (↑x✝ = 0 ∧ y = ∞ ∨ ↑x✝ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * y ^ z

Tactic:
· rcases hz with hz | hz <;> simp [hz, top_unique hxy]

Goal state after:
case inr.inr.coe
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x✝ : ℝ≥0
hxy : ↑x✝ ≤ y
hx0 : ↑x✝ ≠ 0
⊢ (↑x✝ * y) ^ z = if (↑x✝ = 0 ∧ y = ∞ ∨ ↑x✝ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
replace hy := hy.lt_or_gt

Goal state after:
case inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rcases eq_or_ne x ⊤ with (rfl | h_top)

Goal state after:
case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ∞ ≠ 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by simp [hz]

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

Goal state before:
pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p

Tactic:
← Ne

Goal state after:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
linarith [pi_pos, neg_pi_lt_arg x]

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

Goal state before:
pp: x p : ℝ
hx_pos : 0 < x
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp_rw [ENNReal.ofReal]

Goal state after:
x p : ℝ
hx_pos : 0 < x
⊢ ↑x.toNNReal ^ p = ↑(x ^ p).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
← Ne

Goal state after:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

pp: case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
· rw [← Ne] at hp0
    have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
    simp [hx0, hp_pos, hp_pos.ne.symm]

Goal state after:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
← Ne

Goal state after:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ b = a ^ n

Tactic:
h.1,

Goal state after:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ ↑n = a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
h.1,

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

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
⊢ a ^ b = a ^ n

Tactic:
h.1,

Goal state after:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
⊢ a ^ ↑n = a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
h.1,

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

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

Tactic:
by
  suffices IsNNRat (nr / dr : ℝ≥0) nr dr by
    simpa [ha.to_eq, NNReal.div_rpow, hnum.1, hden.1]
  apply IsNNRat.of_raw
  simp [← hden.1, ha.den_nz]

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

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

Tactic:
simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]

Goal state after: