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

Proof state:
case mp.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
a : α
⊢ (a == a) = true

Tactic:
suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
  rw [mkVector_beq_mkVector] at this
  simpa

Result:
case mp.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
a : α
⊢ (mkVector (n + 1) a == mkVector (n + 1) a) = true

Proof state:
case mp.eq_of_beq.a
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h✝ : LawfulBEq (Vector α (n + 1))
a b : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ a = b
⊢ (n + 1 == 0 || a == b) = true

Tactic:
simpa

Result:
no goals

Proof state:
case mpr
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
⊢ LawfulBEq α → LawfulBEq (Vector α (n + 1))

Tactic:
intro h

Result:
case mpr
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq α
⊢ LawfulBEq (Vector α (n + 1))

Proof state:
case mp
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
⊢ LawfulBEq α

Tactic:
constructor

Result:
case mp.eq_of_beq
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
⊢ ∀ {a b : α}, (a == b) = true → a = b

case mp.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
⊢ ∀ {a : α}, (a == a) = true

Proof state:
case mpr
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq α
⊢ LawfulBEq (Vector α (n + 1))

Tactic:
constructor

Result:
case mpr.eq_of_beq
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq α
⊢ ∀ {a b : Vector α (n + 1)}, (a == b) = true → a = b

case mpr.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq α
⊢ ∀ {a : Vector α (n + 1)}, (a == a) = true

Proof state:
case mpr.eq_of_beq.mk.mk
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h✝ : LawfulBEq α
a : Array α
ha : a.size = n + 1
b : Array α
hb : b.size = n + 1
h : (a == b) = true
⊢ { toArray := a, size_toArray := ha } = { toArray := b, size_toArray := hb }

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

Result:
case mpr.eq_of_beq.mk.mk.intro
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h✝ : LawfulBEq α
a : Array α
ha : a.size = n + 1
b : Array α
hb : b.size = n + 1
h : (a == b) = true
hs : a.size = b.size
hi : ∀ (i : Nat) (h' : i < a.size), (a[i] == b[i]) = true
⊢ { toArray := a, size_toArray := ha } = { toArray := b, size_toArray := hb }

Proof state:
case mpr.rfl.mk
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq α
a : Array α
ha : a.size = n + 1
⊢ ({ toArray := a, size_toArray := ha } == { toArray := a, size_toArray := ha }) = true

Tactic:
simpa using Array.isEqv_self_beq ..

Result:
no goals

Proof state:
case mp.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
⊢ ∀ {a : α}, (a == a) = true

Tactic:
intro a

Result:
case mp.rfl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
a : α
⊢ (a == a) = true

Proof state:
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : LawfulBEq (Vector α (n + 1))
a : α
this : (n + 1 == 0 || a == a) = true
⊢ (a == a) = true

Tactic:
simpa

Result:
no goals