mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
geom_sum_inv h₁ h₂,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ)) =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ)) * (↑n.factorial * ↑n) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
mul_comm _ (n.factorial * n : α),

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * ((↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ))) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
⊢ HasSum (fun x ↦ f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Tactic:
apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop

Goal state after:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := ⋯
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Tactic:
simpa only using! hr

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

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖

Tactic:
have hy_eq : y = x + (y - x) := by abel

Goal state after:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
⊢ ((fun x ↦ rexp (f x)) =Θ[l] fun x ↦ rexp (g x)) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |f x - g x|

Tactic:
by
  simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta,
    isBigO_exp_comp_exp_comp, Pi.sub_def]

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

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =o[atTop] fun x ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n

Tactic:
refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
    rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ c = (1 + √5) / 4

Tactic:
have hd : discrim 4 (-2) (-1) = (2 * √5) * (2 * √5) := by norm_num [discrim, mul_mul_mul_comm]

Goal state after:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ c = (1 + √5) / 4
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 : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
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 : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ↑(Units.oneSub x h)⁻¹ = (1 - x)⁻¹ʳ

Tactic:
← Ring.inverse_unit

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (↑(Units.oneSub x h))⁻¹ʳ = (1 - x)⁻¹ʳ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

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

Tactic:
rw [infEDist_zero_of_mem, tsub_eq_zero_of_le hs.le]
    exact hs

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

Goal state before:
pp: 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))
n : ℕ
hn : k < n
⊢ (n + k).choose k ≤ 2 ^ k * n ^ k

Tactic:
calc (n + k).choose k
          _ ≤ (2 * n).choose k := choose_le_choose k (by lia)
          _ ≤ (2 * n) ^ k := Nat.choose_le_pow _ _
          _ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ ⨅ x, ⨅ (_ : IsCompact x.1 ∧ IsOpen[inst✝] x.2 ∧ MapsTo (⇑f) x.1 x.2), 𝓟 {g | MapsTo (⇑g) x.1 x.2} ↔
    ∃ i,
      (i.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) ∧
        ⋂ KU ∈ i, {g | MapsTo (⇑g) KU.1 KU.2} ⊆ s

Tactic:
simp [mem_biInf_principal, and_assoc]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ ofLine ⋯ ⋯ ⋯ = γ

Tactic:
ext t
  simp [ofLine]

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

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

Tactic:
obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂

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

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

Tactic:
split_ifs with h h₁ h₂ <;> rw [coe_symm_eq] at h

Goal state after:
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, ⋯⟩)

case neg
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 - 1, ⋯⟩)

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) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
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) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
⊢ CompactSpace (AddCircle p)

Tactic:
rw [← isCompact_univ_iff, ← coe_image_Icc_eq p 0]

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
⊢ IsCompact (QuotientAddGroup.mk '' Icc 0 (0 + p))
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ (refl x).reparam f hfcont hf₀ hf₁ = refl x

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case pos
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:
rw [if_pos]
    exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]

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

Goal state before:
pp: x : ℝ
⊢ Summable fun n ↦ x ^ n / ↑n !

Tactic:
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n ↦ x ^ n / ↑n !
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‖
⊢ f x ≠ 0 → g x ∈ closedBall 0 ε

Tactic:
hf0

Goal state after:
α : 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
⊢ g x ∈ closedBall 0 ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
by_cases h₀ : z = 0

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
by_cases h₀ : z = 0

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
by_cases h₀ : z = 0

Goal state after:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ ↑(Real.log (rexp x.re)) + ↑(cexp x).arg * I = x

Tactic:
Real.log_exp,

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

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

Tactic:
Real.log_exp,

Goal state after:
x : ℂ
⊢ ↑x.re + ↑(cexp x).arg * I = ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
by
  simpa only [not_or] using log_eq_zero.not

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)

Tactic:
← mul_comm (2 * π * I),

Goal state after:
k N : ℕ
hN : N ≠ 0
n : ℤ
| 2 * ↑π * I * ↑k / ↑N = 2 * ↑π * I * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case pos
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∃ w, cexp w = z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
rcases h with ⟨w, rfl⟩

Goal state after:
case pos
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (cexp ⁻¹' {cexp w}).Countable
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

Tactic:
· rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_cpow h
    · exact cpow_zero _

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

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < ↑n * x.arg
hle : ↑n * x.arg ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
rw [mul_comm] at hlt hle
  rw [cpow_mul, cpow_intCast] <;> simpa [log_im]

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

Goal state before:
pp: case mp.refine_2
θ : ℝ
⊢ cexp (↑(toIocMod ⋯ (-π) θ) * I) = cexp (↑θ * I)

Tactic:
eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ,

Goal state after:
case mp.refine_2
θ : ℝ
⊢ cexp (↑(θ - toIocDiv ⋯ (-π) θ • (2 * π)) * I) = cexp (↑θ * I)
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 ↔ 0 ≤ z.im

Tactic:
simp only [him.not_ge]
    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]
    exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

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

Goal state before:
pp: ⊢ (↑0).sin = 0

Tactic:
sin_coe,

Goal state after:
⊢ Real.sin 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑π).sin = 0

Tactic:
sin_coe,

Goal state after:
⊢ Real.sin π = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.succ
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : ↑(x ^ n).arg = n • ↑x.arg
⊢ n • ↑x.arg + ↑x.arg = (n + 1) • ↑x.arg

Tactic:
succ_nsmul

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

Goal state before:
pp: x : ℝ
⊢ (↑x).sin / (↑x).cos = Real.tan x

Tactic:
sin_coe,

Goal state after:
x : ℝ
⊢ Real.sin x / (↑x).cos = Real.tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: x : ℝ
⊢ (↑x).tan = Real.tan x

Tactic:
by
  rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]

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

Goal state before:
pp: ⊢ SignType.sign (↑(π / 2)).sin = 1

Tactic:
sin_coe,

Goal state after:
⊢ SignType.sign (Real.sin (π / 2)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ SignType.sign (↑(-π / 2)).sin = -1

Tactic:
sin_coe,

Goal state after:
⊢ SignType.sign (Real.sin (-π / 2)) = -1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ rexp (log x * y)

Tactic:
abs_mul,

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y)| * |cos (y * π)| ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0
ha : ↑a ∈ Set.Ioi ↑c
⊢ ↑x < ↑a ^ y

Tactic:
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc

Goal state after:
case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
⊢ ↑x < ↑a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p

Tactic:
intro p hp_pos

Goal state after:
p✝ : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rw [ne_eq, coe_eq_zero] at hx0

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

Goal state before:
pp: x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |t * (log x * x ^ t)| < 1
⊢ |log x * x ^ t| * t < 1

Tactic:
abs_mul,

Goal state after:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |t| * |log x * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : y = z
⊢ x ^ y = x ^ z

Tactic:
rw [H]

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

Goal state before:
pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

pp: case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
· rwa [arg_nonneg_iff]

Goal state after:
case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
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:
rw [← Ne] at hp_zero
    have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
    rw [← zero_rpow_of_pos hp_pos]
    exact rpow_lt_rpow hx_pos hp_pos

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

Goal state before:
pp: x : ℂ
⊢ |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)

Tactic:
abs_mul,

Goal state after:
x : ℂ
⊢ |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i

Tactic:
obtain ⟨i, hy⟩ := hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ y ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
by rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x -[𝕜] y]

Tactic:
← sub_nonneg

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x -[𝕜] y]
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 : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
⊢ v +ᵥ p ∈ s ↔ p ∈ s

Tactic:
by
  refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩
  convert! vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h
  simp

Goal state after:
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v +ᵥ p ∈ s₁ ⊓ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂

Tactic:
mem_inf_iff

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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ b • x ∈ s

Tactic:
calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]

Goal state after: