internlm/Lean-Github huggingface dataset:
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val (⋯ ▸ j).val
Tactic:
rw [val_ndrec]
Proof state after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val j.val
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r i.val j.val
Tactic:
exact h
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
Tactic:
rw [eqNdrec_symm]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (dedup s i).tail = ⋯ ▸ j
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
match hj : this ▸ j with
| head =>
  rw [eqNdrec_symm] at hj
  rw [hj, val_ndrec, val_head] at h
  absurd ha
  apply Logic.Any.of_index (i.map (s.r x))
  rw [val_map]
  symmetry
  exact h
| tail j =>
  rw [eqNdrec_symm] at hj
  rw [hj, val_ndrec, val_tail] at h
  rw [hj, ih h]
  elim_casts
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : this ▸ j = head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
rw [eqNdrec_symm] at hj
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
rw [hj, val_ndrec, val_head] at h
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (dedup s i).tail = ⋯ ▸ j
Tactic:
absurd ha
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Logic.Any (List.map (Setoid.r x) xs)
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Logic.Any (List.map (Setoid.r x) xs)
Tactic:
apply Logic.Any.of_index (i.map (s.r x))
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (map (Setoid.r x) i).val
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ (map (Setoid.r x) i).val
Tactic:
rw [val_map]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r x i.val
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r x i.val
Tactic:
symmetry
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r i.val x
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
h : Setoid.r i.val x
hj : j = ⋯ ▸ head
⊢ Setoid.r i.val x
Tactic:
exact h
Proof state after:
no goals
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : this ▸ j✝ = j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [eqNdrec_symm] at hj
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [hj, val_ndrec, val_tail] at h
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ (dedup s i).tail = ⋯ ▸ j✝
Tactic:
rw [hj, ih h]
Proof state after:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ j.tail = ⋯ ▸ ⋯ ▸ j.tail
Theorem: List.Index.dedup_eq_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j✝ : (List.dedup s (x :: xs)).Index
i : xs.Index
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
h : Setoid.r i.val j.val
hj : j✝ = ⋯ ▸ j.tail
⊢ j.tail = ⋯ ▸ ⋯ ▸ j.tail
Tactic:
elim_casts
Proof state after:
no goals
Theorem: List.Index.dedup_eq_iff_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j ↔ Setoid.r i.val j.val
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j → Setoid.r i.val j.val

case mpr
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ Setoid.r i.val j.val → dedup s i = j
Theorem: List.Index.dedup_eq_iff_rel
Proof state before:
case mp
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j → Setoid.r i.val j.val
Tactic:
intro | rfl => exact val_dedup ..
Proof state after:
no goals
Theorem: List.Index.dedup_eq_iff_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
x✝ : dedup s i = j
⊢ Setoid.r i.val (dedup s i).val
Tactic:
exact val_dedup ..
Proof state after:
no goals
Theorem: List.Index.dedup_eq_iff_rel
Proof state before:
case mpr
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ Setoid.r i.val j.val → dedup s i = j
Tactic:
exact dedup_eq_of_rel s
Proof state after:
no goals
Theorem: List.Index.dedup_eq_dedup_of_rel
Proof state before:
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ dedup s i = dedup s j
Tactic:
apply dedup_eq_of_rel
Proof state after:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val (dedup s j).val
Theorem: List.Index.dedup_eq_dedup_of_rel
Proof state before:
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val (dedup s j).val
Tactic:
transitivity j.val
Proof state after:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val j.val

case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r j.val (dedup s j).val
Theorem: List.Index.dedup_eq_dedup_of_rel
Proof state before:
case h.left
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val j.val
Tactic:
exact h
Proof state after:
no goals
Theorem: List.Index.dedup_eq_dedup_of_rel
Proof state before:
case h.right
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r j.val (dedup s j).val
Tactic:
exact val_dedup ..
Proof state after:
no goals
Theorem: ENat.mono_add
Proof state before:
n m : Nat
x : ENat
⊢ x.leNat n = true → x.leNat (n + m) = true
Tactic:
intro h
Proof state after:
n m : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + m) = true
Theorem: ENat.mono_add
Proof state before:
n m : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + m) = true
Tactic:
induction m with
| zero => exact h
| succ _ h => exact mono_step _ h
Proof state after:
no goals
Theorem: ENat.mono_add
Proof state before:
case zero
n : Nat
x : ENat
h : x.leNat n = true
⊢ x.leNat (n + 0) = true
Tactic:
exact h
Proof state after:
no goals
Theorem: ENat.mono_add
Proof state before:
case succ
n : Nat
x : ENat
h✝ : x.leNat n = true
n✝ : Nat
h : x.leNat (n + n✝) = true
⊢ x.leNat (n + (n✝ + 1)) = true
Tactic:
exact mono_step _ h
Proof state after:
no goals
Theorem: ENat.mono
Proof state before:
n m : Nat
x : ENat
⊢ n ≤ m → x.leNat n = true → x.leNat m = true
Tactic:
intro h hx
Proof state after:
n m : Nat
x : ENat
h : n ≤ m
hx : x.leNat n = true
⊢ x.leNat m = true
Theorem: ENat.mono
Proof state before:
n m : Nat
x : ENat
h : n ≤ m
hx : x.leNat n = true
⊢ x.leNat m = true
Tactic:
match Nat.le.dest h with
| ⟨_, h⟩ => cases h; exact mono_add hx
Proof state after:
no goals
Theorem: ENat.mono
Proof state before:
n m : Nat
x : ENat
h✝ : n ≤ m
hx : x.leNat n = true
w✝ : Nat
h : n + w✝ = m
⊢ x.leNat m = true
Tactic:
cases h
Proof state after:
case refl
n : Nat
x : ENat
hx : x.leNat n = true
w✝ : Nat
h : n ≤ n + w✝
⊢ x.leNat (n + w✝) = true
Theorem: ENat.mono
Proof state before:
case refl
n : Nat
x : ENat
hx : x.leNat n = true
w✝ : Nat
h : n ≤ n + w✝
⊢ x.leNat (n + w✝) = true
Tactic:
exact mono_add hx
Proof state after:
no goals
Theorem: ENat.mono'
Proof state before:
e : ENat
x y : Nat
⊢ x ≤ y → e.leNat y = false → e.leNat x = false
Tactic:
intro h hy
Proof state after:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y = false
⊢ e.leNat x = false
Theorem: ENat.mono'
Proof state before:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y = false
⊢ e.leNat x = false
Tactic:
rw [Bool.eq_false_iff] at hy ⊢
Proof state after:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y ≠ true
⊢ e.leNat x ≠ true
Theorem: ENat.mono'
Proof state before:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y ≠ true
⊢ e.leNat x ≠ true
Tactic:
exact mt (mono h) hy
Proof state after:
no goals
Theorem: ENat.leNat_coe_eq_true_iff_le
Proof state before:
m n : Nat
⊢ (ENat.ofNat n).leNat m = true ↔ n ≤ m
Tactic:
rw [ENat.ofNat, Nat.ble_eq]
Proof state after:
no goals
Theorem: ENat.leNat_coe_eq_false_iff_gt
Proof state before:
m n : Nat
⊢ (ENat.ofNat n).leNat m = false ↔ m < n
Tactic:
rw [Bool.eq_false_iff, ←Nat.not_le, ←leNat_coe_eq_true_iff_le]
Proof state after:
no goals
Theorem: ENat.leNat_zero_eq_true
Proof state before:
n : Nat
⊢ leNat 0 n = true
Tactic:
simp only [OfNat.ofNat, leNat_coe_eq_true_iff_le, Nat.zero_le]
Proof state after:
no goals
Theorem: Pos.toInd_ofInd
Proof state before:
n : Pos.asInd
⊢ (Pos.ofInd n).toInd = n
Tactic:
induction n with
| one => rfl
| succ n ih =>
  rw [ofInd_succ]
  rw [toInd_succ]
  rw [ih]
Proof state after:
no goals
Theorem: Pos.toInd_ofInd
Proof state before:
case one

⊢ (Pos.ofInd asInd.one).toInd = asInd.one
Tactic:
rfl
Proof state after:
no goals
Theorem: Pos.toInd_ofInd
Proof state before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n.succ).toInd = n.succ
Tactic:
rw [ofInd_succ]
Proof state after:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n + 1).toInd = n.succ
Theorem: Pos.toInd_ofInd
Proof state before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n + 1).toInd = n.succ
Tactic:
rw [toInd_succ]
Proof state after:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n).toInd.succ = n.succ
Theorem: Pos.toInd_ofInd
Proof state before:
case succ
n : Pos.asInd
ih : (Pos.ofInd n).toInd = n
⊢ (Pos.ofInd n).toInd.succ = n.succ
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Pos.ofInd_toInd
Proof state before:
n : Pos
⊢ Pos.ofInd n.toInd = n
Tactic:
induction n with
| one => rfl
| succ n ih =>
  rw [toInd_succ]
  rw [ofInd_succ]
  rw [ih]
Proof state after:
no goals
Theorem: Pos.ofInd_toInd
Proof state before:
case one

⊢ Pos.ofInd (Pos.toInd 1) = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Pos.ofInd_toInd
Proof state before:
case succ
n : Pos
ih : Pos.ofInd n.toInd = n
⊢ Pos.ofInd (n + 1).toInd = n + 1
Tactic:
rw [toInd_succ]
Proof state after:
case succ
n : Pos
ih : Pos.ofInd n.toInd = n
⊢ Pos.ofInd n.toInd.succ = n + 1
Theorem: Pos.ofInd_toInd
Proof state before:
case succ
n : Pos
ih : Pos.ofInd n.toInd = n
⊢ Pos.ofInd n.toInd.succ = n + 1
Tactic:
rw [ofInd_succ]
Proof state after:
case succ
n : Pos
ih : Pos.ofInd n.toInd = n
⊢ Pos.ofInd n.toInd + 1 = n + 1
Theorem: Pos.ofInd_toInd
Proof state before:
case succ
n : Pos
ih : Pos.ofInd n.toInd = n
⊢ Pos.ofInd n.toInd + 1 = n + 1
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
n : Pos.asBin
⊢ n.toNat ≠ 0
Tactic:
induction n with
| one => exact Nat.one_ne_zero
| bit0 n ih =>
  rw [←Nat.mul_zero 2, asBin.toNat_bit0]
  intro h
  absurd ih
  exact Nat.eq_of_mul_eq_mul_left (Nat.is_pos 2) h
| bit1 n _ => exact Nat.succ_ne_zero (2 * n.toNat)
Proof state after:
no goals
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case one

⊢ one.toNat ≠ 0
Tactic:
exact Nat.one_ne_zero
Proof state after:
no goals
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ n.bit0.toNat ≠ 0
Tactic:
rw [←Nat.mul_zero 2, asBin.toNat_bit0]
Proof state after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ 2 * n.toNat ≠ 2 * 0
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
⊢ 2 * n.toNat ≠ 2 * 0
Tactic:
intro h
Proof state after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ False
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ False
Tactic:
absurd ih
Proof state after:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ n.toNat = 0
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case bit0
n : Pos.asBin
ih : n.toNat ≠ 0
h : 2 * n.toNat = 2 * 0
⊢ n.toNat = 0
Tactic:
exact Nat.eq_of_mul_eq_mul_left (Nat.is_pos 2) h
Proof state after:
no goals
Theorem: Pos.asBin.toNat_ne_zero
Proof state before:
case bit1
n : Pos.asBin
a_ih✝ : n.toNat ≠ 0
⊢ n.bit1.toNat ≠ 0
Tactic:
exact Nat.succ_ne_zero (2 * n.toNat)
Proof state after:
no goals
Theorem: Pos.div2_eq
Proof state before:
n : Nat
⊢ 2 * (div2 (n + 2)).fst + ↑(div2 (n + 2)).snd = n + 2
Tactic:
simp only [div2]
Proof state after:
n : Nat
⊢ 2 * ((div2 n).fst + 1) + ↑(div2 n).snd = n + 2
Theorem: Pos.div2_eq
Proof state before:
n : Nat
⊢ 2 * ((div2 n).fst + 1) + ↑(div2 n).snd = n + 2
Tactic:
rw [Nat.mul_succ]
Proof state after:
n : Nat
⊢ 2 * (div2 n).fst + 2 + ↑(div2 n).snd = n + 2
Theorem: Pos.div2_eq
Proof state before:
n : Nat
⊢ 2 * (div2 n).fst + 2 + ↑(div2 n).snd = n + 2
Tactic:
rw [Nat.add_right_comm]
Proof state after:
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd + 2 = n + 2
Theorem: Pos.div2_eq
Proof state before:
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd + 2 = n + 2
Tactic:
congr
Proof state after:
case e_a
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd = n
Theorem: Pos.div2_eq
Proof state before:
case e_a
n : Nat
⊢ 2 * (div2 n).fst + ↑(div2 n).snd = n
Tactic:
exact div2_eq n
Proof state after:
no goals
Theorem: Nat.zero_pow_succ
Proof state before:
x : Nat
⊢ 0 ^ (x + 1) = 0 ^ x * 0
Tactic:
rw [Nat.pow_succ]
Proof state after:
no goals
Theorem: Nat.zero_pow_succ
Proof state before:
x : Nat
⊢ 0 ^ x * 0 = 0
Tactic:
rw [Nat.mul_zero]
Proof state after:
no goals
Theorem: Nat.zero_pow_of_nonzero
Proof state before:
x : Nat
⊢ x ≠ 0 → 0 ^ x = 0
Tactic:
cases x with
| zero => intro; contradiction
| succ x => intro; rw [Nat.zero_pow_succ]
Proof state after:
no goals
Theorem: Nat.zero_pow_of_nonzero
Proof state before:
case zero

⊢ 0 ≠ 0 → 0 ^ 0 = 0
Tactic:
intro
Proof state after:
case zero
a✝ : 0 ≠ 0
⊢ 0 ^ 0 = 0