internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.zipWith_push
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) (f a b) =
    push (mapIdx (fun i => f x[i]) y) (f a b)
Tactic:
apply congrFun
Proof state after:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) =
    push (mapIdx (fun i => f x[i]) y)
Theorem: SizedArray.zipWith_push
Proof state before:
case h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ push (mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y) =
    push (mapIdx (fun i => f x[i]) y)
Tactic:
apply congrArg
Proof state after:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y = mapIdx (fun i => f x[i]) y
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ mapIdx (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) y = mapIdx (fun i => f x[i]) y
Tactic:
apply congrFun
Proof state after:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (mapIdx fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun y => mapIdx (fun i => f x[i]) y
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (mapIdx fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun y => mapIdx (fun i => f x[i]) y
Tactic:
apply congrArg
Proof state after:
case h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun i => f x[i]
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
⊢ (fun i => f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }]) = fun i => f x[i]
Tactic:
funext i
Proof state after:
case h.h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Fin n
⊢ f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }] = f x[i]
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h.h.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Fin n
⊢ f (push x a)[{ val := ↑i, isLt := (_ : ↑i < Nat.succ n) }] = f x[i]
Tactic:
cases i with | mk i h =>
apply congrArg
show (push x a)[i]'(.step h) = x[i]'h
rw [get_push, dif_pos h]
Proof state after:
no goals
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h.h.h.mk
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ f (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    f x[{ val := i, isLt := h }]
Tactic:
apply congrArg
Proof state after:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    x[{ val := i, isLt := h }]
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[{ val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }] =
    x[{ val := i, isLt := h }]
Tactic:
show (push x a)[i]'(.step h) = x[i]'h
Proof state after:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[i] = x[i]
Theorem: SizedArray.zipWith_push
Proof state before:
case h.h.h.h.h.mk.h
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
a : α
y : SizedArray β n
b : β
f : α → β → γ
i : Nat
h : i < n
⊢ (push x a)[i] = x[i]
Tactic:
rw [get_push, dif_pos h]
Proof state after:
no goals
Theorem: SizedArray.get_zipWith
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
y : SizedArray β n
f : α → β → γ
i : Nat
h : i < n
⊢ (zipWith x y f)[i] = f x[i] y[i]
Tactic:
induction x, y using cons_induction_on₂ generalizing i with
| empty => cases h
| cons a x b y IH =>
  simp only [zipWith_cons]
  cases i with
  | zero => simp only [get_cons_zero]
  | succ i =>
    simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
    exact IH
Proof state after:
no goals
Theorem: SizedArray.get_zipWith
Proof state before:
case empty
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
i : Nat
h : i < 0
⊢ (zipWith empty empty f)[i] = f empty[i] empty[i]
Tactic:
cases h
Proof state after:
no goals
Theorem: SizedArray.get_zipWith
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (zipWith (cons a x) (cons b y) f)[i] = f (cons a x)[i] (cons b y)[i]
Tactic:
simp only [zipWith_cons]
Proof state after:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[i] = f (cons a x)[i] (cons b y)[i]
Theorem: SizedArray.get_zipWith
Proof state before:
case cons
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[i] = f (cons a x)[i] (cons b y)[i]
Tactic:
cases i with
| zero => simp only [get_cons_zero]
| succ i =>
  simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
  exact IH
Proof state after:
no goals
Theorem: SizedArray.get_zipWith
Proof state before:
case cons.zero
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
h : Nat.zero < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[Nat.zero] = f (cons a x)[Nat.zero] (cons b y)[Nat.zero]
Tactic:
simp only [get_cons_zero]
Proof state after:
no goals
Theorem: SizedArray.get_zipWith
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (cons (f a b) (zipWith x y f))[Nat.succ i] = f (cons a x)[Nat.succ i] (cons b y)[Nat.succ i]
Tactic:
simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
Proof state after:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (zipWith x y f)[i] = f x[i] y[i]
Theorem: SizedArray.get_zipWith
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : ∀ {i : Nat} {h : i < n✝}, (zipWith x y f)[i] = f x[i] y[i]
i : Nat
h : Nat.succ i < n✝ + 1
⊢ (zipWith x y f)[i] = f x[i] y[i]
Tactic:
exact IH
Proof state after:
no goals
Theorem: SizedArray.zipWith_flip
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ zipWith (cons b y) (cons a x) (flip f) = zipWith (cons a x) (cons b y) f
Tactic:
simp only [zipWith_cons]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ cons (flip f b a) (zipWith y x (flip f)) = cons (f a b) (zipWith x y f)
Theorem: SizedArray.zipWith_flip
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x✝ : SizedArray α n
y✝ : SizedArray β n
f : α → β → γ
n✝ : Nat
a : α
x : SizedArray α n✝
b : β
y : SizedArray β n✝
IH : zipWith y x (flip f) = zipWith x y f
⊢ cons (flip f b a) (zipWith y x (flip f)) = cons (f a b) (zipWith x y f)
Tactic:
exact congrArg (cons (f a b)) IH
Proof state after:
no goals
Theorem: SizedArray.zipWith_zipWith_left
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) z g = zipWith₃ (cons a x) (cons b y) z fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
Tactic:
rw [← z.cons_head_tail]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) (cons (head z) (tail z)) g =
    zipWith₃ (cons a x) (cons b y) (cons (head z) (tail z)) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
Theorem: SizedArray.zipWith_zipWith_left
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ zipWith (zipWith (cons a x) (cons b y) f) (cons (head z) (tail z)) g =
    zipWith₃ (cons a x) (cons b y) (cons (head z) (tail z)) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
Tactic:
simp only [zipWith_cons, zipWith₃_cons]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ cons (g (f a b) (head z)) (zipWith (zipWith x y f) (tail z) g) =
    cons (g (f a b) (head z)) (zipWith₃ x y (tail z) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂)
Theorem: SizedArray.zipWith_zipWith_left
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray α₂ n
f : α₁ → α₂ → β₁
z✝ : SizedArray β₂ n
g : β₁ → β₂ → γ
n✝ : Nat
a : α₁
x : SizedArray α₁ n✝
b : α₂
y : SizedArray α₂ n✝
IH : ∀ (x_1 : SizedArray β₂ n✝), zipWith (zipWith x y f) x_1 g = zipWith₃ x y x_1 fun a₁ a₂ b₂ => g (f a₁ a₂) b₂
z : SizedArray β₂ (n✝ + 1)
⊢ cons (g (f a b) (head z)) (zipWith (zipWith x y f) (tail z) g) =
    cons (g (f a b) (head z)) (zipWith₃ x y (tail z) fun a₁ a₂ b₂ => g (f a₁ a₂) b₂)
Tactic:
rw [IH z.tail]
Proof state after:
no goals
Theorem: SizedArray.zipWith_zipWith_right
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray β₁ n
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith x (zipWith (cons b y) (cons c z) f) g = zipWith₃ x (cons b y) (cons c z) fun a b c => g a (f b c)
Tactic:
rw [← x.cons_head_tail]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray β₁ n
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith (cons (head x) (tail x)) (zipWith (cons b y) (cons c z) f) g =
    zipWith₃ (cons (head x) (tail x)) (cons b y) (cons c z) fun a b c => g a (f b c)
Theorem: SizedArray.zipWith_zipWith_right
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray β₁ n
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ zipWith (cons (head x) (tail x)) (zipWith (cons b y) (cons c z) f) g =
    zipWith₃ (cons (head x) (tail x)) (cons b y) (cons c z) fun a b c => g a (f b c)
Tactic:
simp only [zipWith_cons, zipWith₃_cons]
Proof state after:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray β₁ n
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ cons (g (head x) (f b c)) (zipWith (tail x) (zipWith y z f) g) =
    cons (g (head x) (f b c)) (zipWith₃ (tail x) y z fun a b c => g a (f b c))
Theorem: SizedArray.zipWith_zipWith_right
Proof state before:
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
α₁ : Type u₁
α₂ : Type u₂
β₁ : Type v₁
β₂ : Type v₂
x✝ : SizedArray α₁ n
y✝ : SizedArray β₁ n
z✝ : SizedArray β₂ n
f : β₁ → β₂ → α₂
g : α₁ → α₂ → γ
n✝ : Nat
b : β₁
y : SizedArray β₁ n✝
c : β₂
z : SizedArray β₂ n✝
IH : ∀ (x : SizedArray α₁ n✝), zipWith x (zipWith y z f) g = zipWith₃ x y z fun a b c => g a (f b c)
x : SizedArray α₁ (n✝ + 1)
⊢ cons (g (head x) (f b c)) (zipWith (tail x) (zipWith y z f) g) =
    cons (g (head x) (f b c)) (zipWith₃ (tail x) y z fun a b c => g a (f b c))
Tactic:
rw [IH x.tail]
Proof state after:
no goals
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Nodup x ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
dsimp [Nodup]
Proof state after:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Array.Nodup x.val ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Array.Nodup x.val ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
rewrite [Array.nodup_iff_getElem_inj]
Proof state after:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
constructor
Proof state after:
case mp
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) → ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mp
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) → ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
Tactic:
all_goals
  intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  specialize h ⟨i, x.size_eq.symm ▸ hi⟩ ⟨j, x.size_eq.symm ▸ hj⟩ hxij
  cases h; rfl
Proof state after:
no goals
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
Tactic:
intro h i j hxij
Proof state after:
case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i j : Fin (Array.size x.val)
hxij : x.val[↑i] = x.val[↑j]
⊢ i = j
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i j : Fin (Array.size x.val)
hxij : x.val[↑i] = x.val[↑j]
⊢ i = j
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mpr.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
j : Fin (Array.size x.val)
i : Nat
hi : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑j]
⊢ { val := i, isLt := hi } = j
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
j : Fin (Array.size x.val)
i : Nat
hi : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑j]
⊢ { val := i, isLt := hi } = j
Tactic:
rcases j with ⟨j,hj⟩
Proof state after:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
specialize h ⟨i, x.size_eq.symm ▸ hi⟩ ⟨j, x.size_eq.symm ▸ hj⟩ hxij
Proof state after:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
h : { val := i, isLt := (_ : i < n) } = { val := j, isLt := (_ : j < n) }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
h : { val := i, isLt := (_ : i < n) } = { val := j, isLt := (_ : j < n) }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
cases h
Proof state after:
case mpr.mk.mk.refl
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi hj : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := i, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }
Theorem: SizedArray.nodup_iff_get_inj
Proof state before:
case mpr.mk.mk.refl
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi hj : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := i, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.eq_of_div_mod_two_eq
Proof state before:
m n : Nat
hdiv : m / 2 = n / 2
hmod : m % 2 = n % 2
⊢ 2 * (m / 2) + m % 2 = 2 * (n / 2) + n % 2
Tactic:
rw [hdiv, hmod]
Proof state after:
no goals
Theorem: Nat.eq_mod2_of_decide
Proof state before:
m n : Nat
⊢ decide (m % 2 = 1) = decide (n % 2 = 1) → m % 2 = n % 2
Tactic:
cases m.mod_two_eq_zero_or_one <;> cases n.mod_two_eq_zero_or_one
<;> rw [‹m%2=_›, ‹n%2=_›] <;> intro hdec <;> cases hdec <;> rfl
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
n k : Nat
⊢ n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
Tactic:
intro hn i hi
Proof state after:
n k : Nat
hn : n < 2 ^ k
i : Nat
hi : i ≥ k
⊢ getBit n i = false
Theorem: Nat.getBit_high
Proof state before:
n k : Nat
hn : n < 2 ^ k
i : Nat
hi : i ≥ k
⊢ getBit n i = false
Tactic:
induction k generalizing n i
Proof state after:
case zero
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false

case succ
n✝ : Nat
n_ih✝ : ∀ {n : Nat}, n < 2 ^ n✝ → ∀ (i : Nat), i ≥ n✝ → getBit n i = false
n : Nat
hn : n < 2 ^ succ n✝
i : Nat
hi : i ≥ succ n✝
⊢ getBit n i = false
Theorem: Nat.getBit_high
Proof state before:
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false
Tactic:
case zero => cases Nat.eq_zero_of_lt_one hn; exact zero_getBit i
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
⊢ getBit n i = false
Tactic:
case succ k h_ind =>
  have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
  cases hi
  case refl =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› k Nat.le.refl
  case step i hstep =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false
Tactic:
cases Nat.eq_zero_of_lt_one hn
Proof state after:
case refl
i : Nat
hi : i ≥ zero
hn : 0 < 2 ^ zero
⊢ getBit 0 i = false
Theorem: Nat.getBit_high
Proof state before:
case refl
i : Nat
hi : i ≥ zero
hn : 0 < 2 ^ zero
⊢ getBit 0 i = false
Tactic:
exact zero_getBit i
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
⊢ getBit n i = false
Tactic:
have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
Proof state after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
this : n / 2 < 2 ^ k
⊢ getBit n i = false