Classifies porting notes claiming:
was decide!
Examples
|
/-- The orthocenter lies in the altitudes. -/ |
|
theorem orthocenter_mem_altitude (t : Triangle ℝ P) {i₁ : Fin 3} : |
|
t.orthocenter ∈ t.altitude i₁ := by |
|
obtain ⟨i₂, i₃, h₁₂, h₂₃, h₁₃⟩ : ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by |
|
-- porting note: was `decide!` |
|
fin_cases i₁ <;> decide |
|
rw [orthocenter_eq_mongePoint, t.altitude_eq_mongePlane h₁₂ h₁₃ h₂₃] |
|
exact t.mongePoint_mem_mongePlane |
|
#align affine.triangle.orthocenter_mem_altitude Affine.Triangle.orthocenter_mem_altitude |
|
/-- `χ₄` takes values in `{0, 1, -1}` -/ |
|
theorem isQuadratic_χ₄ : χ₄.IsQuadratic := by |
|
intro a |
|
-- Porting note: was `decide!` |
|
fin_cases a |
|
all_goals decide |
|
#align zmod.is_quadratic_χ₄ ZMod.isQuadratic_χ₄ |
