Theorem: Array.ofFn_data (LeanSAT/Upstream/ToStd.lean)

State before:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).data = List.map f (List.fins n)
Tactic:
ext i x
State after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ x ∈ List.get? (ofFn f).data i ↔ x ∈ List.get? (List.map f (List.fins n)) i

State before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ x ∈ List.get? (ofFn f).data i ↔ x ∈ List.get? (List.map f (List.fins n)) i
Tactic:
simp [List.get?_eq_some]
State after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, List.get (ofFn f).data { val := i, isLt := h } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x

State before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, List.get (ofFn f).data { val := i, isLt := h } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
simp only [← Array.getElem_eq_data_get, Array.getElem_ofFn]
State after:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x

State before:
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) ↔ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
refine ⟨?mp,?mpr⟩
State after:
case mp
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x

case mpr
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
case mp =>
  rintro ⟨h,rfl⟩
  refine ⟨_,?_,rfl⟩
  simpa using h
State after:
no goals

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
Tactic:
case mpr =>
  rintro ⟨_,⟨h,rfl⟩,rfl⟩
  simpa using h
State after:
no goals

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ h, f { val := i, isLt := ⋯ } = x) → ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x
Tactic:
rintro ⟨h,rfl⟩
State after:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = f { val := i, isLt := ⋯ }

State before:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = f { val := i, isLt := ⋯ }
Tactic:
refine ⟨_,?_,rfl⟩
State after:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ h_1, { val := i, isLt := ⋯ } = { val := i, isLt := ⋯ }

State before:
case intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < size (ofFn f)
⊢ ∃ h_1, { val := i, isLt := ⋯ } = { val := i, isLt := ⋯ }
Tactic:
simpa using h
State after:
no goals

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
Tactic:
rintro ⟨_,⟨h,rfl⟩,rfl⟩
State after:
case intro.intro.intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < List.length (List.fins n)
⊢ ∃ h_1, f { val := i, isLt := ⋯ } = f { val := i, isLt := ⋯ }

State before:
case intro.intro.intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < List.length (List.fins n)
⊢ ∃ h_1, f { val := i, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
simpa using h
State after:
no goals