batteries

batteries copied to clipboard

feat: implement `ext?` and `ext!?`

1

Implement `ext?`, `ext1?` to show used extensionality lemmas, and `ext!?` to brute-force try all ext-lemmas. - `ext?` displays a tactic replacement suggestion that could replace the `ext`. The tactic sequence...

joneugster

rcases doesn't seem to support ?_ placeholders

3

```lean import Std.Tactic.RCases theorem aux (h : 0 < 2) : ∃ n : Nat, n = 2 := ⟨2, rfl⟩ example : True := by rcases aux ?_ with...

Ruben-VandeVelde

feat: Sum.left, Sum.right

4

More intuitive names than `.inl` and `.inr` for non-type-theorists. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/No.20Either.20type

JamesGallicchio

JamesGallicchio

kim-em

`simpNF` should use dsimp for lemmas proved by `rfl`

1

The `@[simp]` attribute is used by both simp and dsimp, so it is possible for a rfl lemma to have a proof by simp but not one by dsimp, and...

digama0

```lean import Std.Tactic.Simpa theorem foo : ℕ = ℤ ↔ False := sorry example (bar : ℕ = ℤ) : False := by simpa [foo] using bar /- try 'simp...

kbuzzard

`simpNF` linter rejecting working simp lemma

3

```lean import Std.Tactic.Lint def Set (α : Type u) := α → Prop def unionᵢ (s : ι → Set β) : Set β := sorry -- supᵢ s def...

kbuzzard

rcases can't use `rfl` on `0 = a` in some circumstances.

6

``` import Std.Tactic.RCases variable {α : Type _} [LT α] (a : α) theorem lt_trichotomy (a b : α) : a < b ∨ a = b ∨ b <...

kim-em

Achieve parity between Array and List lemmas

4

In order to encourage std4 users to write verifiable code with arrays, we should aim to have a similar set of lemmas for arrays (https://github.com/leanprover/std4/blob/main/Std/Data/Array/Lemmas.lean) as we do for lists...

mpenciak