subst at hyp

Stream: general

[Johan Commelin]

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]

subst foobar

[Chris Hughes]

What about simp only [foobar] at hyp

[Johan Commelin]

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]

simp only works!

[Kenny Lau]

MWE?

[Johan Commelin]

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

[Kenny Lau]

?

[Johan Commelin]

Right, so now you only see the simps. For the repeat {rw ...} you have to look in the history.

[Johan Commelin]

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

[Kenny Lau]

what import is allowed?

[Johan Commelin]

I don't really care

[Johan Commelin]

What would you want to use? tidy?

[Kenny Lau]

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

[Johan Commelin]

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]

simpa using this

[Reid Barton]

Or rather simpa using ...

[Johan Commelin]

And what do I need to import to get simpa?

[Reid Barton]

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

[Reid Barton]

Anything in mathlib, but say tactic.interactive

[Kenny Lau]

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]

Well done!

[Johan Commelin]

@Kenny Lau https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf
I added your name.

[Kenny Lau]

lol