internlm/Lean-Github huggingface dataset:
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ENat.ofNat n < x
Tactic:
absurd h
Proof state after:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ¬n + 1 ≤ n
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ¬n + 1 ≤ n
Tactic:
exact Nat.lt_irrefl n
Proof state after:
no goals
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ ENat.ofNat n < x
Tactic:
exists n
Proof state after:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Tactic:
rw [leNat_coe_eq_true_iff_le]
Proof state after:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ n ≤ n ∧ x.leNat n = false
Theorem: ENat.coe_lt_iff_coe_succ_le
Proof state before:
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ n ≤ n ∧ x.leNat n = false
Tactic:
exact ⟨Nat.le_refl n, h⟩
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case zero
x : ENat
⊢ x ≤ ENat.ofNat 0 → ∃ m, m ≤ 0 ∧ x = ENat.ofNat m
Tactic:
intro h
Proof state after:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ ∃ m, m ≤ 0 ∧ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ ∃ m, m ≤ 0 ∧ x = ENat.ofNat m
Tactic:
exists 0
Proof state after:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0 ∧ x = ENat.ofNat 0
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case zero
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0 ∧ x = ENat.ofNat 0
Tactic:
constructor
Proof state after:
case zero.left
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0

case zero.right
x : ENat
h : x ≤ ENat.ofNat 0
⊢ x = ENat.ofNat 0
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case zero.left
x : ENat
h : x ≤ ENat.ofNat 0
⊢ 0 ≤ 0
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case zero.right
x : ENat
h : x ≤ ENat.ofNat 0
⊢ x = ENat.ofNat 0
Tactic:
exact eq_zero_of_le_zero h
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
⊢ x ≤ ENat.ofNat (n + 1) → ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
intro h
Proof state after:
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x.leNat n = true
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
rw [leNat_eq_true_iff_le_coe] at hn
Proof state after:
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
exists m
Proof state after:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1 ∧ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
constructor
Proof state after:
case left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1

case right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ m ≤ n + 1
Tactic:
exact Nat.le_succ_of_le h
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h✝ : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
m : Nat
h : m ≤ n
hm : x = ENat.ofNat m
⊢ x = ENat.ofNat m
Tactic:
exact hm
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x.leNat n = false
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
rw [leNat_eq_false_iff_coe_lt] at hn
Proof state after:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
Tactic:
exists n+1
Proof state after:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1 ∧ x = ENat.ofNat (n + 1)
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1 ∧ x = ENat.ofNat (n + 1)
Tactic:
constructor
Proof state after:
case succ.false.left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1

case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ x = ENat.ofNat (n + 1)
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false.left
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ n + 1 ≤ n + 1
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ x = ENat.ofNat (n + 1)
Tactic:
apply le_antisymm h
Proof state after:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ENat.ofNat (n + 1) ≤ x
Theorem: ENat.eq_ofNat_of_le_ofNat
Proof state before:
case succ.false.right
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : ENat.ofNat n < x
⊢ ENat.ofNat (n + 1) ≤ x
Tactic:
exact coe_lt_iff_coe_succ_le.1 hn
Proof state after:
no goals
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
x : Nat
⊢ x < bfind p h → ¬p x = true
Tactic:
intro hlt h
Proof state after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < bfind p h✝
h : p x = true
⊢ False
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < bfind p h✝
h : p x = true
⊢ False
Tactic:
unfold bfind at hlt
Proof state after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ False
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ False
Tactic:
apply Nat.not_le.2 hlt
Proof state after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x
Tactic:
apply toNat_le_of_leNat
Proof state after:
case h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).leNat x = true
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
case h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).leNat x = true
Tactic:
apply first_leNat_of
Proof state after:
case h.h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ p x = true
Theorem: Nat.not_prop_of_lt_bfind
Proof state before:
case h.h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ p x = true
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.bfind_le_of_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
x : Nat
⊢ p x = true → bfind p h ≤ x
Tactic:
intro h
Proof state after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ bfind p h✝ ≤ x
Theorem: Nat.bfind_le_of_prop
Proof state before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ bfind p h✝ ≤ x
Tactic:
apply Nat.le_of_not_gt
Proof state after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ ¬bfind p h✝ > x
Theorem: Nat.bfind_le_of_prop
Proof state before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ ¬bfind p h✝ > x
Tactic:
intro (hlt:_ < _)
Proof state after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ False
Theorem: Nat.bfind_le_of_prop
Proof state before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ False
Tactic:
apply not_prop_of_lt_bfind hlt
Proof state after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ p x = true
Theorem: Nat.bfind_le_of_prop
Proof state before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ p x = true
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.bfind_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ p (bfind p h) = true
Tactic:
have : (first p).leNat (bfind p h) := by
  unfold bfind
  rw [leNat_toNat]
Proof state after:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
⊢ p (bfind p h) = true
Theorem: Nat.bfind_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat (bfind p h) = true
Tactic:
unfold bfind
Proof state after:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat ((first p).toNat ⋯) = true
Theorem: Nat.bfind_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat ((first p).toNat ⋯) = true
Tactic:
rw [leNat_toNat]
Proof state after:
no goals
Theorem: Nat.bfind_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
heq : x = bfind p h
⊢ p (bfind p h) = true
Tactic:
rw [←heq, hx]
Proof state after:
no goals
Theorem: Nat.bfind_prop
Proof state before:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x = bfind p h
Tactic:
antisymmetry using (.≤.:Nat→Nat→Prop)
Proof state after:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x ≤ bfind p h

case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ bfind p h ≤ x
Theorem: Nat.bfind_prop
Proof state before:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x ≤ bfind p h
Tactic:
exact hle
Proof state after:
no goals
Theorem: Nat.bfind_prop
Proof state before:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ bfind p h ≤ x
Tactic:
exact bfind_le_of_prop hx
Proof state after:
no goals
Theorem: Nat.find_property
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (find p h)
Tactic:
apply of_decide_eq_true
Proof state after:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ decide (p (find p h)) = true
Theorem: Nat.find_property
Proof state before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ decide (p (find p h)) = true
Tactic:
apply bfind_prop (λ n => decide (p n))
Proof state after:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ∃ n, decide (p n) = true
Theorem: Nat.find_property
Proof state before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ∃ n, decide (p n) = true
Tactic:
match h with | ⟨n, hn⟩ => exists n; exact decide_eq_true hn
Proof state after:
no goals
Theorem: Nat.find_property
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : Nat
hn : p n
⊢ ∃ n, decide (p n) = true
Tactic:
exists n
Proof state after:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : Nat
hn : p n
⊢ decide (p n) = true
Theorem: Nat.find_property
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : Nat
hn : p n
⊢ decide (p n) = true
Tactic:
exact decide_eq_true hn
Proof state after:
no goals
Theorem: Nat.find_minimal
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
⊢ p x → find p h ≤ x
Tactic:
intro hx
Proof state after:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ find p h ≤ x
Theorem: Nat.find_minimal
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ find p h ≤ x
Tactic:
apply bfind_le_of_prop
Proof state after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ ∃ n, decide (p n) = true

case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ decide (p x) = true
Theorem: Nat.find_minimal
Proof state before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ ∃ n, decide (p n) = true
Tactic:
match h with | ⟨n, hn⟩ => exists n; exact decide_eq_true hn
Proof state after:
no goals
Theorem: Nat.find_minimal
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ ∃ n, decide (p n) = true
Tactic:
exists n
Proof state after:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ decide (p n) = true
Theorem: Nat.find_minimal
Proof state before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ decide (p n) = true
Tactic:
exact decide_eq_true hn
Proof state after:
no goals
Theorem: Nat.find_minimal
Proof state before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ decide (p x) = true
Tactic:
exact decide_eq_true hx
Proof state after:
no goals
Theorem: Nat.find_ext
Proof state before:
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
⊢ p₁ = p₂
Tactic:
funext n
Proof state after:
case h
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n = p₂ n
Theorem: Nat.find_ext
Proof state before:
case h
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n = p₂ n
Tactic:
apply propext
Proof state after:
case h.a
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n ↔ p₂ n
Theorem: Nat.find_ext
Proof state before:
case h.a
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n ↔ p₂ n
Tactic:
exact h n
Proof state after:
no goals
Theorem: Bool.bne_eq_decide_ne
Proof state before:
x y z : Bool
⊢ x.bne y = decide (x ≠ y)
Tactic:
bool_tt x y
Proof state after:
no goals
Theorem: Bool.bge_eq_decide_ge
Proof state before:
x y z : Bool
⊢ x.bge y = decide (x ≥ y)
Tactic:
bool_tt x y
Proof state after:
no goals
Theorem: Bool.bgt_eq_decide_gt
Proof state before:
x y z : Bool
⊢ x.bgt y = decide (x > y)
Tactic:
bool_tt x y
Proof state after:
no goals
Theorem: Bool.ble_eq_decide_le
Proof state before:
x y z : Bool
⊢ x.ble y = decide (x ≤ y)
Tactic:
bool_tt x y
Proof state after:
no goals
Theorem: Bool.blt_eq_decide_lt
Proof state before:
x y z : Bool
⊢ x.blt y = decide (x < y)
Tactic:
bool_tt x y
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
a : α
⊢ iter f (m + n) a = iter f m (iter f n a)
Tactic:
induction n generalizing a with
| zero => rfl
| succ n ih =>
  calc
  _ = iter f (m + n + 1) a := rfl
  _ = iter f (m + n) (f a) := by rw [iter_succ]
  _ = iter f m (iter f n (f a)) := by rw [ih]
  _ = iter f m (iter f (n + 1) a) := by rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
case zero
α : Sort u_1
f : α → α
m : Nat
a : α
⊢ iter f (m + 0) a = iter f m (iter f 0 a)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
case succ
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m + n) a = iter f m (iter f n a)
a : α
⊢ iter f (m + (n + 1)) a = iter f m (iter f (n + 1) a)
Tactic:
calc
_ = iter f (m + n + 1) a := rfl
_ = iter f (m + n) (f a) := by rw [iter_succ]
_ = iter f m (iter f n (f a)) := by rw [ih]
_ = iter f m (iter f (n + 1) a) := by rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m + n) a = iter f m (iter f n a)
a : α
⊢ iter f (m + n + 1) a = iter f (m + n) (f a)
Tactic:
rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m + n) a = iter f m (iter f n a)
a : α
⊢ iter f (m + n) (f a) = iter f m (iter f n (f a))
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Nat.iter_add
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m + n) a = iter f m (iter f n a)
a : α
⊢ iter f m (iter f n (f a)) = iter f m (iter f (n + 1) a)
Tactic:
rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
a : α
⊢ iter f (m * n) a = iter (iter f m) n a
Tactic:
induction n generalizing a with
| zero => rfl
| succ n ih =>
  calc
  _ = iter f (m * n + m) a := rfl
  _ = iter f (m * n) (iter f m a) := by rw [iter_add]
  _ = iter (iter f m) n (iter f m a) := by rw [ih]
  _ = iter (iter f m) (n + 1) a := by rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
case zero
α : Sort u_1
f : α → α
m : Nat
a : α
⊢ iter f (m * 0) a = iter (iter f m) 0 a
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
case succ
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * (n + 1)) a = iter (iter f m) (n + 1) a
Tactic:
calc
_ = iter f (m * n + m) a := rfl
_ = iter f (m * n) (iter f m a) := by rw [iter_add]
_ = iter (iter f m) n (iter f m a) := by rw [ih]
_ = iter (iter f m) (n + 1) a := by rw [iter_succ]
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * n + m) a = iter f (m * n) (iter f m a)
Tactic:
rw [iter_add]
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter f (m * n) (iter f m a) = iter (iter f m) n (iter f m a)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Nat.iter_mul
Proof state before:
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m * n) a = iter (iter f m) n a
a : α
⊢ iter (iter f m) n (iter f m a) = iter (iter f m) (n + 1) a
Tactic:
rw [iter_succ]
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (compareOfLE x y).swap = compareOfLE y x
Tactic:
unfold compareOfLE
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
by_cases x ≤ y, y ≤ x with
| isTrue _, isTrue _ => split <;> rfl
| isTrue _, isFalse _ => split <;> rfl
| isFalse _, isTrue _ => split <;> rfl
| isFalse _, isFalse _ =>
  cases Total.total (r:=(.≤.)) x y with
  | inl hxy => absurd hxy; assumption
  | inr hyx => absurd hyx; assumption
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : x ≤ y
h✝ : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : x ≤ y
h✝ : ¬y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
cases Total.total (r:=(.≤.)) x y with
| inl hxy => absurd hxy; assumption
| inr hyx => absurd hyx; assumption
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
absurd hxy
Proof state after:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ ¬x ≤ y
Theorem: compareOfLE.symm
Proof state before:
case inl
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hxy : x ≤ y
⊢ ¬x ≤ y
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLE.symm
Proof state before:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
Tactic:
absurd hyx
Proof state after:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ ¬y ≤ x