awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have hs₁ : -(-θ).sign = (θ + ψ).sign
Tactic: rw [← neg_neg θ.sign, ← sign_neg] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : -(-θ).sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have this : (θ + ψ + -θ).toReal = (θ + ψ).toReal + (-θ).toReal
Tactic: have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hθs₁ : θ.toReal ∈ Set.Ioo 0 π
Tactic: rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs
Cleared hypotheses: hθs, hψs, hsa
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
hθs₁ : θ.toReal ∈ Set.Ioo 0 π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hψs₁ : ψ.toReal ∈ Set.Ioo 0 π
Tactic: rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs
Cleared hypotheses: hθs, hψs, hsa
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
Tactic: have : ((θ + ψ).toReal : Angle) = ↑(θ.toReal + ψ.toReal) := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have obtain : ∀ (k : ℤ) (hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)),
  |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain ⟨k, hk⟩ := angle_eq_iff_two_pi_dvd_sub.mp this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
⊢ (θ + ψ).toReal ≤ 0 ∨ θ + ψ = (↑π : Angle)
have this₁ : (θ + ψ).sign = -1 ∨ (θ + ψ).sign = 0 ∨ (θ + ψ).sign = 1
Tactic: have := (θ + ψ).sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inl : ∀ (h : (θ + ψ).toReal ≤ 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain (h | h) : (θ + ψ).toReal ≤ 0 ∨ θ + ψ = π := by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
inl : ∀ (h : (θ + ψ).toReal ≤ 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inr : ∀ (h : θ + ψ = (↑π : Angle)), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain (h | h) : (θ + ψ).toReal ≤ 0 ∨ θ + ψ = π := by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hk₁ : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑(-1) : ℝ)
Tactic: obtain rfl : k = -1 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos <| by
      grind [toReal_mem_Ioc]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : θ + ψ = (↑π : Angle)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inr : ∀ (hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)) (h : θ + ψ = (↑π : Angle)), π = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: simp_all only [sign_coe_pi, ne_eq, zero_ne_one, not_false_eq_true, toReal_pi, coe_add,
      coe_toReal, pi_pos, abs_of_pos]
Cleared hypotheses: hsa, this, hk, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
k : ℤ
hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : θ + ψ = (↑π : Angle)
⊢ π = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hk₁ : π - (θ.toReal + ψ.toReal) = 2 * π * (↑0 : ℝ)
Tactic: obtain rfl : k = 0 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos (by grind)
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inl : ∀ (h : θ.sign = -1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain h | h | h := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
inl : ∀ (h : θ.sign = -1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inr : ∀ (h : θ.sign = 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain h | h | h := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
inl : ∀ (h : θ.sign = -1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
inr : ∀ (h : θ.sign = 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have inr₁ : ∀ (h : θ.sign = 1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Tactic: obtain h | h | h := θ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hθ' : (-θ).sign = 1
Tactic: obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hψ' : (-ψ).sign = 1
Tactic: obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ + -ψ).sign ≠ 1
have rwa : (-θ + -ψ).sign ≠ (-θ).sign
Tactic: rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
rwa : (-θ + -ψ).sign ≠ (-θ).sign
⊢ (-θ + -ψ).sign ≠ 1
have rwa₁ : (-θ).sign ≠ (-θ + -ψ).sign
Tactic: rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
rwa : (-θ + -ψ).sign ≠ (-θ).sign
rwa₁ : (-θ).sign ≠ (-θ + -ψ).sign
⊢ (-θ + -ψ).sign ≠ 1
have rwa₂ : (-θ).sign ≠ (-(θ + ψ)).sign
Tactic: rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
rwa : (-θ + -ψ).sign ≠ (-θ).sign
rwa₁ : (-θ).sign ≠ (-θ + -ψ).sign
rwa₂ : (-θ).sign ≠ (-(θ + ψ)).sign
⊢ (-θ + -ψ).sign ≠ 1
have rwa₃ : -θ.sign ≠ (-(θ + ψ)).sign
Tactic: rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
rwa : (-θ + -ψ).sign ≠ (-θ).sign
rwa₁ : (-θ).sign ≠ (-θ + -ψ).sign
rwa₂ : (-θ).sign ≠ (-(θ + ψ)).sign
rwa₃ : -θ.sign ≠ (-(θ + ψ)).sign
⊢ (-θ + -ψ).sign ≠ 1
have rwa₄ : -θ.sign ≠ -(θ + ψ).sign
Tactic: rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have hsa' : (-θ + -ψ).sign ≠ 1
Tactic: have hsa' : (-θ + -ψ).sign ≠ 1 := by
      rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have h₁ : |(θ + ψ).toReal| = |(-θ + -ψ).toReal|
Tactic: convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
h₁ : |(θ + ψ).toReal| = |(-θ + -ψ).toReal|
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
have h₂ : 2 * π - (|θ.toReal| + |ψ.toReal|) = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)
Tactic: convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
⊢ ContinuousOn (sign ∘ f) s
have refine : ∀ (θ : Angle) (hθ : θ ∈ f '' s), ContinuousAt sign θ
Tactic: refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ
have obtain : ∀ (z : α) (hz : z ∈ s), ContinuousAt sign (f z)
Tactic: obtain ⟨z, hz, rfl⟩ := hθ
Cleared hypotheses: θ, hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
have h₁ : ∀ (a : ℤ),
  (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
h₁ :
  ∀ (a : ℤ),
    (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
have h₂ : ∀ (a : ℤ),
  (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
h₁ :
  ∀ (a : ℤ),
    (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
h₂ :
  ∀ (a : ℤ),
    (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
have h₃ : ∀ (x_1 : ℤ),
  (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
h₁ :
  ∀ (a : ℤ),
    (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
h₂ :
  ∀ (a : ℤ),
    (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
h₃ :
  ∀ (x_1 : ℤ),
    (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2
have h₄ : ∀ (x : ℤ),
  (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y = (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * π / 2
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
a : ℤ
⊢ (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
have h₁ : ¬x = (↑(2 * a + 1) : ℝ) * π / 2 ↔ ¬x = (↑(2 * a + 1) : ℝ) * π / 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
a : ℤ
⊢ (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
have h₁ : ¬y = (↑(2 * a + 1) : ℝ) * π / 2 ↔ ¬y = (↑(2 * a + 1) : ℝ) * π / 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
x_1 : ℤ
⊢ (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2
have h₁ : x = (↑(2 * x_1 + 1) : ℝ) * π / 2 ↔ x = (↑(2 * x_1 + 1) : ℝ) * π / 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
x_1 : ℤ
⊢ (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2
have h₁ : y = (↑(2 * x_1 + 1) : ℝ) * π / 2 ↔ y = (↑(2 * x_1 + 1) : ℝ) * π / 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
⊢ tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)
have this : Complex.tan (2 * (↑x : ℂ)) = 2 * Complex.tan (↑x : ℂ) / (1 - HPow.hPow (β := ℕ) (Complex.tan (↑x : ℂ)) 2)
Tactic: have := @Complex.tan_two_mul x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
this : Complex.tan (2 * (↑x : ℂ)) = 2 * Complex.tan (↑x : ℂ) / (1 - HPow.hPow (β := ℕ) (Complex.tan (↑x : ℂ)) 2)
⊢ tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)
have norm_cast : ∀ (this : tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)),
  tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)
Tactic: norm_cast at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
n w : ℤ
⊢ ∃ (k : ℤ), (↑k : ℝ) * π / 2 = (↑n : ℝ) * π / 2
have h : (↑n : ℝ) * π / 2 = (↑n : ℝ) * π / 2
Tactic: use n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
⊢ (fun (x : ℝ) ↦ sin x / cos x) = tan
have h : ∀ (x : ℝ), sin x / cos x = tan x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
have h : sin x / cos x = sin x / cos x
Tactic: rw [tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
⊢ ContinuousOn tan {x : ℝ | cos x ≠ 0}
have h_eq : (fun (x : ℝ) ↦ sin x / cos x) = tan
Tactic: have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]