internlm/Lean-Github huggingface dataset:
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
⊢ False
Tactic:
have a_fintype := subset_fintype Set.subset_union_left ab_fintype
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
⊢ False
Tactic:
have b_fintype := subset_fintype Set.subset_union_right ab_fintype
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
⊢ False
Tactic:
have h3 := @Set.toFinset_union ℕ A B _ a_fintype b_fintype ab_fintype
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Tactic:
rw [← @Set.toFinset_card _ (A ∪ B) ab_fintype] at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : (A ∪ B).toFinset.card = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : (A ∪ B).toFinset.card = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Tactic:
rw [h3] at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
Tactic:
clear h3
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
⊢ False
Tactic:
have ab_disjoint' :=
  (@Set.disjoint_toFinset _ _ _ a_fintype b_fintype).mpr ab_disjoint
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : (A.toFinset ∪ B.toFinset).card = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Tactic:
rw [Finset.card_union_of_disjoint ab_disjoint'] at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : A.toFinset.card + B.toFinset.card = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : A.toFinset.card + B.toFinset.card = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Tactic:
rw [Set.toFinset_card, Set.toFinset_card] at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : Fintype.card ↑A + Fintype.card ↑B = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : Fintype.card ↑A + Fintype.card ↑B = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Tactic:
rw [Set.card_image_of_injective A f_injective] at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : Fintype.card ↑A + Fintype.card ↑A = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h2 : Fintype.card ↑A + Fintype.card ↑A = 2 * m + 1
ab_disjoint' : Disjoint A.toFinset B.toFinset
⊢ False
Tactic:
ring_nf at h2
Proof state after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
ab_disjoint' : Disjoint A.toFinset B.toFinset
h2 : Fintype.card ↑A * 2 = 1 + m * 2
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
ab_disjoint' : Disjoint A.toFinset B.toFinset
h2 : Fintype.card ↑A * 2 % 2 = (1 + m * 2) % 2
⊢ False
Tactic:
norm_num at h2
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ Function.Injective f
Tactic:
intro n m hnm
Proof state after:
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
⊢ n = m
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
⊢ n = m
Tactic:
have hfn := hf n
Proof state after:
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
hfn : f (f n) = n + (2 * m✝ + 1)
⊢ n = m
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
hfn : f (f n) = n + (2 * m✝ + 1)
⊢ n = m
Tactic:
simp_all only [add_left_inj]
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : f '' (NN \ f '' NN) = f '' NN \ f '' (f '' NN)
⊢ f '' (NN \ f '' NN) = B
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
⊢ Disjoint A B
Tactic:
intro _C hca hcb c hc
Proof state after:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
_C : Set ℕ
hca : _C ≤ A
hcb : _C ≤ B
c : ℕ
hc : c ∈ _C
⊢ c ∈ ⊥
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
_C : Set ℕ
hca : _C ≤ A
hcb : _C ≤ B
c : ℕ
hc : c ∈ _C
⊢ c ∈ ⊥
Tactic:
exact Set.not_mem_of_mem_diff (hca hc) (Set.image_subset f sdiff_le (hcb hc))
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ A ∪ B = NN \ f '' (f '' NN)
Tactic:
rw [hid]
Proof state after:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ A ∪ f '' NN \ f '' (f '' NN) = NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ A ∪ f '' NN \ f '' (f '' NN) = NN \ f '' (f '' NN)
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ A ∪ f '' NN \ f '' (f '' NN) ⊆ NN \ f '' (f '' NN)

case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ NN \ f '' (f '' NN) ⊆ A ∪ f '' NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ A ∪ f '' NN \ f '' (f '' NN) ⊆ NN \ f '' (f '' NN)
Tactic:
intro x hx
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
hx : x ∈ A ∪ f '' NN \ f '' (f '' NN)
⊢ x ∈ NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
hx : x ∈ A ∪ f '' NN \ f '' (f '' NN)
⊢ x ∈ NN \ f '' (f '' NN)
Tactic:
unfold_let NN A at *
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' Set.univ \ f '' (f '' Set.univ)
ab_disjoint : Disjoint (Set.univ \ f '' Set.univ) B
x : ℕ
hx : x ∈ Set.univ \ f '' Set.univ ∪ f '' Set.univ \ f '' (f '' Set.univ)
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' Set.univ \ f '' (f '' Set.univ)
ab_disjoint : Disjoint (Set.univ \ f '' Set.univ) B
x : ℕ
hx : x ∈ Set.univ \ f '' Set.univ ∪ f '' Set.univ \ f '' (f '' Set.univ)
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)
Tactic:
cases hx <;> aesop
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
⊢ NN \ f '' (f '' NN) ⊆ A ∪ f '' NN \ f '' (f '' NN)
Tactic:
intro x hx
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
hx : x ∈ NN \ f '' (f '' NN)
⊢ x ∈ A ∪ f '' NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
hx : x ∈ NN \ f '' (f '' NN)
⊢ x ∈ A ∪ f '' NN \ f '' (f '' NN)
Tactic:
obtain ⟨_hx, hx'⟩ := hx
Proof state after:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
_hx : x ∈ NN
hx' : x ∉ f '' (f '' NN)
⊢ x ∈ A ∪ f '' NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
_hx : x ∈ NN
hx' : x ∉ f '' (f '' NN)
⊢ x ∈ A ∪ f '' NN \ f '' (f '' NN)
Tactic:
by_cases (x ∈ A) <;> unfold_let NN A at * <;> aesop
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ A ∪ B = {n | n < 2 * m + 1}
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ A ∪ B ⊆ {n | n < 2 * m + 1}

case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ {n | n < 2 * m + 1} ⊆ A ∪ B
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ A ∪ B ⊆ {n | n < 2 * m + 1}
Tactic:
rw [ab_union]
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ NN \ f '' (f '' NN) ⊆ {n | n < 2 * m + 1}
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ NN \ f '' (f '' NN) ⊆ {n | n < 2 * m + 1}
Tactic:
rintro x hx
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : x ∈ NN \ f '' (f '' NN)
⊢ x ∈ {n | n < 2 * m + 1}
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : x ∈ NN \ f '' (f '' NN)
⊢ x ∈ {n | n < 2 * m + 1}
Tactic:
simp only [Set.image_univ, Set.mem_diff, Set.mem_univ, Set.mem_image,
           Set.mem_range, exists_exists_eq_and, not_exists,
           true_and, NN] at hx
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
⊢ x ∈ {n | n < 2 * m + 1}
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
⊢ x ∈ {n | n < 2 * m + 1}
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
⊢ x < 2 * m + 1