Theorem: C03S01.my_lemma4 (LeanInRome/S3_Logic/S01_Implication_and_the_Universal_Quantifier.lean)

State before:
⊢ ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε
Tactic:
intro x y ε epos ele1 xlt ylt
State after:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε

State before:
x y ε : ℝ
epos : 0 < ε
ele1 : ε ≤ 1
xlt : |x| < ε
ylt : |y| < ε
⊢ |x * y| < ε
Tactic:
calc
  |x * y| = |x| * |y| := sorry
  _ ≤ |x| * ε := sorry
  _ < 1 * ε := sorry
  _ = ε := sorry
State after:
no goals