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

State before:
n : Nat
α✝ : Type u_1
f : Fin n → α✝
i : Nat
h : i < size (init n f)
⊢ (init n f)[i] = f { val := i, isLt := ⋯ }
Tactic:
induction n generalizing i with
| zero => simp at h; exact False.elim <| Nat.not_lt_zero _ h
| succ n ih =>
  simp [init_succ, get_push]
  split
  next h =>
    have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
    simp at this ⊢
    rw [this]
  next h' =>
    simp at h'
    have : i = n := Nat.le_antisymm
      (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
      h'
    cases this
    congr
State after:
no goals

State before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h : i < size (init Nat.zero f)
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }
Tactic:
simp at h
State after:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h✝ : i < size (init Nat.zero f)
h : i < 0
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }

State before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
i : Nat
h✝ : i < size (init Nat.zero f)
h : i < 0
⊢ (init Nat.zero f)[i] = f { val := i, isLt := ⋯ }
Tactic:
exact False.elim <| Nat.not_lt_zero _ h
State after:
no goals

State before:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (init (Nat.succ n) f)[i] = f { val := i, isLt := ⋯ }
Tactic:
simp [init_succ, get_push]
State after:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (if h : i < n then (init n fun i => f { val := ↑i, isLt := ⋯ })[i] else f { val := n, isLt := ⋯ }) =
    f { val := i, isLt := ⋯ }

State before:
case succ
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
⊢ (if h : i < n then (init n fun i => f { val := ↑i, isLt := ⋯ })[i] else f { val := n, isLt := ⋯ }) =
    f { val := i, isLt := ⋯ }
Tactic:
split
State after:
case succ.inl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }

State before:
case succ.inl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
next h =>
  have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
  simp at this ⊢
  rw [this]
State after:
case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }

State before:
case succ.inr
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h✝ : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
next h' =>
  simp at h'
  have : i = n := Nat.le_antisymm
    (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
    h'
  cases this
  congr
State after:
no goals

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
have := @ih (fun i => f ⟨i,Nat.lt_trans i.isLt (by exact Nat.le_refl _)⟩) i (by simp; assumption)
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := ↑{ val := i, isLt := ⋯ }, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := ↑{ val := i, isLt := ⋯ }, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
simp at this ⊢
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
this : (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
⊢ (init n fun i => f { val := ↑i, isLt := ⋯ })[i] = f { val := i, isLt := ⋯ }
Tactic:
rw [this]
State after:
no goals

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i✝ : Nat
h✝ : i✝ < size (init (Nat.succ n) f)
h : i✝ < n
i : Fin n
⊢ n < Nat.succ n
Tactic:
exact Nat.le_refl _
State after:
no goals

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < size (init n fun i => f { val := ↑i, isLt := ⋯ })
Tactic:
simp
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < n

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h✝ : i < size (init (Nat.succ n) f)
h : i < n
⊢ i < n
Tactic:
assumption
State after:
no goals

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : ¬i < n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
simp at h'
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
have : i = n := Nat.le_antisymm
  (Nat.le_of_succ_le_succ (by rw [size_init] at h; exact h))
  h'
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
this : i = n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
this : i = n
⊢ f { val := n, isLt := ⋯ } = f { val := i, isLt := ⋯ }
Tactic:
cases this
State after:
case refl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
h : n < size (init (Nat.succ n) f)
h' : n ≤ n
⊢ f { val := n, isLt := ⋯ } = f { val := n, isLt := ⋯ }

State before:
case refl
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
h : n < size (init (Nat.succ n) f)
h' : n ≤ n
⊢ f { val := n, isLt := ⋯ } = f { val := n, isLt := ⋯ }
Tactic:
congr
State after:
no goals

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < size (init (Nat.succ n) f)
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n
Tactic:
rw [size_init] at h
State after:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < Nat.succ n
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n

State before:
α✝ : Type u_1
n : Nat
ih : ∀ {f : Fin n → α✝} {i : Nat} {h : i < size (init n f)}, (init n f)[i] = f { val := i, isLt := ⋯ }
f : Fin (Nat.succ n) → α✝
i : Nat
h : i < Nat.succ n
h' : n ≤ i
⊢ Nat.succ i ≤ Nat.succ n
Tactic:
exact h
State after:
no goals