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

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ unitary A ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
rw [Unitary.mem_iff]
  refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩
  · have : IsStarNormal x := ⟨h.trans h'.symm⟩
    exact ⟨this, by simp [sq, ← star_mul_self_eq_realPart_sq_add_imaginaryPart_sq x, h]⟩
  · simp [← hx.star_comm_self.eq, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← sq, h]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (codRestrict (e.source.domRestrict ↑e.toPartialEquiv) e.target ⋯)

Tactic:
rw [← PartialEquiv.toEquiv_eq_codRestrict_restrict]

Goal state after:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing ⇑e.toEquiv
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (⇑e.toHomeomorphSourceTarget) (comap Subtype.val (𝓝 ↑(e.toHomeomorphSourceTarget x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))

Tactic:
simp only [Function.comp_def, toHomeomorphSourceTarget_apply_coe, comap_comap]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
by
  rw [pos_iff_exists_ofReal] at hz
  obtain ⟨x, hx, hx'⟩ := hz
  rw [← hx', ← ofReal_inv, ofReal_pos]
  exact inv_pos_of_pos hx

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
⊢ (⋯ ▸
        let __spread.0 := h.toNormedField;
        re)
      I =
    0

Tactic:
exact h.I_re_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
rw [isBigO_iff]

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
by
  simp only [isLittleO_iff, eventually_prod_iff]
  exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖f' x‖) ↔ f =o[l] f'

Tactic:
isLittleO_norm_right

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f =o[l] f' ↔ f =o[l] f'
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

pp: case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Tactic:
· simp

Goal state after:
case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ Ico n j
⊢ i - n ≤ i

Tactic:
· simp

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

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
this : Complex.cos ↑x ≠ 0
⊢ ↑(1 + tan x ^ 2)⁻¹ = ↑(cos x ^ 2)

Tactic:
by simpa using Complex.inv_one_add_tan_sq this

Goal state after:
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 : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
rw [isBigO_iff]

Goal state after:
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 : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖1 * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖

Tactic:
← exp_zero

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp 0 * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
hb : b ≠ 0
m : ℕ
⊢ a ^ ofNat m = -b ^ ofNat m ↔ a = -b ∧ Odd (ofNat m)

Tactic:
by
    simp [pow_eq_neg_pow_iff, hb]

Goal state after:
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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ n₁ ≤ n

Tactic:
by grind

Goal state after:
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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ max C₀ C₁ ≥ C₀

Tactic:
by grind

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

Goal state before:
pp: case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ rexp 0 ≤ 1 / (1 - 0)

pp: case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
· simp

Goal state after:
case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inl
⊢ 0 + 1 ≤ rexp 0

pp: case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
· simp

Goal state after:
case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
⊢ -1 ≤ ↑n

Tactic:
by grind

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

Goal state before:
pp: case e'_4
n : ℕ
⊢ rexp 1 = rexp (- -1)

Tactic:
· simp

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 ≤ x / 2

Tactic:
by grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ x / 2 ≤ 1

Tactic:
by grind

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

Goal state before:
pp: case inl
hx : 0 ≤ 0
hx' : 0 < 2
⊢ rexp 0 ≤ (2 + 0) / (2 - 0)

pp: case inr
x : ℝ
hx : 0 ≤ x
hx' : x < 2
hx₀ : 0 < x
⊢ rexp x ≤ (2 + x) / (2 - x)

Tactic:
· simp

Goal state after:
case inr
x : ℝ
hx : 0 ≤ x
hx' : x < 2
hx₀ : 0 < x
⊢ rexp x ≤ (2 + x) / (2 - x)
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 1 ^ k < (rexp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * π) + π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

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
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε

Tactic:
by
      have := (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp
        ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε
      simp only [mem_ball, dist, abs_sub_lt_iff] at this
      rcases this with ⟨δ, hδ, h⟩
      obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ
      specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩
      calc
        _ ≤ ‖k‖ * ‖a‖ := (norm_mk_le ..).trans (norm_smul_le k a)
        _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

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

Goal state before:

Tactic:
_ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
      _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

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

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
⊢ ‖0‖₊ • ediam ∅ ≤ ediam (0 • ∅)

pp: case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
s : Set E
hs : s.Nonempty
⊢ ‖0‖₊ • ediam s ≤ ediam (0 • s)

Tactic:
· simp

Goal state after:
case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
s : Set E
hs : s.Nonempty
⊢ ‖0‖₊ • ediam s ≤ ediam (0 • s)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) \ interior (ball x r) = sphere x r

Tactic:
closure_ball x hr,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closedBall x r \ interior (ball x r) = sphere x r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
· simp

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

Goal state before:
pp: ⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
· simp

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

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

Tactic:
· simp

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

Goal state before:
pp: ⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
· simp

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

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

Tactic:
· simp

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

Goal state before:
pp: ⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
· simp

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

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

Tactic:
· simp

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

Goal state before:
pp: ⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
· simp

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

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

Tactic:
set c := cos θ

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : ℝ≥0∞
h : edist x z < r
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < r

Tactic:
cases r with

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))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
    ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n

Tactic:
apply Finset.sum_congr rfl (fun i hi ↦ ?_)

Goal state after:
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 ∈ Finset.range (n + 1)
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

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
U : Set Y
inst✝ : CompactSpace X
hU : IsOpen[inst✝¹] U
⊢ IsOpen {f | range ⇑f ⊆ U}

Tactic:
← 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.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
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i

Tactic:
have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _

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
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f

Tactic:
by_cases! hr₀ : 0 ≤ r

Goal state after:
case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
Module: Mathlib.Topology.Path

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

Tactic:
by grind

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
cases p using snocCases with | _ p x => ?_
  simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe,
    Path.target_mem_range, and_true] at hp ⊢
  obtain ⟨hp, hx⟩ := hp
  induction p using snocInduction generalizing x with
  | elim0 =>
    simp only [snoc_zero]
    use Path.refl x
    simp [hx]
  | @snoc n p y hp₂ =>
    simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
    obtain ⟨hp, hy⟩ := hp
    specialize hp₂ y hp hy
    obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
    obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
    rw [← range_subset_iff] at hγ₁
    use γ₀.trans γ₁
    simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]
    tauto

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (range f)

Tactic:
← image_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (f '' univ)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x : (i : ι) → Z i
hx : ∀ (i : ι), x i ∈ s i
hjoin : ∀ (i : ι) ⦃y : Z i⦄, y ∈ s i → JoinedIn (s i) (x i) y
y : (i : ι) → Z i
hy : y ∈ univ.pi s
i : ι
⊢ y i ∈ s i

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑x.val / ↑N = ↑y.val / ↑N
this : 0 < ↑N
⊢ x = y

pp: case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ

Tactic:
div_left_inj' this.ne',

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑x.val = ↑y.val
this : 0 < ↑N
⊢ x = y

case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
p x : ℝ
⊢ ‖↑(0 * x)‖ = |0| * ‖↑x‖

pp: case inr
p x t : ℝ
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖

Tactic:
· simp

Goal state after:
case inr
p x t : ℝ
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (0⁻¹ * x)) * 0|

pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
· simp

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
abs_inv,

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p|⁻¹ * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
⊢ ‖↑(0 / 2)‖ = |0| / 2

pp: case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
· simp

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + 0 • p - ε) (x + 0 • p + ε) ∩ s = if 0 = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

pp: case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Tactic:
· simp

Goal state after:
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ ↑‖0‖ * cexp (↑(arg 0) * I) = 0

pp: case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
· simp

Goal state after:
case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
sub_eq_iff_eq_add,

Goal state after:
x : ℝ
⊢ π / 2 = π + arcsin x ↔ x ≤ -1
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 : α
⊢ ‖f x • g x‖ ≤ c → c / ε ≤ ‖f x‖ → f x ≠ 0 → g x ∈ closedBall 0 ε

Tactic:
hfgc

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
⊢ c / ε ≤ ‖f x‖ → f x ≠ 0 → g x ∈ closedBall 0 ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

pp: case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
· simp

Goal state after:
case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im