# Zulip Chat Archive

## Stream: general

### Topic: subst at hyp

#### Johan Commelin (Sep 07 2018 at 08:31):

Could we have `subst foobar at hyp`

for substituting in the hypotheses of the local context? Currently I am using `repeat {rw foobar at hyp}`

which feels a bit verbose...

#### Kenny Lau (Sep 07 2018 at 08:32):

`subst foobar`

#### Chris Hughes (Sep 07 2018 at 08:34):

What about `simp only [foobar] at hyp`

#### Johan Commelin (Sep 07 2018 at 08:35):

aah never mind. `subst`

is only for local constants. I wanted to substitute `x = y`

where `x = y`

was the result of some proposition.

#### Johan Commelin (Sep 07 2018 at 08:36):

`simp only`

works!

#### Kenny Lau (Sep 07 2018 at 08:38):

MWE?

#### Johan Commelin (Sep 07 2018 at 08:38):

https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf

#### Kenny Lau (Sep 07 2018 at 08:39):

?

#### Johan Commelin (Sep 07 2018 at 08:40):

Right, so now you only see the `simp`

s. For the `repeat {rw ...}`

you have to look in the history.

#### Johan Commelin (Sep 07 2018 at 08:40):

Basically I'm challenging you to golf it :lol:

#### Kenny Lau (Sep 07 2018 at 08:44):

what import is allowed?

#### Johan Commelin (Sep 07 2018 at 08:45):

I don't really care

#### Johan Commelin (Sep 07 2018 at 08:45):

What would you want to use? `tidy`

?

#### Kenny Lau (Sep 07 2018 at 08:46):

you didn't import any file from mathlib, so I can't use any mathlib tactic

#### Johan Commelin (Sep 07 2018 at 08:47):

Wasnt `have ... simp at this ... exact this`

some sort of idiom that can be golfed into a `simpa`

-oneliner? I tried but failed.

#### Reid Barton (Sep 07 2018 at 08:50):

`simpa using this`

#### Reid Barton (Sep 07 2018 at 08:51):

Or rather `simpa using ...`

#### Johan Commelin (Sep 07 2018 at 08:54):

And what do I need to import to get `simpa`

?

#### Reid Barton (Sep 07 2018 at 08:54):

My attempt: https://gist.github.com/rwbarton/b79b804e4bff300a5aa2a4ec2951c55e

#### Reid Barton (Sep 07 2018 at 08:54):

Anything in mathlib, but say `tactic.interactive`

#### Kenny Lau (Sep 07 2018 at 08:55):

import tactic.interactive universe u namespace eckmann_hilton variables (X : Type u) local notation a `<`m`>` b := @has_mul.mul X m a b class is_unital [m : has_mul X] [e : has_one X] : Prop := (one_mul : ∀ x : X, (e.one <m> x) = x) (mul_one : ∀ x : X, (x <m> e.one) = x) attribute [simp] is_unital.one_mul is_unital.mul_one variables {X} {m₁ : has_mul X} {e₁ : has_one X} {m₂ : has_mul X} {e₂ : has_one X} variables (h₁ : @is_unital X m₁ e₁) (h₂ : @is_unital X m₂ e₂) variables (distrib : ∀ a b c d, ((a <m₂> b) <m₁> (c <m₂> d)) = ((a <m₁> c) <m₂> (b <m₁> d))) include h₁ h₂ distrib lemma one : (e₁.one = e₂.one) := by simpa using distrib e₂.one e₁.one e₁.one e₂.one lemma mul : (m₁.mul = m₂.mul) := by funext a b; have := distrib a e₁.one e₁.one b; simp at this; simpa [one h₁ h₂ distrib] using this lemma mul_comm : is_commutative _ m₂.mul := ⟨λ a b, by simpa [mul h₁ h₂ distrib] using distrib e₂.one a b e₂.one⟩ lemma mul_assoc : is_associative _ m₂.mul := ⟨λ a b c, by simpa [mul h₁ h₂ distrib] using distrib a b e₂.one c⟩ instance : comm_monoid X := { mul_comm := (mul_comm h₁ h₂ distrib).comm, mul_assoc := (mul_assoc h₁ h₂ distrib).assoc, ..m₂, ..e₂, ..h₂ } end eckmann_hilton

#### Johan Commelin (Sep 07 2018 at 09:00):

Well done!

#### Johan Commelin (Sep 07 2018 at 09:02):

@Kenny Lau https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf

I added your name.

#### Kenny Lau (Sep 07 2018 at 09:02):

lol

Last updated: May 14 2021 at 22:15 UTC