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

Proof state:
case mpr.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq α
⊢ ∀ {a b : Option α}, (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 : Option α
h : (a == b) = true
⊢ a = b

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

Tactic:
simpa using h

Result:
no goals

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

Tactic:
intro h

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

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

Tactic:
intro a

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

Proof state:
case mp.eq_of_beq
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (Option α)
⊢ ∀ {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 (Option α)
a b : α
h : (a == b) = true
⊢ a = b

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

Tactic:
apply Option.some.inj

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

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

Tactic:
intro a

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

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

Tactic:
intro h

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

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

Tactic:
suffices (some a == some a) = true by
  simpa only [some_beq_some]

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
apply eq_of_beq

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

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

Tactic:
constructor

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

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
h : LawfulBEq (Option α)
a : α
this : (some a == some a) = true
⊢ (a == a) = true

Tactic:
simpa only [some_beq_some]

Result:
no goals

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

Tactic:
constructor

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

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