[Merged by Bors] - chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean

[dwrensha]

Uncomment two theorems that were added in commented form in #22.

You may compare to the mathlib3 versions here: https://github.com/leanprover-community/mathlib/blob/aaf7dc2c34831dbd92a21b9e37c1f63017d35f45/src/data/list/basic.lean#L50-L54

[digama0]

nolints are almost never the right thing to do in response to a linter warning. In this case the issue is that injective is reducible, I don't think it was in lean 3. (The reason it was omitted from #22 is because injective didn't exist at the time.)

[dwrensha]

Should we remove the @[reducible] attribute from injective?

[gebner]

Yes, injective should not be reducible. See also leanprover-community/mathport#118

[gebner]

Please also follow the commit message guidelines and title this PR chore: uncomment cons_injective and cons_inj

[dwrensha]

(link to commit message guidelines: https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md )

[gebner]

New guidelines: https://github.com/leanprover/lean4/blob/3a20b6be8a570eb2027675aee1ca2206c7b73b8a/doc/dev/commit_convention.md

[dwrensha]

Updated the PR title (subject) and summary (body) to conform with the conventions.

[gebner]

Can you please remove the @[reducible] from injective instead?

[gebner]

And please follow the new conventions. (Which no longer have the (Data/List/Basic) part.)

[dwrensha]

Removing @[reducible] from Function.injective causes these errors:

./././Mathlib/Order/Basic.lean:317:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toLE ?α)
./././Mathlib/Order/Basic.lean:339:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toPreorder ?α)
./././Mathlib/Order/Basic.lean:347:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toPartialOrder ?α)
./././Mathlib/Order/Basic.lean:361:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
./././Mathlib/Order/Basic.lean:366:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
./././Mathlib/Order/Basic.lean:372:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

These didn't look trivial to fix, so I thought it would it would make sense to land this with the comment instead.
I'll look into fixing them...

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build