-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem lawfulBEq_iff [BEq α] : LawfulBEq (List α) ↔ LawfulBEq α

Proof state:
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
a : α
this : ([a] == [a]) = true
⊢ (a == a) = true

Tactic:
simpa only [List.instBEq, List.beq, Bool.and_true]

Result:
no goals

Proof state:
case mp.eq_of_beq.a
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ (a == b && true) = true

Tactic:
simpa

Result:
no goals

Proof state:
case mpr.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ ∀ {a : List α}, (a == a) = true

Tactic:
intro a

Result:
case mpr.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
a : List α
⊢ (a == a) = true

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ LawfulBEq α

Tactic:
constructor

Result:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ ∀ {a b : α}, (a == b) = true → a = b

case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ ∀ {a : α}, (a == a) = true

Proof state:
case mpr.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : List α
h : (a == b) = true
⊢ a = b

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ ∀ {a b : α}, (a == b) = true → a = b

Tactic:
intro a b h

Result:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ a = b

Proof state:
case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
a : α
⊢ (a == a) = true

Tactic:
suffices ([a] == [a]) = true by
  simpa only [List.instBEq, List.beq, Bool.and_true]

Result:
case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
a : α
⊢ ([a] == [a]) = true

Proof state:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ a = b

Tactic:
apply singleton_inj.1

Result:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ [a] = [b]

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
⊢ LawfulBEq (List α) → LawfulBEq α

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ LawfulBEq α

Proof state:
α : Type u_1
inst✝ : BEq α
⊢ LawfulBEq (List α) ↔ LawfulBEq α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : BEq α
⊢ LawfulBEq (List α) → LawfulBEq α

case mpr
α : Type u_1
inst✝ : BEq α
⊢ LawfulBEq α → LawfulBEq (List α)

Proof state:
case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
⊢ ∀ {a : α}, (a == a) = true

Tactic:
intro a

Result:
case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
a : α
⊢ (a == a) = true

Proof state:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ [a] = [b]

Tactic:
apply eq_of_beq

Result:
case mp.eq_of_beq.a
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ ([a] == [b]) = true

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ LawfulBEq (List α)

Tactic:
constructor

Result:
case mpr.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ ∀ {a b : List α}, (a == b) = true → a = b

case mpr.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ ∀ {a : List α}, (a == a) = true

Proof state:
case mpr.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
a : List α
⊢ (a == a) = true

Tactic:
simp

Result:
no goals

Proof state:
case mp.rfl
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (List α)
a : α
⊢ ([a] == [a]) = true

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
⊢ LawfulBEq α → LawfulBEq (List α)

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ LawfulBEq (List α)

Proof state:
case mpr.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ ∀ {a b : List α}, (a == b) = true → a = b

Tactic:
intro a b h

Result:
case mpr.eq_of_beq
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : List α
h : (a == b) = true
⊢ a = b

Proof state:
case mp.eq_of_beq.a
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ ([a] == [b]) = true

Tactic:
simp only [List.instBEq, List.beq]

Result:
case mp.eq_of_beq.a
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq (List α)
a b : α
h : (a == b) = true
⊢ (a == b && true) = true