rw show by

Stream: new members

[Anatole Dedecker]

Is there a prettier way to do things like that ?

rw (show ? = ?, by {...}),

[Jalex Stark]

I'm not sure I understand what's going on there, but maybe you want tactic#convert

[Alex J. Best]

I'd say that and have : ? = ? := by blah, rw this are your main choices, depending on the length of blah.

[Markus Himmel]

Sometimes you can avoid these constructions by restructuring your proof into a calc proof.

[Anatole Dedecker]

Yes but the problem of calc proofs is they need to close the goal :sad:

[Jalex Stark]

so start by creating the goal which is the last statement of the calc proof?

[Anatole Dedecker]

Indeed, but the whole objective of using the rw (show ..., by ...) syntax is we don't need to create a 1-use subgoal

[Jalex Stark]

does the following work as a way to introduce a lemma A = C?

have := calc A = B : by sorry
... = C : by sorry

[Adam Topaz]

You can also refine calc foo = bar : _ etc

[Alex J. Best]

Well you're still introducing it when you prove it it just disappears out of scope after, you can clear a have if you're finding you have two many of these one time things floating around.

[Anatole Dedecker]

Oh yes I forget about this all the time x)

[Alex J. Best]

Or prove it as a lemma if its not too specific ! So you can rewrite it without introducing it.

[Anatole Dedecker]

Jalex Stark said:

does the following work as a way to introduce a lemma A = C?

have := calc A = B : by sorry
... = C : by sorry

It does, that's clever

[Anatole Dedecker]

The use I had in mind was for things like that :

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : ℝ, x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  rw (show (0 : ℝ) = 1 * 0, by simp),
  apply tendsto.mul,
  exact tendsto_id,
  rw (show (0 : ℝ) = 1 - 1, by simp),
  exact tendsto.sub tendsto_const_nhds tendsto_id,
end

[Jalex Stark]

in this case, both lemmas have names

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : ℝ, x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  rw ← one_mul (0:ℝ),
  apply tendsto.mul, { exact tendsto_id },
  rw ← sub_self (1:ℝ),
  apply tendsto.sub, { exact tendsto_const_nhds },
  exact tendsto_id,
end

[Anatole Dedecker]

Indeed, but that's a simple example

[Jalex Stark]

one can also do this which feels silly but maybe demonstrates convert:

import topology.instances.real

open filter
open_locale topological_space filter

example : tendsto (λ x : ℝ, x * (1 - x)) (𝓝 1) (𝓝 0) :=
begin
  convert tendsto.mul _ _, rw one_mul, apply_instance,
  { exact tendsto_id },
  convert tendsto.sub _ _, rw sub_self, exact 1, apply_instance,
  { exact tendsto_const_nhds },
  exact tendsto_id,
end

[Anatole Dedecker]

Oh interesting. I need to learn how to use convert

[Kevin Buzzard]

convert is great. It is like rw on steroids. Once you have a hypothesis h which is basically equal to your goal modulo a few differences, convert h will just explicitly give you the differences as new goals, saving you the trouble of having to work with them as subterms of a larger term