internlm/Lean-Github huggingface dataset:
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ n = q
Tactic:
linarith
Proof state after:
no goals
Theorem: countably_infinite
Proof state before:
⊢ Set.Infinite A ∧ Set.Countable A
Tactic:
constructor
Proof state after:
case left

⊢ Set.Infinite A

case right

⊢ Set.Countable A
Theorem: countably_infinite
Proof state before:
case left

⊢ Set.Infinite A
Tactic:
let f (n : ℕ) : ℕ × ℕ := (n, n + 1)
Proof state after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Set.Infinite A
Theorem: countably_infinite
Proof state before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Set.Infinite A
Tactic:
have inj_f : Function.Injective f := by
  intros a b heq
  simp only [f] at heq
  simp only [Prod.mk.inj_iff] at heq
  exact heq.1
Proof state after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ Set.Infinite A
Theorem: countably_infinite
Proof state before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ Set.Infinite A
Tactic:
have hf : ∀ (x : ℕ), f x ∈ A := by
  intro x
  simp only [A, f]
  simp only [Set.mem_setOf_eq, le_add_iff_nonneg_right, zero_le]
Proof state after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
hf : ∀ (x : ℕ), f x ∈ A
⊢ Set.Infinite A
Theorem: countably_infinite
Proof state before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
hf : ∀ (x : ℕ), f x ∈ A
⊢ Set.Infinite A
Tactic:
exact Set.infinite_of_injective_forall_mem inj_f hf
Proof state after:
no goals
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Function.Injective f
Tactic:
intros a b heq
Proof state after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : f a = f b
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : f a = f b
⊢ a = b
Tactic:
simp only [f] at heq
Proof state after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : (a, a + 1) = (b, b + 1)
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : (a, a + 1) = (b, b + 1)
⊢ a = b
Tactic:
simp only [Prod.mk.inj_iff] at heq
Proof state after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : a = b ∧ a + 1 = b + 1
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : a = b ∧ a + 1 = b + 1
⊢ a = b
Tactic:
exact heq.1
Proof state after:
no goals
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ ∀ (x : ℕ), f x ∈ A
Tactic:
intro x
Proof state after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ f x ∈ A
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ f x ∈ A
Tactic:
simp only [A, f]
Proof state after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ (x, x + 1) ∈ {p | p.1 ≤ p.2}
Theorem: countably_infinite
Proof state before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ (x, x + 1) ∈ {p | p.1 ≤ p.2}
Tactic:
simp only [Set.mem_setOf_eq, le_add_iff_nonneg_right, zero_le]
Proof state after:
no goals
Theorem: countably_infinite
Proof state before:
case right

⊢ Set.Countable A
Tactic:
rw [Set.countable_iff_exists_injective]
Proof state after:
case right

⊢ ∃ f, Function.Injective f
Theorem: countably_infinite
Proof state before:
case right

⊢ ∃ f, Function.Injective f
Tactic:
let f (n : A) : ℕ  := 2^n.val.1 * 3^n.val.2
Proof state after:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ ∃ f, Function.Injective f
Theorem: countably_infinite
Proof state before:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ ∃ f, Function.Injective f
Tactic:
have inj_f : Function.Injective f := by
  intros a b heq
  simp only [f] at heq
  have unique_fac := two_pow_three_pow_unique_factorization heq
  rw [←Prod.eq_iff_fst_eq_snd_eq] at unique_fac
  exact SetCoe.ext unique_fac
Proof state after:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
inj_f : Function.Injective f
⊢ ∃ f, Function.Injective f
Theorem: countably_infinite
Proof state before:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
inj_f : Function.Injective f
⊢ ∃ f, Function.Injective f
Tactic:
use f
Proof state after:
no goals
Theorem: countably_infinite
Proof state before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ Function.Injective f
Tactic:
intros a b heq
Proof state after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : f a = f b
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : f a = f b
⊢ a = b
Tactic:
simp only [f] at heq
Proof state after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
⊢ a = b
Tactic:
have unique_fac := two_pow_three_pow_unique_factorization heq
Proof state after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : (↑a).1 = (↑b).1 ∧ (↑a).2 = (↑b).2
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : (↑a).1 = (↑b).1 ∧ (↑a).2 = (↑b).2
⊢ a = b
Tactic:
rw [←Prod.eq_iff_fst_eq_snd_eq] at unique_fac
Proof state after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : ↑a = ↑b
⊢ a = b
Theorem: countably_infinite
Proof state before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : ↑a = ↑b
⊢ a = b
Tactic:
exact SetCoe.ext unique_fac
Proof state after:
no goals
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
⊢ f^[n] x = x → n = 0
Tactic:
intro eq
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
simp_rw [Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt] at hper
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : {x | ∃ n > 0, f^[n] x = x} = ∅
eq : f^[n] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : {x | ∃ n > 0, f^[n] x = x} = ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
rw [Set.ext_iff] at hper
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : ∀ (x : α), x ∈ {x | ∃ n > 0, f^[n] x = x} ↔ x ∈ ∅
eq : f^[n] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : ∀ (x : α), x ∈ {x | ∃ n > 0, f^[n] x = x} ↔ x ∈ ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
simp at hper
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x : α) (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x : α) (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Tactic:
specialize hper x
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Tactic:
specialize hper n
Proof state after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
⊢ n = 0
Tactic:
by_cases h : 0 < n
Proof state after:
case pos
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : 0 < n
⊢ n = 0

case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
case pos
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : 0 < n
⊢ n = 0
Tactic:
exact absurd eq (hper h)
Proof state after:
no goals
Theorem: iterate_monotone_eq_zero
Proof state before:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0
Tactic:
simp only [not_lt, nonpos_iff_eq_zero] at h
Proof state after:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : n = 0
⊢ n = 0
Theorem: iterate_monotone_eq_zero
Proof state before:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : n = 0
⊢ n = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: aperiodic_next
Proof state before:
⊢ Function.periodicPts next = ∅
Tactic:
simp_rw [Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt]
Proof state after:
⊢ {x | ∃ n > 0, next^[n] x = x} = ∅
Theorem: aperiodic_next
Proof state before:
⊢ {x | ∃ n > 0, next^[n] x = x} = ∅
Tactic:
ext x
Proof state after:
case h
x : ℕ × ℕ
⊢ x ∈ {x | ∃ n > 0, next^[n] x = x} ↔ x ∈ ∅
Theorem: aperiodic_next
Proof state before:
case h
x : ℕ × ℕ
⊢ x ∈ {x | ∃ n > 0, next^[n] x = x} ↔ x ∈ ∅
Tactic:
simp only [gt_iff_lt, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_exists, not_and]
Proof state after:
case h
x : ℕ × ℕ
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬next^[x_1] x = x
Theorem: aperiodic_next
Proof state before:
case h
x : ℕ × ℕ
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬next^[x_1] x = x
Tactic:
intro n hlt heq
Proof state after:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : next^[n] x = x
⊢ False
Theorem: aperiodic_next
Proof state before:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : next^[n] x = x
⊢ False
Tactic:
simp_rw [next_apply] at heq
Proof state after:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x
⊢ False
Theorem: aperiodic_next
Proof state before:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x
⊢ False
Tactic:
induction' n with n ih
Proof state after:
case h.zero
x : ℕ × ℕ
hlt : 0 < Nat.zero
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.zero] x = x
⊢ False

case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
hlt : 0 < Nat.succ n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.succ n] x = x
⊢ False
Theorem: aperiodic_next
Proof state before:
case h.zero
x : ℕ × ℕ
hlt : 0 < Nat.zero
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.zero] x = x
⊢ False
Tactic:
simp only [Nat.zero_eq, lt_self_iff_false] at hlt
Proof state after:
no goals
Theorem: aperiodic_next
Proof state before:
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
hlt : 0 < Nat.succ n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.succ n] x = x
⊢ False
Tactic:
simp at *
Proof state after:
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
heq :
  (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n]
      (if x.1 = x.2 then (0, x.2 + 1) else (x.1 + 1, x.2)) =
    x
hlt : True
⊢ False
Theorem: enumerator_bijective
Proof state before:
⊢ Function.Bijective enumerator
Tactic:
simp_rw [Function.Bijective, enumerator_apply]
Proof state after:
⊢ (Function.Injective fun n => next^[n] (0, 0)) ∧ Function.Surjective fun n => next^[n] (0, 0)
Theorem: enumerator_bijective
Proof state before:
⊢ (Function.Injective fun n => next^[n] (0, 0)) ∧ Function.Surjective fun n => next^[n] (0, 0)
Tactic:
constructor
Proof state after:
case left

⊢ Function.Injective fun n => next^[n] (0, 0)

case right

⊢ Function.Surjective fun n => next^[n] (0, 0)
Theorem: enumerator_bijective
Proof state before:
case left

⊢ Function.Injective fun n => next^[n] (0, 0)
Tactic:
intros a b heq
Proof state after:
case left
a b : ℕ
heq : (fun n => next^[n] (0, 0)) a = (fun n => next^[n] (0, 0)) b
⊢ a = b
Theorem: enumerator_bijective
Proof state before:
case left
a b : ℕ
heq : (fun n => next^[n] (0, 0)) a = (fun n => next^[n] (0, 0)) b
⊢ a = b
Tactic:
simp only at heq
Proof state after:
case left
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a = b
Theorem: enumerator_bijective
Proof state before:
case left
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a = b
Tactic:
rw [Function.iterate_eq_iterate_iff_of_lt_minimalPeriod] at heq
Proof state after:
case left
a b : ℕ
heq : a = b
⊢ a = b

case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < Function.minimalPeriod next (0, 0)

case left.hn
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ b < Function.minimalPeriod next (0, 0)
Theorem: enumerator_bijective
Proof state before:
case left
a b : ℕ
heq : a = b
⊢ a = b
Tactic:
exact heq
Proof state after:
no goals
Theorem: enumerator_bijective
Proof state before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < Function.minimalPeriod next (0, 0)
Tactic:
rw [Function.minimalPeriod]
Proof state after:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < if h : (0, 0) ∈ Function.periodicPts next then Nat.find h else 0
Theorem: enumerator_bijective
Proof state before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < if h : (0, 0) ∈ Function.periodicPts next then Nat.find h else 0
Tactic:
simp
Proof state after:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a <
    if h : (0, 0) ∈ Function.periodicPts next then
      Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
    else 0
Theorem: enumerator_bijective
Proof state before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a <
    if h : (0, 0) ∈ Function.periodicPts next then
      Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
    else 0
Tactic:
split
Proof state after:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ a < Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)

case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
⊢ a < 0
Theorem: enumerator_bijective
Proof state before:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ a < Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
Tactic:
rw [Nat.lt_find_iff sorry a]
Proof state after:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ ∀ m ≤ a, ¬(0 < m ∧ Function.IsPeriodicPt next m (0, 0))
Theorem: enumerator_bijective
Proof state before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
⊢ a < 0
Tactic:
have foo := Function.iterate_cancel sorry heq
Proof state after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : next^[a - b] (0, 0) = (0, 0)
⊢ a < 0
Theorem: enumerator_bijective
Proof state before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : next^[a - b] (0, 0) = (0, 0)
⊢ a < 0
Tactic:
rw [←Function.IsFixedPt] at foo
Proof state after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsFixedPt next^[a - b] (0, 0)
⊢ a < 0
Theorem: enumerator_bijective
Proof state before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsFixedPt next^[a - b] (0, 0)
⊢ a < 0
Tactic:
rw [←Function.IsPeriodicPt] at foo
Proof state after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsPeriodicPt next (a - b) (0, 0)
⊢ a < 0
Theorem: distrib
Proof state before:
r p q R : Prop
⊢ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
Tactic:
tauto
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
p q r : Prop
⊢ ¬(p ∧ q) ↔ ¬p ∨ ¬q
Tactic:
constructor
Proof state after:
case mp
p q r : Prop
⊢ ¬(p ∧ q) → ¬p ∨ ¬q

case mpr
p q r : Prop
⊢ ¬p ∨ ¬q → ¬(p ∧ q)
Theorem: not_and_iff_or_not
Proof state before:
case mp
p q r : Prop
⊢ ¬(p ∧ q) → ¬p ∨ ¬q

case mpr
p q r : Prop
⊢ ¬p ∨ ¬q → ¬(p ∧ q)
Tactic:
{ intro hnand
  by_cases p 
  { exact Or.inr λ hq => hnand ⟨h, hq⟩}
  { left
    exact h
  }
}
Proof state after:
case mpr
p q r : Prop
⊢ ¬p ∨ ¬q → ¬(p ∧ q)
Theorem: not_and_iff_or_not
Proof state before:
case mpr
p q r : Prop
⊢ ¬p ∨ ¬q → ¬(p ∧ q)
Tactic:
{ 
  intros hnor hand
  rcases hand with ⟨hp, hq⟩  
  cases hnor with
    | inl hnp => exact hnp hp
    | inr hnq => exact hnq hq
}
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case mp
p q r : Prop
⊢ ¬(p ∧ q) → ¬p ∨ ¬q
Tactic:
intro hnand
Proof state after:
case mp
p q r : Prop
hnand : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Theorem: not_and_iff_or_not
Proof state before:
case mp
p q r : Prop
hnand : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Tactic:
by_cases p
Proof state after:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q

case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Theorem: not_and_iff_or_not
Proof state before:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q

case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
{ exact Or.inr λ hq => hnand ⟨h, hq⟩}
Proof state after:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Theorem: not_and_iff_or_not
Proof state before:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
{ left
  exact h
}
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q
Tactic:
exact Or.inr λ hq => hnand ⟨h, hq⟩
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
left
Proof state after:
case neg.h
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p
Theorem: not_and_iff_or_not
Proof state before:
case neg.h
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p
Tactic:
exact h
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case mpr
p q r : Prop
⊢ ¬p ∨ ¬q → ¬(p ∧ q)
Tactic:
intros hnor hand
Proof state after:
case mpr
p q r : Prop
hnor : ¬p ∨ ¬q
hand : p ∧ q
⊢ False
Theorem: not_and_iff_or_not
Proof state before:
case mpr
p q r : Prop
hnor : ¬p ∨ ¬q
hand : p ∧ q
⊢ False
Tactic:
rcases hand with ⟨hp, hq⟩
Proof state after:
case mpr.intro
p q r : Prop
hnor : ¬p ∨ ¬q
hp : p
hq : q
⊢ False
Theorem: not_and_iff_or_not
Proof state before:
case mpr.intro
p q r : Prop
hnor : ¬p ∨ ¬q
hp : p
hq : q
⊢ False
Tactic:
cases hnor with
  | inl hnp => exact hnp hp
  | inr hnq => exact hnq hq
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case mpr.intro.inl
p q r : Prop
hp : p
hq : q
hnp : ¬p
⊢ False
Tactic:
exact hnp hp
Proof state after:
no goals
Theorem: not_and_iff_or_not
Proof state before:
case mpr.intro.inr
p q r : Prop
hp : p
hq : q
hnq : ¬q
⊢ False
Tactic:
exact hnq hq
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
p q r : Prop
⊢ ¬(p ∨ q) ↔ ¬p ∧ ¬q
Tactic:
constructor
Proof state after:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Theorem: not_or_iff_and_not
Proof state before:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
{ intro hnor
  constructor
  { intro hp
    exact hnor (Or.inl hp)
  }
  { intro hq
    exact hnor (Or.inr hq)
  }
}
Proof state after:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Theorem: not_or_iff_and_not
Proof state before:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
{ 
  intros hnand hor
  rcases hnand with ⟨hnp, hnq⟩  
  cases hor with
    | inl hp => exact hnp hp
    | inr hq => exact hnq hq
}
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
intro hnor
Proof state after:
case mp
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Theorem: not_or_iff_and_not
Proof state before:
case mp
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Tactic:
constructor
Proof state after:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p

case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Theorem: not_or_iff_and_not
Proof state before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p

case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
{ intro hp
  exact hnor (Or.inl hp)
}
Proof state after:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Theorem: not_or_iff_and_not
Proof state before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
{ intro hq
  exact hnor (Or.inr hq)
}
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p
Tactic:
intro hp
Proof state after:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
hp : p
⊢ False
Theorem: not_or_iff_and_not
Proof state before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
hp : p
⊢ False
Tactic:
exact hnor (Or.inl hp)
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
intro hq
Proof state after:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
hq : q
⊢ False
Theorem: not_or_iff_and_not
Proof state before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
hq : q
⊢ False
Tactic:
exact hnor (Or.inr hq)
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
intros hnand hor
Proof state after:
case mpr
p q r : Prop
hnand : ¬p ∧ ¬q
hor : p ∨ q
⊢ False
Theorem: not_or_iff_and_not
Proof state before:
case mpr
p q r : Prop
hnand : ¬p ∧ ¬q
hor : p ∨ q
⊢ False
Tactic:
rcases hnand with ⟨hnp, hnq⟩
Proof state after:
case mpr.intro
p q r : Prop
hor : p ∨ q
hnp : ¬p
hnq : ¬q
⊢ False
Theorem: not_or_iff_and_not
Proof state before:
case mpr.intro
p q r : Prop
hor : p ∨ q
hnp : ¬p
hnq : ¬q
⊢ False
Tactic:
cases hor with
  | inl hp => exact hnp hp
  | inr hq => exact hnq hq
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mpr.intro.inl
p q r : Prop
hnp : ¬p
hnq : ¬q
hp : p
⊢ False
Tactic:
exact hnp hp
Proof state after:
no goals
Theorem: not_or_iff_and_not
Proof state before:
case mpr.intro.inr
p q r : Prop
hnp : ¬p
hnq : ¬q
hq : q
⊢ False
Tactic:
exact hnq hq
Proof state after:
no goals
Theorem: MotivatedTree.funext_ord
Proof state before:
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
⊢ f ≤ g
Tactic:
exact h
Proof state after:
no goals
Theorem: Cantor
Proof state before:
⊢ ∀ (X : Type u) (f : X → Set X), ¬Function.Surjective f
Tactic:
motivated_proof
  tree_rewrite_def [1, 1, 1, 2]
  tree_push_neg [1, 1]
  lib_rewrite [1, 1, 1, 2, 0, 1] Set.ext_iff [1, 1, 1, 1, 1, 2]
  tree_push_neg [1, 1, 1, 1]
  lib_rewrite [1, 1, 2, 0, 1] not_iff [1, 1, 1, 1, 1]
  unify_forall_exists [1, 1, 1]
  lib_apply refl [1, 1, 1, 1, 2]
Proof state after:
no goals
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬Function.Surjective f
Tactic:
tree_rewrite_def [1, 1, 1, 2]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬∀ b⋆ : Set X, ∃ a : X⠀
    f a = b⋆
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X⠀
  ¬∀ b⋆ : Set X, ∃ a : X⠀
    f a = b⋆
Tactic:
tree_push_neg [1, 1]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬f x_1 = x•