## Stream: general

### Topic: tauto?

#### Sebastien Gouezel (Oct 19 2018 at 20:13):

Suppose I have an assumption

h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → ∀ (y : α), dist (F n y) (f y) ≤ ε)


and a goal

∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → ∀ (y : α), y ∈ ball x 1 → dist (F n y) (f y) ≤ ε)


The goal is a trivial consequence of h (there are more assumptions in the goal than in h). I can prove it by hand doing the intros/rcases dance, but I did not find a tactic that would do it out of the box. Did I miss something?

#### Reid Barton (Oct 19 2018 at 20:19):

tidy can do these sometimes

#### Reid Barton (Oct 19 2018 at 20:20):

Also, there's rintros now :smile:

#### Sebastien Gouezel (Oct 19 2018 at 20:27):

Poor tidy is completely lost when there are real numbers: it unfolds the Cauchy sequences definition, and asks for new goals looking like

dist (F n y) (f y) ≤ quot.mk setoid.r ⟨ε_val, ε_property⟩


#### Kenny Lau (Oct 19 2018 at 20:27):

I don't see why one can't just prove it by hand. It isn't like it's very complicated

#### Kenny Lau (Oct 19 2018 at 20:27):

but yes, I agree there should be a tactic that doesn't only take iff things as argument

#### Patrick Massot (Oct 19 2018 at 20:28):

Because proving things by hand don't scale

#### Patrick Massot (Oct 19 2018 at 20:28):

We want thousands of those trivial proofs

#### Sebastien Gouezel (Oct 19 2018 at 20:32):

Isabelle proof: using h by blast :)

#### Patrick Massot (Oct 19 2018 at 20:33):

That still two words of noise, but it's getting close to acceptable

(deleted)

#### Chris Hughes (Oct 19 2018 at 20:36):

(deleted)

Last updated: May 14 2021 at 14:20 UTC