Theorem: Array.getElem_ofFn' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (ofFn f)[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
simp only [ofFn_succ f, get_push']
State after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
if h' : i < size (ofFn λ x => f ⟨x.1, Nat.lt_succ_of_lt x.2⟩)
then rw [dif_pos h']; exact IH _ h'
else
  rw [dif_neg h']
  suffices i = n by cases this; rfl
  simp only [size_ofFn] at h h'
  exact Nat.le_antisymm (Nat.le_of_succ_le_succ h) (Nat.ge_of_not_lt h')
State after:
no goals

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
rw [dif_pos h']
State after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i] = f { val := i, isLt := (_ : i < Nat.succ n) }

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
exact IH _ h'
State after:
no goals

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
rw [dif_neg h']
State after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
suffices i = n by cases this; rfl
State after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ i = n

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ i = n
Tactic:
simp only [size_ofFn] at h h'
State after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < Nat.succ n
h' : ¬i < n
⊢ i = n

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < Nat.succ n
h' : ¬i < n
⊢ i = n
Tactic:
exact Nat.le_antisymm (Nat.le_of_succ_le_succ h) (Nat.ge_of_not_lt h')
State after:
no goals

State before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
this : i = n
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
cases this
State after:
case refl
α : Type u
n : Nat
f✝ : Fin n → α
i : Nat
IH : ∀ (x : Fin i → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < i) }
f : Fin (Nat.succ i) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ i) })
⊢ f { val := i, isLt := (_ : i < Nat.succ i) } = f { val := i, isLt := (_ : i < Nat.succ i) }

State before:
case refl
α : Type u
n : Nat
f✝ : Fin n → α
i : Nat
IH : ∀ (x : Fin i → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < i) }
f : Fin (Nat.succ i) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ i) })
⊢ f { val := i, isLt := (_ : i < Nat.succ i) } = f { val := i, isLt := (_ : i < Nat.succ i) }
Tactic:
rfl
State after:
no goals