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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr with i hi
      · rw [Complex.norm_pow]
      · simp

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 : ℕ) in atTop, g n = 0 → f n = 0

Tactic:
filter_upwards [hf, hg]; grind

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

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ ↑⌈x⌉₊ ^ n

Tactic:
by gcongr; exact Nat.le_ceil _

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

Goal state before:
pp: α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ⟨rexp x, ⋯⟩) atTop atTop

Tactic:
rw [tendsto_Ioi_atTop]

Goal state after:
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑⟨rexp x, ⋯⟩) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ rexp (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
← comp_apply (f := exp),

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (rexp ∘ f) x) l atTop ↔ Tendsto f l atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

Tactic:
← comp_apply (f := exp),

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (rexp ∘ f) x) l (𝓝 0) ↔ Tendsto f l atBot
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * π ≠ x

Tactic:
contrapose!

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ ∃ n, ↑n * π = x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
← comp_apply (f := exp),

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ (cexp ∘ f) x) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x ↦ (f x).re) l atBot
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ ‖↑m‖ = 0 ↔ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S

Tactic:
rw [norm_mk, ← mem_closure_iff_infDist_zero]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ (↑S).Nonempty
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * ball y⁻¹ δ = ball (x * y⁻¹) δ

Tactic:
singleton_mul_ball

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Tactic:
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
    rw [Set.image_nonempty]
    exact ⟨0, f.ker.zero_mem⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ

Tactic:
simp_rw [singleton_mul_ball, mul_one]

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:
by
    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.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ * c < r * 1

Tactic:
apply mul_lt_mul' <;> assumption

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

Goal state before:
pp: R : Type u_2
inst✝ : SeminormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0)

Tactic:
by
  apply squeeze_zero_norm' (eventually_norm_pow_le x)
  exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
⊢ Tendsto (fun n ↦ v (1 / (1 + a ^ n))) atTop (𝓝 1)

Tactic:
simp_rw [map_div₀ v, v.map_one]

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
⊢ Tendsto (fun n ↦ 1 / v (1 + a ^ n)) atTop (𝓝 1)
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))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Tactic:
rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEDist_cthickening]

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable fun b ↦ ↑(a i) * ↑b ^ i * r ^ b

Tactic:
simp_rw [mul_assoc]

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable fun b ↦ ↑(a i) * (↑b ^ i * r ^ b)
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
h : (fun γ ↦ ⇑γ.toContinuousMap) γ₁ = (fun γ ↦ ⇑γ.toContinuousMap) γ₂
⊢ γ₁ = γ₂

Tactic:
simp only [DFunLike.coe_fn_eq] at h

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : γ₁.toContinuousMap = γ₂.toContinuousMap
⊢ γ₁ = γ₂
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦
    f (n.succ - 1) • ∑ i ∈ Finset.range n.succ, z i +
      -∑ x ∈ Finset.range (n.succ - 1), (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i

Tactic:
Nat.succ_sub_succ_eq_sub,

Goal state after:
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦
    f (n - 0) • ∑ i ∈ Finset.range n.succ, z i +
      -∑ x ∈ Finset.range (n - 0), (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ (fun x ↦ 1) =ᶠ[nhds a] ⇑SignType.sign

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∀ᶠ (x : α) in nhds a, 1 = SignType.sign x
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
⊢ (fun x ↦ -1) =ᶠ[nhds a] ⇑SignType.sign

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∀ᶠ (x : α) in nhds a, -1 = SignType.sign x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg

Tactic:
contrapose!

Goal state after:
z : ℂ
h₀ : z ≠ 0
⊢ z.arg < 0 → Real.sin z.arg < 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
h : log x < y
⊢ x < rexp y

Tactic:
by
  rcases le_or_gt x 0 with hx | hx
  · exact hx.trans_lt <| exp_pos y
  · exact (log_lt_iff_lt_exp hx).mp h

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x

Tactic:
rw [← not_lt, log_neg_iff hx, not_lt]

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

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

Tactic:
← neg_zero,

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

Goal state before:
pp: case mp.inl
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h

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

Goal state before:
pp: case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2) = ↑(-π / 2)

Tactic:
← sub_eq_zero,

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2) - ↑(-π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← sub_eq_zero,

Goal state after:
case mp
θ ψ : ℝ
Hcos : cos θ - cos ψ = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x

Tactic:
· have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop
    refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)
    exact continuousAt_arg h

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

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

Tactic:
← sub_eq_zero,

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ cos θ - cos ψ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← sub_eq_zero,

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ - cos ψ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← sub_eq_zero,

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ sin θ - sin ψ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ

Tactic:
← sub_eq_zero,

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

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -1 * π
⊢ ↑θ = ↑ψ

Tactic:
← sub_eq_zero,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) - -1 * π = 0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
toReal_coe_eq_self_iff

Goal state after:
⊢ -π < 0 ∧ 0 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
toReal_coe_eq_self_iff

Goal state after:
⊢ -π < π ∧ π ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(-θ.toReal)).toReal = -θ.toReal ↔ θ ≠ ↑π

Tactic:
toReal_coe_eq_self_iff

Goal state after:
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
contrapose!

Goal state after:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ rexp (x * y) = rexp x ^ y

Tactic:
by rw [rpow_def_of_pos (exp_pos _), log_exp]

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

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (↑(θ.toReal + ψ.toReal)).toReal = θ.toReal + ψ.toReal

Tactic:
toReal_coe_eq_self_iff

Goal state after:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ x ^ z = x ^ 0 * x ^ z

Tactic:
rpow_zero,

Goal state after:
case inl
x z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ x ^ z = 1 * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y

Tactic:
by
  simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]; split_ifs <;>
    simp [Complex.ofReal_log hx]

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

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
by
  repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
  rw [exp_lt_exp]; exact mul_lt_mul_of_pos_left hyz (log_pos hx)

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

Goal state before:
pp: case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z

Tactic:
rpow_zero,

Goal state after:
case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = 1 * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * ∞ ^ 0

Tactic:
rpow_zero,

Goal state after:
case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y z : ℝ
hyz : 0 < y + z
hx : 0 ≠ ∞
hy' : ¬0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
have hz' : 0 < z := by linarith
      simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']

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

Goal state before:
pp: p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
⊢ 0 < x ^ p

Tactic:
by_cases hp_zero : p = 0

Goal state after:
case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
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 y : P
⊢ ((⅟2 • (y -ᵥ x) +ᵥ x) -ᵥ x) +ᵥ ⅟2 • (y -ᵥ x) +ᵥ x = y

Tactic:
vadd_vsub,

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 y : P
⊢ ⅟2 • (y -ᵥ x) +ᵥ ⅟2 • (y -ᵥ x) +ᵥ x = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
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
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0

Tactic:
← sub_eq_zero,

Goal state after:
case inr.inr
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
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x - r₂ • r • x = 0
⊢ x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
⊢ x • -(p₁ - p₀) ≤ -(y • (p₁ - p₀))

Tactic:
← smul_neg

Goal state after:
k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
⊢ x • -(p₁ - p₀) ≤ y • -(p₁ - p₀)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
⊢ z ∈ [c -[𝕜] x] ∩ [c -[𝕜] y] → z ∈ {c}

Tactic:
⟨hzt, hzs⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
⊢ z ∈ {c}
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x

Tactic:
eq_comm (a := x)

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
eq_comm (a := x)

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x

Tactic:
eq_comm (a := x)

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
⊢ a ∈ Icc x y → a ∈ [x -[{ t // 0 ≤ t }] y]

Tactic:
⟨hxa, hay⟩

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : x ≤ a
hay : a ≤ y
⊢ a ∈ [x -[{ t // 0 ≤ t }] y]
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ 2⁻¹ • s + 2⁻¹ • s = s

Tactic:
rw [← h_conv.add_smul (by norm_num) (by norm_num)]
  ring_nf
  rw [one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s = {x}

Tactic:
rw [← Set.Nonempty.subset_singleton_iff, ← hs]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s ⊆ (convexHull 𝕜) s

𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s.Nonempty