Theorem: C03S01.my_lemma3 (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:
sorry
State after:
no goals