awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : √π ≠ 0
h :
  ∀ (n : ℕ),
    HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ))
        (fun (n : ℕ) ↦ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) n =
      HDiv.hDiv (β := ℕ → ℝ) stirlingSeq (fun (x : ℕ) ↦ √π) n
⊢ (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) =
    stirlingSeq / fun (x : ℕ) ↦ √π

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : √π ≠ 0
n : ℕ
⊢ HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ))
      (fun (n : ℕ) ↦ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) n =
    HDiv.hDiv (β := ℕ → ℝ) stirlingSeq (fun (x : ℕ) ↦ √π) n

Tactic:
simp [field, stirlingSeq, mul_right_comm]

Premises used: Stirling.stirlingSeq, mul_right_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ √π ≤ stirlingSeq n

Tactic:
match n, hn with
  | n + 1, _ =>
    stirlingSeq'_antitone.le_of_tendsto (b := n) <|
      tendsto_stirlingSeq_sqrt_pi.comp (tendsto_add_atTop_nat 1)

Premises used: Real.pi, Stirling.stirlingSeq'_antitone, LE.le, Stirling.stirlingSeq, Antitone.le_of_tendsto, Real.sqrt, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat, Stirling.tendsto_stirlingSeq_sqrt_pi, _private.0.Stirling.sqrt_pi_le_stirlingSeq.match_1
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
inl : √(2 * π * (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0 ≤ (↑0! : ℝ)
inr : ∀ (hn : n ≠ 0), √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ √(2 * π * (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0 ≤ (↑0! : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
simp : √2 * √π * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√2 * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
simp [sqrt_mul']

Premises used: Real.sqrt_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ √2 * √π * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√2 * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by
    simp [sqrt_mul']; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ 0 < √(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
inr : √π ≤ (↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)

Tactic:
rw [this, ← le_div_iff₀ (by positivity)]

Premises used: le_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ √π ≤ (↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
sqrt_pi_le_stirlingSeq hn

Premises used: Stirling.sqrt_pi_le_stirlingSeq, Stirling.stirlingSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ √π ≤ (↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
exact sqrt_pi_le_stirlingSeq hn

Premises used: Stirling.sqrt_pi_le_stirlingSeq
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 =
    (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
hy : rexp 1 ≠ 0
hx₁ : 2 * π ≠ 0
hy₁ : Ne (α := ℝ) (↑n : ℝ) 0
rw : 0 ≤ 2 * π * (↑n : ℝ)
hx₂ : √(2 * π * (↑n : ℝ)) ≠ 0
hy₂ : ((↑n : ℝ) / rexp 1) ^ n ≠ 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)

Tactic:
rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]

Premises used: Real.log_sqrt, Real.log_exp, Real.log_div, Real.log_pow, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * (↑n : ℝ)) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ ((↑n : ℝ) / rexp 1) ^ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ 0 < √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
_ :
  (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 =
    (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1)
_₁ :
  (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 ≤ log (↑n ! : ℝ)

Tactic:
calc
    _ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
    _ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
      rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity
    _ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)

Premises used: Real.pi, HMul.hMul, HSub.hSub, Stirling.le_factorial_stirling, HDiv.hDiv, Real.exp, Real.log_le_log, Nat.cast, Real.log, HPow.hPow, HAdd.hAdd, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ 0 < 2 * π

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ Continuous Angle.coe

Tactic:
continuous_quotient_mk'

Premises used: Real.Angle, Real.Angle.coe, continuous_quotient_mk', Quotient.mk'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ (⇑coeHom : (a : ℝ) → Angle) = Angle.coe

Tactic:
rfl

Premises used: Real.Angle.coe, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
p : Angle → Prop
θ : Angle
h : ∀ (x : ℝ), p (↑x : Angle)
⊢ p θ

Tactic:
Quotient.inductionOn' θ h

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ (↑0 : Angle) = 0

Tactic:
rfl

Premises used: Real.Angle.coe, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x y : ℝ
⊢ (↑(x + y) : Angle) = (↑x : Angle) + (↑y : Angle)

Tactic:
rfl

Premises used: Real.Angle.coe, Quotient.map₂, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (↑(-x) : Angle) = -(↑x : Angle)

Tactic:
rfl

Premises used: Real.Angle.coe, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x y : ℝ
⊢ (↑(x - y) : Angle) = (↑x : Angle) - (↑y : Angle)

Tactic:
rfl

Premises used: Real.Angle.coe, Quotient.map₂, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
n : ℕ
x : ℝ
⊢ (↑(n • x) : Angle) = n • (↑x : Angle)

Tactic:
rfl

Premises used: Real.Angle.coe, QuotientAddGroup.Quotient.addGroup._aux_4, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
z : ℤ
x : ℝ
⊢ (↑(z • x) : Angle) = z • (↑x : Angle)

Tactic:
rfl

Premises used: Real.Angle.coe, QuotientAddGroup.Quotient.addGroup._aux_9, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (↑x : Angle) = 0 ↔ ∃ (n : ℤ), n • (2 * π) = x

Tactic:
AddCircle.coe_eq_zero_iff (2 * π)

Premises used: AddCircle.coe_eq_zero_iff, Real.pi, HMul.hMul, Real.Angle, Real.Angle.coe, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
n : ℕ
⊢ (↑((↑n : ℝ) * x) : Angle) = n • (↑x : Angle)

Tactic:
simpa only [nsmul_eq_mul] using coeHom.map_nsmul n x

Premises used: AddMonoidHom.map_nsmul, nsmul_eq_mul, Real.Angle.coeHom
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
n : ℤ
⊢ (↑((↑n : ℝ) * x) : Angle) = n • (↑x : Angle)

Tactic:
simpa only [zsmul_eq_mul] using coeHom.map_zsmul n x

Premises used: zsmul_eq_mul, AddMonoidHom.map_zsmul, Real.Angle.coeHom
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : ℝ
simp : (↑ψ : Angle) = (↑θ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
⊢ (↑θ : Angle) = (↑ψ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)

Tactic:
simp only [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : ℝ
rw : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)) (-ψ + θ) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
⊢ (↑ψ : Angle) = (↑θ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)

Tactic:
rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]

Premises used: QuotientAddGroup.eq, Real.Angle.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : ℝ
⊢ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)) (-ψ + θ) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)

Tactic:
simp only [AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

Premises used: sub_eq_neg_add, AddSubgroup.zmultiples_eq_closure, eq_comm, Eq.symm, AddSubgroup.mem_closure_singleton, zsmul_eq_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : 2 * π = 2 * π * (↑1 : ℝ)
rw₁ : 2 * π = 2 * π * 1
rw₂ rw₃ : 2 * π = 2 * π
⊢ 2 * π - 0 = 2 * π * (↑1 : ℝ)

Tactic:
rw [sub_zero, Int.cast_one, mul_one]

Premises used: sub_zero, mul_one, Int.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : ∃ (k : ℤ), -π - π = 2 * π * (↑k : ℝ)
⊢ -(↑π : Angle) = (↑π : Angle)

Tactic:
rw [← coe_neg, angle_eq_iff_two_pi_dvd_sub]

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
h : -π - π = 2 * π * (↑(-1) : ℝ)
⊢ ∃ (k : ℤ), -π - π = 2 * π * (↑k : ℝ)

Tactic:
use -1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π - π = 2 * π * (↑(-1) : ℝ)

Tactic:
simp [two_mul, sub_eq_add_neg]

Premises used: sub_eq_add_neg, two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℕ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
rw₂ rw₃ : (↑θ : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)

Tactic:
rw [← coe_nsmul, two_nsmul, add_halves]

Premises used: add_halves, Real.Angle.coe_nsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℤ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
rw₂ rw₃ : (↑θ : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)

Tactic:
rw [← coe_zsmul, two_zsmul, add_halves]

Premises used: add_halves, two_zsmul, Real.Angle.coe_zsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : (↑(-π) : Angle) = (↑π : Angle)
rw₁ : -(↑π : Angle) = (↑π : Angle)
rw₂ rw₃ : (↑π : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)

Tactic:
rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]

Premises used: Real.Angle.neg_coe_pi, Real.Angle.two_nsmul_coe_div_two, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : (↑(-π / 2) : Angle) + (↑(-π / 2) : Angle) = (↑π : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
rw₂ rw₃ : (↑π : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]

Premises used: two_zsmul, Real.Angle.two_nsmul_neg_pi_div_two, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ + -(↑π : Angle) = θ + (↑π : Angle)
rw₁ rw₂ : θ + (↑π : Angle) = θ + (↑π : Angle)
⊢ θ - (↑π : Angle) = θ + (↑π : Angle)

Tactic:
rw [sub_eq_add_neg, neg_coe_pi]

Premises used: sub_eq_add_neg, Real.Angle.neg_coe_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ HSMul.hSMul (α := ℕ) 2 (↑π : Angle) = 0

Tactic:
simp [← natCast_mul_eq_nsmul]

Premises used: Real.Angle.natCast_mul_eq_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ HSMul.hSMul (α := ℤ) 2 (↑π : Angle) = 0

Tactic:
simp [← intCast_mul_eq_zsmul]

Premises used: Real.Angle.intCast_mul_eq_zsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : HSMul.hSMul (α := ℕ) 2 (↑π : Angle) = 0
rw₁ rw₂ : Eq (α := Angle) 0 0
⊢ (↑π : Angle) + (↑π : Angle) = 0

Tactic:
rw [← two_nsmul, two_nsmul_coe_pi]

Premises used: Real.Angle.two_nsmul_coe_pi, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : Angle
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ (k : Fin z.natAbs), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑z : ℝ)) : Angle)

Tactic:
QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff hz

Premises used: Real.Angle, QuotientAddGroup.Quotient.addGroup._aux_4, QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff, Quot.map, Quotient.map'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : Angle
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ (k : Fin n), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑n : ℝ)) : Angle)

Tactic:
QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff hz

Premises used: Real.Angle, Real.Angle.coe, QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : Angle
⊢ Int.natAbs 2 = 2

Tactic:
have : Int.natAbs 2 = 2 := rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₆ : ψ = θ ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₇ : ψ = θ ∨ ψ = θ + (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₈ : ψ = θ ∨ ψ = θ + (↑(2 * π / 2) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₉ rw₁₀ : ψ = θ ∨ ψ = θ + (↑π : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)

Tactic:
rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]

Premises used: Int.cast_two, mul_div_cancel_left₀, Fin.val_one, Fin.exists_fin_two, one_smul, two_ne_zero, zero_smul, Real.Angle.zsmul_eq_iff, add_zero, Fin.val_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ θ : Angle
simp_rw : HSMul.hSMul (α := ℤ) (↑2 : ℤ) ψ = HSMul.hSMul (α := ℤ) (↑2 : ℤ) θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
simp_rw₁ : HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 ψ = HSMul.hSMul (α := ℕ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)

Tactic:
simp_rw [← natCast_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]

Premises used: Nat.cast_ofNat, Real.Angle.two_zsmul_eq_iff, natCast_zsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) (β := Angle) 2 0 ↔ θ = 0 ∨ θ = 0 + (↑π : Angle)

Tactic:
two_nsmul_eq_iff

Premises used: Real.Angle.two_nsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : 0 = HSMul.hSMul (α := ℕ) (β := Angle) 2 0
h₁ : (↑π : Angle) = 0 + (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
convert! two_nsmul_eq_iff

Premises used: Real.Angle.two_nsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 = HSMul.hSMul (α := ℕ) (β := Angle) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (↑π : Angle) = 0 + (↑π : Angle)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ ¬HSMul.hSMul (α := ℕ) 2 θ = 0
⊢ HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← two_nsmul_eq_zero_iff]

Premises used: Real.Angle.two_nsmul_eq_zero_iff, not_or
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
simp_rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
simp_rw₁ : HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]

Premises used: Real.Angle.two_nsmul_eq_zero_iff, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ ¬HSMul.hSMul (α := ℤ) 2 θ = 0
⊢ HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← two_zsmul_eq_zero_iff]

Premises used: not_or, Real.Angle.two_zsmul_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₂ rw₃ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]

Premises used: Real.Angle.two_nsmul_eq_zero_iff, add_eq_zero_iff_eq_neg, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ ≠ -θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : θ ≠ -θ ↔ ¬θ = -θ
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← eq_neg_self_iff.not]

Premises used: Iff.not, not_or, Real.Angle.eq_neg_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₁ rw₂ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ -θ = θ ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
rw [eq_comm, eq_neg_self_iff]

Premises used: eq_comm, Real.Angle.eq_neg_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : -θ ≠ θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : -θ ≠ θ ↔ ¬-θ = θ
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← neg_eq_self_iff.not]

Premises used: Iff.not, not_or, Real.Angle.neg_eq_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (↑π : Angle) = (↑(π / 2 + π / 2) : Angle)
rw₁ rw₂ : (↑π : Angle) = (↑π : Angle)
⊢ (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)

Tactic:
rw [two_nsmul, add_halves]

Premises used: add_halves, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)

Tactic:
have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
nth_rw :
  HSMul.hSMul (α := ℕ) 2 θ = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle) ↔
    θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
nth_rw 1 [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
rw : θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle) ↔
    θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
rw [coe_nsmul, two_nsmul_eq_iff]

Premises used: Real.Angle.coe_nsmul, Real.Angle.two_nsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a :
  (θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle)) = (θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle))
⊢ θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
apply iff_of_eq

Premises used: iff_of_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
⊢ (θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle)) = (θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
a₆ : (↑(π + (π / 2 + π / 2)) : Angle) = 0
a₇ : (↑(π + π) : Angle) = 0
a₈ : (↑(2 * π) : Angle) = 0
a₉ a₁₀ : Eq (α := Angle) 0 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)

Tactic:
rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]

Premises used: neg_div, add_halves, sub_eq_zero, add_assoc, Real.Angle.coe_add, two_mul, Real.Angle.coe_sub, add_comm, Real.Angle.coe_two_pi, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ + θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]

Premises used: Real.Angle.two_nsmul_eq_pi_iff, two_zsmul, two_nsmul