-- Mathlib/Data/List/Basic.lean
@[simp] lemma length_injective_iff : Injective (List.length : List α → ℕ) ↔ Subsingleton α

Proof state:
case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝

Tactic:
apply ih

Result:
case e_tail.hl
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length

Proof state:
α : Type u
h : Injective length
x y : α
this : [x] = [y]
⊢ x = y

Tactic:
simpa using this

Result:
no goals

Proof state:
case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Tactic:
(suffices [x] = [y] by simpa using this)

Result:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]

Proof state:
case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

Tactic:
cases hl

Result:
no goals

Proof state:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]

Tactic:
apply h

Result:
case mp.a
α : Type u
h : Injective length
x y : α
⊢ [x].length = [y].length

Proof state:
case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

Tactic:
cases hl

Result:
no goals

Proof state:
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
congr

Result:
case e_head
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ = head✝

case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝

Proof state:
case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this

Result:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]

Proof state:
case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2

Tactic:
induction l1 generalizing l2 <;> cases l2

Result:
case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Proof state:
case mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
intros hα l1 l2 hl

Result:
case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2

Proof state:
case e_head
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ = head✝

Tactic:
subsingleton

Result:
no goals

Proof state:
α : Type u
⊢ Injective length ↔ Subsingleton α

Tactic:
constructor

Result:
case mp
α : Type u
⊢ Injective length → Subsingleton α

case mpr
α : Type u
⊢ Subsingleton α → Injective length

Proof state:
case e_tail.hl
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length

Tactic:
simpa using hl

Result:
no goals

Proof state:
case mp
α : Type u
h : Injective length
⊢ Subsingleton α

Tactic:
refine ⟨fun x y => ?_⟩

Result:
case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Proof state:
case mp
α : Type u
⊢ Injective length → Subsingleton α

Tactic:
intro h

Result:
case mp
α : Type u
h : Injective length
⊢ Subsingleton α

Proof state:
case mp.a
α : Type u
h : Injective length
x y : α
⊢ [x].length = [y].length

Tactic:
rfl

Result:
no goals