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

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 : ({ toArray := a, size_toArray := ha } == { toArray := b, size_toArray := hb }) = true
⊢ { toArray := a, size_toArray := ha } = { toArray := b, size_toArray := hb }

Tactic:
simp at h

Result:
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 }

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

Tactic:
constructor

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

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

Proof state:
case mpr.eq_of_beq.mk.mk.intro.h
α : 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
i : Nat
h : i < n + 1
⊢ { toArray := a, size_toArray := ha }[i] = { toArray := b, size_toArray := hb }[i]

Tactic:
simpa using hi _ (by omega)

Result:
no goals

Proof state:
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 }

Tactic:
ext i h

Result:
case mpr.eq_of_beq.mk.mk.intro.h
α : 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
i : Nat
h : i < n + 1
⊢ { toArray := a, size_toArray := ha }[i] = { toArray := b, size_toArray := hb }[i]

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 : α
⊢ (mkVector (n + 1) a == mkVector (n + 1) a) = true

Tactic:
simp

Result:
no goals

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
⊢ (mkVector (n + 1) a == mkVector (n + 1) b) = true

Tactic:
rw [mkVector_beq_mkVector]

Result:
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

Proof state:
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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ a = b
⊢ mkVector (n + 1) a = mkVector (n + 1) b

Tactic:
apply eq_of_beq

Result:
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
⊢ (mkVector (n + 1) a == mkVector (n + 1) b) = true

Proof state:
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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ a = b
⊢ a = b

Tactic:
rw [← this]

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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ a = b
⊢ mkVector (n + 1) a = mkVector (n + 1) b

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 : (mkVector (n + 1) a == mkVector (n + 1) a) = true
⊢ (a == a) = true

Tactic:
rw [mkVector_beq_mkVector] at this

Result:
α : 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

Proof state:
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

Tactic:
rintro ⟨a, ha⟩

Result:
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

Proof state:
α : 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
i : Nat
h : i < n + 1
⊢ i < a.size

Tactic:
omega

Result:
no goals

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

Tactic:
intro h

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

Proof state:
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

Tactic:
intro a b h

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 : α
h : (a == b) = true
⊢ a = b

Proof state:
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 : α
h : (a == b) = true
⊢ a = b

Tactic:
have := mkVector_inj (n := n+1) (a := a) (b := b)

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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ n + 1 = 0 ∨ a = b
⊢ a = b

Proof state:
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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ n + 1 = 0 ∨ a = b
⊢ a = b

Tactic:
simp only [Nat.add_one_ne_zero, false_or] at this

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 : α
h : (a == b) = true
this : mkVector (n + 1) a = mkVector (n + 1) b ↔ a = b
⊢ a = b

Proof state:
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

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩ h

Result:
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 : ({ toArray := a, size_toArray := ha } == { toArray := b, size_toArray := hb }) = true
⊢ { toArray := a, size_toArray := ha } = { toArray := b, size_toArray := hb }