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

Proof state:
case mpr
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
⊢ ReflBEq α → ReflBEq (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 : ReflBEq α
⊢ ReflBEq (Vector α (n + 1))

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

Tactic:
intro h

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

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

Tactic:
rintro ⟨v, h⟩

Result:
case mpr.refl.mk
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h✝ : ReflBEq α
v : Array α
h : v.size = n + 1
⊢ ({ toArray := v, size_toArray := h } == { toArray := v, size_toArray := h }) = true

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

Tactic:
suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
  rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
  exact this.2

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

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

Tactic:
simpa using Array.isEqv_self_beq ..

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
constructor

Result:
case mp.refl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : ReflBEq (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 : ReflBEq (Vector α (n + 1))
a : α
this : (mkVector n a == mkVector n a) = true ∧ (a == a) = true
⊢ (a == a) = true

Tactic:
exact this.2

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
intro a

Result:
case mp.refl
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : ReflBEq (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 : ReflBEq (Vector α (n + 1))
a : α
this : (mkVector (n + 1) a == mkVector (n + 1) a) = true
⊢ (a == a) = true

Tactic:
rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this

Result:
α : Type u_1
n✝ : Nat
inst✝¹ : BEq α
inst✝ : NeZero n✝
n : Nat
x✝ : n + 1 ≠ 0
h : ReflBEq (Vector α (n + 1))
a : α
this : (mkVector n a == mkVector n a) = true ∧ (a == a) = true
⊢ (a == a) = true

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

Tactic:
constructor

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