-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_eq_decide (a b : Array α) (r) :
    Array.isEqv a b r =
      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false

Proof state:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h✝ : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h✝
h : a.isEqv b r = false
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Proof state:
case pos.intro
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Tactic:
simp [h, w]

Result:
no goals

Proof state:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h✝ : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h✝
h : a.isEqv b r = false
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Tactic:
simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
  Bool.not_eq_true]

Result:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h✝ : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h✝
h : a.isEqv b r = false
⊢ ∀ (h : a.size = b.size), ∃ x h_1, r a[x] b[x] = false

Proof state:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h : ¬a.isEqv b r = true
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Tactic:
let h' := h

Result:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Proof state:
case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h✝ : ¬a.isEqv b r = true
h' : ¬a.isEqv b r = true := h✝
h : a.isEqv b r = false
⊢ ∀ (h : a.size = b.size), ∃ x h_1, r a[x] b[x] = false

Tactic:
simpa [isEqv_iff_rel] using h'

Result:
no goals

Proof state:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Tactic:
obtain ⟨h, w⟩ := h

Result:
case pos.intro
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.size = b.size
w : ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Proof state:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.isEqv b r = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Tactic:
simp only [isEqv_iff_rel] at h

Result:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Proof state:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.isEqv b r = true
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Tactic:
simp only [h, Bool.true_eq]

Result:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.isEqv b r = true
⊢ (if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false) = true

Proof state:
α : Type u_1
a b : Array α
r : α → α → Bool
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

Tactic:
by_cases h : Array.isEqv a b r

Result:
case pos
α : Type u_1
a b : Array α
r : α → α → Bool
h : a.isEqv b r = true
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false

case neg
α : Type u_1
a b : Array α
r : α → α → Bool
h : ¬a.isEqv b r = true
⊢ a.isEqv b r = if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true) else false