internlm/Lean-Github huggingface dataset:
Theorem: HList.append_assoc
Proof state before:
case cons
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ :: (a✝.append bs).append cs ≅ (a✝¹ :: a✝).append (bs.append cs)
Tactic:
apply HList.cons_hcongr
Proof state after:
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ α✝ = α✝

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ αs✝ ++ βs ++ γs = αs✝ ++ (βs ++ γs)

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ ≅ a✝¹

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
Theorem: HList.append_assoc
Proof state before:
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ α✝ = α✝
Tactic:
reflexivity
Proof state after:
no goals
Theorem: HList.append_assoc
Proof state before:
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ αs✝ ++ βs ++ γs = αs✝ ++ (βs ++ γs)
Tactic:
rw [List.append_assoc]
Proof state after:
no goals
Theorem: HList.append_assoc
Proof state before:
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ ≅ a✝¹
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: HList.append_assoc
Proof state before:
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
Tactic:
exact ih
Proof state after:
no goals
Theorem: ENat.leNat_toNatAux
Proof state before:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (ENat.toNatAux isFinite x) = true
Tactic:
rw [toNatAux_eq]
Proof state after:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (if e.leNat x = true then x else ENat.toNatAux isFinite (x + 1)) = true
Theorem: ENat.leNat_toNatAux
Proof state before:
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (if e.leNat x = true then x else ENat.toNatAux isFinite (x + 1)) = true
Tactic:
split
Proof state after:
case isTrue
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : e.leNat x = true
⊢ e.leNat x = true

case isFalse
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : ¬e.leNat x = true
⊢ e.leNat (ENat.toNatAux isFinite (x + 1)) = true
Theorem: ENat.leNat_toNatAux
Proof state before:
case isTrue
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : e.leNat x = true
⊢ e.leNat x = true
Tactic:
assumption
Proof state after:
no goals
Theorem: ENat.leNat_toNatAux
Proof state before:
case isFalse
e : ENat
isFinite : e.IsFinite
x : Nat
h✝ : ¬e.leNat x = true
⊢ e.leNat (ENat.toNatAux isFinite (x + 1)) = true
Tactic:
apply leNat_toNatAux
Proof state after:
no goals
Theorem: ENat.leNat_toNatAux
Proof state before:
e : ENat
isFinite : e.IsFinite
x : Nat
a✝ : ∀ (y : Nat), (invImage (fun x => ⋯.wrap x) Acc.wfRel).1 y x → e.leNat (ENat.toNatAux isFinite y) = true
h✝ : ¬e.leNat x = true
⊢ (invImage (fun x => ⋯.wrap x) Acc.wfRel).1 (x + 1) x
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.toNatAux_le
Proof state before:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ ENat.toNatAux ⋯ x ≤ y
Tactic:
rw [toNatAux_eq]
Proof state after:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ (if e.leNat x = true then x else ENat.toNatAux ⋯ (x + 1)) ≤ y
Theorem: ENat.toNatAux_le
Proof state before:
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ (if e.leNat x = true then x else ENat.toNatAux ⋯ (x + 1)) ≤ y
Tactic:
split
Proof state after:
case isTrue
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : e.leNat x = true
⊢ x ≤ y

case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ENat.toNatAux ⋯ (x + 1) ≤ y
Theorem: ENat.toNatAux_le
Proof state before:
case isTrue
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : e.leNat x = true
⊢ x ≤ y
Tactic:
exact hle
Proof state after:
no goals
Theorem: ENat.toNatAux_le
Proof state before:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ENat.toNatAux ⋯ (x + 1) ≤ y
Tactic:
apply toNatAux_le hy
Proof state after:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x + 1 ≤ y
Theorem: ENat.toNatAux_le
Proof state before:
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x + 1 ≤ y
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < y
Theorem: ENat.toNatAux_le
Proof state before:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < y
Tactic:
apply Nat.lt_of_le_of_ne hle
Proof state after:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ¬x = y
Theorem: ENat.toNatAux_le
Proof state before:
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ ¬x = y
Tactic:
intro | rfl => contradiction
Proof state after:
no goals
Theorem: ENat.toNatAux_le
Proof state before:
y : Nat
e : ENat
x : Nat
h✝ : ¬e.leNat x = true
x✝ : x = y
hy : e.leNat x = true
hle : x ≤ x
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: ENat.toNatAux_le
Proof state before:
y : Nat
e : ENat
hy : e.leNat y = true
x✝ : (x : Nat) ×' x ≤ y
a✝¹ :
  ∀ (y_1 : (x : Nat) ×' x ≤ y),
    (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 y_1 x✝ → ENat.toNatAux ⋯ y_1.1 ≤ y
x : Nat
hle : x ≤ y
a✝ :
  ∀ (y_1 : (x : Nat) ×' x ≤ y),
    (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 y_1 ⟨x, hle⟩ → ENat.toNatAux ⋯ y_1.1 ≤ y
h✝ : ¬e.leNat x = true
⊢ (invImage (fun x => PSigma.casesOn x fun x hle => ⋯.wrap x) Acc.wfRel).1 ⟨x + 1, ⋯⟩ ⟨x, hle⟩
Tactic:
trivial
Proof state after:
no goals
Theorem: ENat.toNat_le_of_leNat
Proof state before:
e : ENat
x : Nat
h : e.leNat x = true
⊢ e.toNat ⋯ ≤ x
Tactic:
apply toNatAux_le h
Proof state after:
e : ENat
x : Nat
h : e.leNat x = true
⊢ 0 ≤ x
Theorem: ENat.toNat_le_of_leNat
Proof state before:
e : ENat
x : Nat
h : e.leNat x = true
⊢ 0 ≤ x
Tactic:
exact Nat.zero_le x
Proof state after:
no goals
Theorem: ENat.leNat_iff_toNat_le
Proof state before:
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true ↔ e.toNat h ≤ x
Tactic:
constructor
Proof state after:
case mp
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true → e.toNat h ≤ x

case mpr
e : ENat
h : e.IsFinite
x : Nat
⊢ e.toNat h ≤ x → e.leNat x = true
Theorem: ENat.leNat_iff_toNat_le
Proof state before:
case mp
e : ENat
h : e.IsFinite
x : Nat
⊢ e.leNat x = true → e.toNat h ≤ x
Tactic:
exact toNat_le_of_leNat
Proof state after:
no goals
Theorem: ENat.leNat_iff_toNat_le
Proof state before:
case mpr
e : ENat
h : e.IsFinite
x : Nat
⊢ e.toNat h ≤ x → e.leNat x = true
Tactic:
intro h
Proof state after:
case mpr
e : ENat
h✝ : e.IsFinite
x : Nat
h : e.toNat h✝ ≤ x
⊢ e.leNat x = true
Theorem: ENat.leNat_iff_toNat_le
Proof state before:
case mpr
e : ENat
h✝ : e.IsFinite
x : Nat
h : e.toNat h✝ ≤ x
⊢ e.leNat x = true
Tactic:
exact mono h (leNat_toNat ..)
Proof state after:
no goals
Theorem: ENat.toNat_ofNat
Proof state before:
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ = x
Tactic:
apply Nat.le_antisymm
Proof state after:
case h₁
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ ≤ x

case h₂
x : Nat
⊢ x ≤ (ENat.ofNat x).toNat ⋯
Theorem: ENat.toNat_ofNat
Proof state before:
case h₁
x : Nat
⊢ (ENat.ofNat x).toNat ⋯ ≤ x
Tactic:
rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le]
Proof state after:
case h₁
x : Nat
⊢ x ≤ x
Theorem: ENat.toNat_ofNat
Proof state before:
case h₁
x : Nat
⊢ x ≤ x
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂
x : Nat
⊢ x ≤ (ENat.ofNat x).toNat ⋯
Tactic:
cases x with
| zero => exact Nat.zero_le _
| succ x =>
  apply Nat.succ_le_of_lt
  apply Nat.not_le.1
  intro (h : _ ≤ x)
  rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le] at h
  apply Nat.not_lt.2 h
  exact Nat.lt_succ_self _
Proof state after:
no goals
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.zero

⊢ 0 ≤ (ENat.ofNat 0).toNat ⋯
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ
x : Nat
⊢ x + 1 ≤ (ENat.ofNat (x + 1)).toNat ⋯
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case h₂.succ.h
x : Nat
⊢ x < (ENat.ofNat (x + 1)).toNat ⋯
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ.h
x : Nat
⊢ x < (ENat.ofNat (x + 1)).toNat ⋯
Tactic:
apply Nat.not_le.1
Proof state after:
case h₂.succ.h
x : Nat
⊢ ¬(ENat.ofNat (x + 1)).toNat ⋯ ≤ x
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ.h
x : Nat
⊢ ¬(ENat.ofNat (x + 1)).toNat ⋯ ≤ x
Tactic:
intro (h : _ ≤ x)
Proof state after:
case h₂.succ.h
x : Nat
h : (ENat.ofNat (x + 1)).toNat ⋯ ≤ x
⊢ False
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ.h
x : Nat
h : (ENat.ofNat (x + 1)).toNat ⋯ ≤ x
⊢ False
Tactic:
rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le] at h
Proof state after:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ False
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ False
Tactic:
apply Nat.not_lt.2 h
Proof state after:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ x < x + 1
Theorem: ENat.toNat_ofNat
Proof state before:
case h₂.succ.h
x : Nat
h : x + 1 ≤ x
⊢ x < x + 1
Tactic:
exact Nat.lt_succ_self _
Proof state after:
no goals
Theorem: ENat.ofNat_toNat
Proof state before:
e : ENat
h : e.IsFinite
⊢ ENat.ofNat (e.toNat h) = e
Tactic:
ext x
Proof state after:
case leNat.h
e : ENat
h : e.IsFinite
x : Nat
⊢ (ENat.ofNat (e.toNat h)).leNat x = e.leNat x
Theorem: ENat.ofNat_toNat
Proof state before:
case leNat.h
e : ENat
h : e.IsFinite
x : Nat
⊢ (ENat.ofNat (e.toNat h)).leNat x = e.leNat x
Tactic:
cases hx : e.leNat x with
| true => rw [leNat_coe_eq_true_iff_le, ←leNat_iff_toNat_le, hx]
| false =>
rw [←Bool.not_eq_true] at hx ⊢
apply mt _ hx
intro hx
rw [leNat_iff_toNat_le _ h]
rwa [leNat_coe_eq_true_iff_le] at hx
Proof state after:
no goals
Theorem: ENat.ofNat_toNat
Proof state before:
case leNat.h.true
e : ENat
h : e.IsFinite
x : Nat
hx : e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true
Tactic:
rw [leNat_coe_eq_true_iff_le, ←leNat_iff_toNat_le, hx]
Proof state after:
no goals
Theorem: ENat.ofNat_toNat
Proof state before:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : e.leNat x = false
⊢ (ENat.ofNat (e.toNat h)).leNat x = false
Tactic:
rw [←Bool.not_eq_true] at hx ⊢
Proof state after:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ ¬(ENat.ofNat (e.toNat h)).leNat x = true
Theorem: ENat.ofNat_toNat
Proof state before:
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ ¬(ENat.ofNat (e.toNat h)).leNat x = true
Tactic:
apply mt _ hx
Proof state after:
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true
Theorem: ENat.ofNat_toNat
Proof state before:
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true
Tactic:
intro hx
Proof state after:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.leNat x = true
Theorem: ENat.ofNat_toNat
Proof state before:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.leNat x = true
Tactic:
rw [leNat_iff_toNat_le _ h]
Proof state after:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.toNat h ≤ x
Theorem: ENat.ofNat_toNat
Proof state before:
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.toNat h ≤ x
Tactic:
rwa [leNat_coe_eq_true_iff_le] at hx
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
h : as ≠ []
⊢ List.length (toDiffs as h).snd < List.length as
Tactic:
match as with
| [] => exact False.elim (h rfl)
| _ :: [] => simp [toDiffs]
| head :: neck :: tail =>
  simp only [toDiffs]
  refine Nat.succ_lt_succ ?_
  calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
       _ = tail.length + 1 := by simp
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
h : [] ≠ []
⊢ List.length (toDiffs [] h).snd < List.length []
Tactic:
exact False.elim (h rfl)
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head✝ : Int
h : [head✝] ≠ []
⊢ List.length (toDiffs [head✝] h).snd < List.length [head✝]
Tactic:
simp [toDiffs]
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (head :: neck :: tail) h).snd < List.length (head :: neck :: tail)
Tactic:
simp only [toDiffs]
Proof state after:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length
      (((toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).fst - head) ::
        (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd) <
    List.length (head :: neck :: tail)
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length
      (((toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).fst - head) ::
        (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd) <
    List.length (head :: neck :: tail)
Tactic:
refine Nat.succ_lt_succ ?_
Proof state after:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd < List.length (neck :: tail)
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd < List.length (neck :: tail)
Tactic:
calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
     _ = tail.length + 1 := by simp
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ neck :: tail ≠ []
Tactic:
simp
Proof state after:
no goals
Theorem: Day09.toDiffs_length_lt
Proof state before:
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (neck :: tail) = List.length tail + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Array.getElem_mkArray
Proof state before:
α : Type ?u.25800
n : Nat
a : α
i : Nat
hi : i < n
⊢ i < size (mkArray n a)
Tactic:
simp [size_mkArray, hi]
Proof state after:
no goals
Theorem: Array.getElem_mkArray
Proof state before:
α : Type u_1
n : Nat
a : α
i : Nat
hi : i < n
⊢ let_fun this := (_ : i < size (mkArray n a));
  (mkArray n a)[i] = a
Tactic:
simp only [mkArray, Array.getElem_eq_data_get, List.get_replicate]
Proof state after:
no goals
Theorem: Vec₂.size_val
Proof state before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
⊢ Array.size as.val = n
Tactic:
rw [as.property.1]
Proof state after:
no goals
Theorem: Vec₂.size_val_get_fin
Proof state before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Fin (Array.size as.val)
⊢ Array.size as.val[i] = m
Tactic:
simp only [getElem_fin, as.property.2 i i.isLt]
Proof state after:
no goals
Theorem: Vec₂.size_val_get
Proof state before:
n m : Nat
α : Type ?u.31992
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ i < Array.size as.val
Tactic:
simp [hi]
Proof state after:
no goals
Theorem: Vec₂.size_val_get
Proof state before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ Array.size as.val[i] = m
Tactic:
have : i < as.val.size := by rwa [as.property.1]
Proof state after:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
this : i < Array.size as.val
⊢ Array.size as.val[i] = m
Theorem: Vec₂.size_val_get
Proof state before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
this : i < Array.size as.val
⊢ Array.size as.val[i] = m
Tactic:
simp [as.property.2 i this]
Proof state after:
no goals
Theorem: Vec₂.size_val_get
Proof state before:
n m : Nat
α : Type u_1
as : Vec₂ n m α
i : Nat
hi : i < n
⊢ i < Array.size as.val
Tactic:
rwa [as.property.1]
Proof state after:
no goals
Theorem: Vec₂.size_toArrayVec
Proof state before:
n m : Nat
α : Type u_1
grid : Vec₂ n m α
⊢ Array.size (toArrayVec grid) = n
Tactic:
rw [toArrayVec, Array.size_mapIdx, grid.property.1]
Proof state after:
no goals
Theorem: ArraySet.contains_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ contains as x = true ↔ x ∈ as
Tactic:
rw [contains]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ Array.contains as.content x = true ↔ x ∈ as
Theorem: ArraySet.contains_iff
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ Array.contains as.content x = true ↔ x ∈ as
Tactic:
exact Array.contains_def
Proof state after:
no goals
Theorem: ArraySet.not_eq_getElem_of_not_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
⊢ ∀ (i : Nat) (h : i < Array.size as.content), as.content[i] ≠ x
Tactic:
intro i hi
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Theorem: ArraySet.not_eq_getElem_of_not_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Tactic:
rw [mem_def, Array.mem_def, List.mem_iff_get, not_exists] at hx
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∀ (x_1 : Fin (List.length as.content.data)), ¬List.get as.content.data x_1 = x
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Theorem: ArraySet.not_eq_getElem_of_not_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∀ (x_1 : Fin (List.length as.content.data)), ¬List.get as.content.data x_1 = x
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Tactic:
specialize hx ⟨i, hi⟩
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Nat
hi : i < Array.size as.content
hx : ¬List.get as.content.data { val := i, isLt := hi } = x
⊢ as.content[i] ≠ x
Theorem: ArraySet.not_eq_getElem_of_not_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Nat
hi : i < Array.size as.content
hx : ¬List.get as.content.data { val := i, isLt := hi } = x
⊢ as.content[i] ≠ x
Tactic:
rwa [Array.getElem_eq_data_get]
Proof state after:
no goals
Theorem: ArraySet.exists_getElem_of_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : x ∈ as
⊢ ∃ i, as.content[i] = x
Tactic:
rw [mem_def, Array.mem_def, List.mem_iff_get] at hx
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∃ n, List.get as.content.data n = x
⊢ ∃ i, as.content[i] = x
Theorem: ArraySet.exists_getElem_of_mem
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∃ n, List.get as.content.data n = x
⊢ ∃ i, as.content[i] = x
Tactic:
obtain ⟨i, hi⟩ := hx
Proof state after:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ ∃ i, as.content[i] = x
Theorem: ArraySet.exists_getElem_of_mem
Proof state before:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ ∃ i, as.content[i] = x
Tactic:
refine ⟨i, ?_⟩
Proof state after:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ as.content[i] = x
Theorem: ArraySet.exists_getElem_of_mem
Proof state before:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ as.content[i] = x
Tactic:
rwa [← Array.getElem_eq_data_get] at hi
Proof state after:
no goals
Theorem: Nat.eq_of_le_of_le
Proof state before:
n m : Nat
h₁ : n ≤ m
h₂ : m ≤ n
⊢ n = m
Tactic:
simp [Nat.le_antisymm_iff, h₁, h₂]
Proof state after:
no goals
Theorem: easy
Proof state before:
P Q R S : Prop
⊢ P → P
Tactic:
intro h
Proof state after:
P Q R S : Prop
h : P
⊢ P
Theorem: easy
Proof state before:
P Q R S : Prop
h : P
⊢ P
Tactic:
apply h
Proof state after:
no goals
Theorem: sum_odds_eq_square
Proof state before:
n : ℕ
⊢ sum_odds n = n ^ 2
Tactic:
induction n with
| zero =>
    rw [sum_odds, Nat.zero_eq, pow_two, zero_mul]
| succ n ih =>
    rw [sum_odds, ih, Nat.succ_eq_add_one]
    ring
Proof state after:
no goals
Theorem: sum_odds_eq_square
Proof state before:
case zero

⊢ sum_odds Nat.zero = Nat.zero ^ 2
Tactic:
rw [sum_odds, Nat.zero_eq, pow_two, zero_mul]
Proof state after:
no goals
Theorem: sum_odds_eq_square
Proof state before:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ sum_odds (Nat.succ n) = Nat.succ n ^ 2
Tactic:
rw [sum_odds, ih, Nat.succ_eq_add_one]
Proof state after:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ 2 * n + 1 + n ^ 2 = (n + 1) ^ 2
Theorem: sum_odds_eq_square
Proof state before:
case succ
n : ℕ
ih : sum_odds n = n ^ 2
⊢ 2 * n + 1 + n ^ 2 = (n + 1) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: zero_add'
Proof state before:
n : ℕ
⊢ add' 0 n = n
Tactic:
induction n with
| zero => rw [add']
| succ n ih => rw [add', ih]
Proof state after:
no goals
Theorem: zero_add'
Proof state before:
case zero

⊢ add' 0 zero = zero
Tactic:
rw [add']
Proof state after:
no goals
Theorem: zero_add'
Proof state before:
case succ
n : ℕ
ih : add' 0 n = n
⊢ add' 0 (succ n) = succ n
Tactic:
rw [add', ih]
Proof state after:
no goals
Theorem: succ_add'
Proof state before:
m n : ℕ
⊢ add' (succ m) n = succ (add' m n)
Tactic:
induction n with
| zero => rw [add', add']
| succ n ih => rw [add', ih, add']
Proof state after:
no goals
Theorem: succ_add'
Proof state before:
case zero
m : ℕ
⊢ add' (succ m) zero = succ (add' m zero)
Tactic:
rw [add', add']
Proof state after:
no goals
Theorem: succ_add'
Proof state before:
case succ
m n : ℕ
ih : add' (succ m) n = succ (add' m n)
⊢ add' (succ m) (succ n) = succ (add' m (succ n))
Tactic:
rw [add', ih, add']
Proof state after:
no goals
Theorem: add'_comm
Proof state before:
m n : ℕ
⊢ add' m n = add' n m
Tactic:
induction m with
| zero =>
  rw [zero_eq, zero_add', add']
| succ m ih =>
  rw [add', succ_add', ih]
Proof state after:
no goals
Theorem: add'_comm
Proof state before:
case zero
n : ℕ
⊢ add' zero n = add' n zero
Tactic:
rw [zero_eq, zero_add', add']
Proof state after:
no goals
Theorem: add'_comm
Proof state before:
case succ
n m : ℕ
ih : add' m n = add' n m
⊢ add' (succ m) n = add' n (succ m)
Tactic:
rw [add', succ_add', ih]
Proof state after:
no goals
Theorem: append_nil'
Proof state before:
α : Type
as bs cs : List α
a b c : α
⊢ as ++ [] = as
Tactic:
induction as with
| nil => rw [nil_append]
| cons a as ih => rw [cons_append, ih]
Proof state after:
no goals
Theorem: append_nil'
Proof state before:
case nil
α : Type
as bs cs : List α
a b c : α
⊢ [] ++ [] = []
Tactic:
rw [nil_append]
Proof state after:
no goals
Theorem: append_nil'
Proof state before:
case cons
α : Type
as✝ bs cs : List α
a✝ b c a : α
as : List α
ih : as ++ [] = as
⊢ a :: as ++ [] = a :: as
Tactic:
rw [cons_append, ih]
Proof state after:
no goals