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

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

Tactic:
constructor

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

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

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

Tactic:
intro h

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

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

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

Tactic:
simpa [instBEq, isEqv, isEqvAux]

Result:
no goals

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
obtain ⟨hs, hi⟩ := isEqv_iff_rel.mp h

Result:
case mpr.eq_of_beq.intro
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
⊢ a = b

Proof state:
case mpr.eq_of_beq.intro.h₁
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
⊢ a.size = b.size

Tactic:
exact hs

Result:
no goals

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

Proof state:
case mpr.eq_of_beq.intro.h₂
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
i : Nat
h₁ : i < a.size
h₂ : i < b.size
⊢ a[i] = b[i]

Tactic:
simpa using hi _ h₁

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
intro a

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

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

Tactic:
intro h

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

Proof state:
case mpr.eq_of_beq.intro
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
⊢ a = b

Tactic:
ext i h₁ h₂

Result:
case mpr.eq_of_beq.intro.h₁
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
⊢ a.size = b.size

case mpr.eq_of_beq.intro.h₂
α : Type u_1
inst✝ : BEq α
h✝ : LawfulBEq α
a b : Array α
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
i : Nat
h₁ : i < a.size
h₂ : i < b.size
⊢ a[i] = b[i]

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

Tactic:
apply Array.isEqv_self_beq

Result:
no goals

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

Tactic:
intro a

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

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

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

Tactic:
constructor

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

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

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

Tactic:
apply beq_of_beq_singleton

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