simpa

Stream: mathlib4

[Patrick Massot]

I'm sure this has been discussed before, but did we loose simpa as an abbreviation of simpa using this on purpose?

[Patrick Massot]

After some more investigation, simpa indeed does something with this, but not the expected thing (expected based on Lean 3 behavior). In Lean 3:

import logic.basic
import tactic.simpa

example (P : Prop) (h : ¬ ¬ P) : P :=
begin
  have : ¬ ¬ P := h,
  simpa,
end

works but in Lean 4,

import Mathlib.Logic.Basic
import Std.Tactic.Simpa

example (P : Prop) (h : ¬ ¬ P) : P := by
  have : ¬ ¬ P := h
  simpa

doesn't, you need to do

import Mathlib.Logic.Basic
import Std.Tactic.Simpa

example (P : Prop) (h : ¬ ¬ P) : P := by
  have : ¬ ¬ P := h
  simp at this
  assumption

@Mario Carneiro

[Mario Carneiro]

fixed on master

[Patrick Massot]

Thanks!