internlm/Lean-Github huggingface dataset:
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ¬a < b → a = b ∨ a > b
Tactic:
apply trichot_cases (r:=LT.lt) (motive:=λ a b => ¬ a < b → a=b ∨ a > b)
Proof state after:
case of_rfl
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a

case of_rel
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b

case of_opp
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a
Tactic:
case of_rfl => exact λ _ _ => Or.inl rfl
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b
Tactic:
case of_rel => exact λ _ _ => absurd
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b
Tactic:
case of_opp => exact λ _ _ h _ => Or.inr h
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a
Tactic:
exact λ _ _ => Or.inl rfl
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b
Tactic:
exact λ _ _ => absurd
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b
Tactic:
exact λ _ _ h _ => Or.inr h
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ a = b ∨ a > b → ¬a < b
Tactic:
intro hor hlt
Proof state after:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a = b ∨ a > b
hlt : a < b
⊢ False
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a = b ∨ a > b
hlt : a < b
⊢ False
Tactic:
cases hor
Proof state after:
case inl
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
h✝ : a = b
⊢ False

case inr
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
h✝ : a > b
⊢ False
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
heq : a = b
⊢ False
Tactic:
case inl heq => cases heq; exact Irreflective.irrefl _ hlt
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
hgt : a > b
⊢ False
Tactic:
case inr hgt => exact Asymmetry.asymm _ _ hlt hgt
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
heq : a = b
⊢ False
Tactic:
cases heq
Proof state after:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hlt : a < a
⊢ False
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hlt : a < a
⊢ False
Tactic:
exact Irreflective.irrefl _ hlt
Proof state after:
no goals
Theorem: LinearLT.not_lt_iff_eq_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
hgt : a > b
⊢ False
Tactic:
exact Asymmetry.asymm _ _ hlt hgt
Proof state after:
no goals
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
⊢ a ≠ b
Tactic:
intro heq
Proof state after:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
heq : a = b
⊢ False
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
heq : a = b
⊢ False
Tactic:
cases heq
Proof state after:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hor : a < a ∨ a > a
⊢ False
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hor : a < a ∨ a > a
⊢ False
Tactic:
cases hor
Proof state after:
case refl.inl
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a < a
⊢ False

case refl.inr
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a > a
⊢ False
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a < a
⊢ False
Tactic:
case inl h => exact LinearLT.toLawfulLT.irrefl _ h
Proof state after:
no goals
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a > a
⊢ False
Tactic:
case inr h => exact LinearLT.toLawfulLT.irrefl _ h
Proof state after:
no goals
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a < a
⊢ False
Tactic:
exact LinearLT.toLawfulLT.irrefl _ h
Proof state after:
no goals
Theorem: LinearLT.not_eq_iff_lt_or_gt
Proof state before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a > a
⊢ False
Tactic:
exact LinearLT.toLawfulLT.irrefl _ h
Proof state after:
no goals
Theorem: ArrayLike.get_set_ite
Proof state before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
if h : i = j then
  cases h
  exact Eq.trans (get_set_eq xs i e) (if_pos rfl).symm
else
  exact Eq.trans (get_set_ne xs h e hj) (if_neg h).symm
Proof state after:
no goals
Theorem: ArrayLike.get_set_ite
Proof state before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
h : i = j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
cases h
Proof state after:
case refl
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) i
⊢ (SetElem.setElem xs i e hi)[i] = if i = i then e else xs[i]
Theorem: ArrayLike.get_set_ite
Proof state before:
case refl
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) i
⊢ (SetElem.setElem xs i e hi)[i] = if i = i then e else xs[i]
Tactic:
exact Eq.trans (get_set_eq xs i e) (if_pos rfl).symm
Proof state after:
no goals
Theorem: ArrayLike.get_set_ite
Proof state before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
h : ¬i = j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
exact Eq.trans (get_set_ne xs h e hj) (if_neg h).symm
Proof state after:
no goals
Theorem: ArrayLike.get_mapIdx
Proof state before:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : (fun j ys => ∀ (k : Fin n), (↑k < j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ j → ys[↑k] = xs[↑k])) (↑j) ys
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])
Tactic:
dsimp at *
Proof state after:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])
Theorem: ArrayLike.get_mapIdx
Proof state before:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])
Tactic:
constructor
Proof state after:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
. show k.1 < j.1 + 1 → _
  intro hij
  cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hij) with
  | inl heq =>
    cases (Fin.eq_of_val_eq heq)
    simp only [get_set_eq ys]
    exact congrArg _ <| (IH j).2 .refl
  | inr hlt =>
    have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
    simp only [get_set_ne ys this]
    exact (IH k).1 hlt
Proof state after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
. show k.1 ≥ j.1 + 1 → _
  intro hij
  simp only [get_set_ne ys (Nat.ne_of_lt hij)]
  exact (IH k).2 (Nat.le_of_succ_le hij)
Proof state after:
no goals
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
intro hij
Proof state after:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hij) with
| inl heq =>
  cases (Fin.eq_of_val_eq heq)
  simp only [get_set_eq ys]
  exact congrArg _ <| (IH j).2 .refl
| inr hlt =>
  have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
  simp only [get_set_ne ys this]
  exact (IH k).1 hlt
Proof state after:
no goals
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
heq : ↑k = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
cases (Fin.eq_of_val_eq heq)
Proof state after:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑j] = f j xs[↑j]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑j] = f j xs[↑j]
Tactic:
simp only [get_set_eq ys]
Proof state after:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ f j ys[↑j] = f j xs[↑j]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ f j ys[↑j] = f j xs[↑j]
Tactic:
exact congrArg _ <| (IH j).2 .refl
Proof state after:
no goals
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
Proof state after:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
simp only [get_set_ne ys this]
Proof state after:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ ys[↑k] = f k xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ ys[↑k] = f k xs[↑k]
Tactic:
exact (IH k).1 hlt
Proof state after:
no goals
Theorem: ArrayLike.get_mapIdx
Proof state before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
intro hij
Proof state after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
simp only [get_set_ne ys (Nat.ne_of_lt hij)]
Proof state after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ ys[↑k] = xs[↑k]
Theorem: ArrayLike.get_mapIdx
Proof state before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ ys[↑k] = xs[↑k]
Tactic:
exact (IH k).2 (Nat.le_of_succ_le hij)
Proof state after:
no goals