calc vs suffices

Stream: new members

[Luke Mantle]

I'm working through chapter 7 - Topology from Mathematics In Lean. In this exercise, the solution uses calc, but I'm wondering why suffices isn't working.

The proof in the solution is structured like this:

import topology.instances.real

open set filter
open_locale topological_space filter

def tendsto₁ {X Y : Type*} (f : X → Y) (F : filter X) (G : filter Y) :=
∀ V ∈ G, f ⁻¹' V ∈ F

example {X Y Z : Type*} {F : filter X} {G : filter Y} {H : filter Z} {f : X → Y} {g : Y → Z}
  (hf : tendsto₁ f F G) (hg : tendsto₁ g G H) : tendsto₁ (g ∘ f) F H :=
begin
  calc map (g ∘ f) F ≤ H : sorry
end

Whereas this structure of proof doesn't work:

example {X Y Z : Type*} {F : filter X} {G : filter Y} {H : filter Z} {f : X → Y} {g : Y → Z}
  (hf : tendsto₁ f F G) (hg : tendsto₁ g G H) : tendsto₁ (g ∘ f) F H :=
begin
  suffices : map (g ∘ f) F ≤ H,
  { simp },
  sorry,
end

[Eric Wieser]

calc solves the current goal

[Eric Wieser]

You can do have := calc map (g ∘ f) F ≤ H : sorry if you want to use calc to create a hypothesis

[Luke Mantle]

Well, I was specifically wondering why, once we show map (g ∘ f) F ≤ H using calc, lean knows that it's equivalent to the goal tendsto₁ (g ∘ f) F H without any additional explanation. Meanwhile, assuming map (g ∘ f) F ≤ H using suffices, Lean can no longer match map (g ∘ f) F ≤ H to the goal tendsto₁ (g ∘ f) F H.

[Jake Levinson]

I think simpa (instead of simp) works for your suffices approach. (simpa is basically simp, assumption)

[Kevin Buzzard]

simp tries lots of rewrites on the goal (all of the lemmas which have been tagged with the @[simp] attribute) and solves the goal if it manages to reduce it to something like X=X. In your situation simp might be able to reduce the goal to the hypothesis this, but that's not of the form X=X so we'd not expect it to work. As Jake says, what you want to do is to run the simplifier on both the goal and a hypothesis, and then close the goal if it becomes equal to the hypothesis, and that's a different tactic.