Theorem: Imo1987P4.imo1987_p4_generalized (Compfiles/Imo1987P4.lean)

State before:
m : ℕ
⊢ ¬∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
Tactic:
intro hf
State after:
m : ℕ
hf : ∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False

State before:
m : ℕ
hf : ∃ f, ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Tactic:
obtain ⟨f, hf⟩ := hf
State after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False

State before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
Tactic:
have f_injective : f.Injective := by
  intro n m hnm; have hfn := hf n; simp_all only [add_left_inj]
State after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
⊢ False

State before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
⊢ False
Tactic:
let NN : Set ℕ := Set.univ
State after:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
⊢ False

State before:
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
⊢ False
Tactic:
let A : Set ℕ := NN \ (f '' NN)
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
⊢ False

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
⊢ False
Tactic:
let B : Set ℕ := f '' A
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
⊢ False

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
⊢ False
Tactic:
have hid := Set.image_diff f_injective NN (f '' NN)
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 : f '' (NN \ f '' NN) = f '' NN \ f '' (f '' NN)
⊢ False

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 : f '' (NN \ f '' NN) = f '' NN \ f '' (f '' NN)
⊢ False
Tactic:
rw [show f '' (NN \ f '' NN) = B by rfl] at hid
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)
⊢ False

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)
⊢ False
Tactic:
have ab_disjoint : Disjoint A B := by
  intro _C hca hcb c hc
  exact Set.not_mem_of_mem_diff (hca hc) (Set.image_subset f sdiff_le (hcb hc))
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
⊢ False

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}
⊢ False
Tactic:
have ab_fintype : Fintype ↑(A ∪ B) := by rw [ab_range]; exact inferInstance
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)
⊢ False

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)
⊢ False
Tactic:
have h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1 := by
  have hc := @Fintype.card_congr' ↑(A ∪ B)
                {x | x < 2 * m + 1} _ _ (by rw [ab_range])
  simp only [hc, Fintype.card_ofFinset, Finset.card_range]
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
⊢ False

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

State before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ Function.Injective f
Tactic:
intro n m hnm
State after:
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
⊢ n = m

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
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

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]
State after:
no goals

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
State after:
no goals

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
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 ∈ ⊥

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))
State after:
no goals

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]
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)

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
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)

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
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)

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 *
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)

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
State after:
no goals

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
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)

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
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)

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
State after:
no goals

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
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

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]
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}

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
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}

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
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}

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]
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

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 < 2 * m + 1
Tactic:
by_contra! H
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
H : 2 * m + 1 ≤ x
⊢ False

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
H : 2 * m + 1 ≤ x
⊢ False
Tactic:
obtain ⟨z, hz⟩ : ∃ z, x = (2 * m + 1) + z := exists_add_of_le H
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
z : ℕ
hz : x = 2 * m + 1 + z
⊢ False

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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
z : ℕ
hz : x = 2 * m + 1 + z
⊢ False
Tactic:
rw [hz] at hx
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
⊢ False

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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
⊢ False
Tactic:
have hzz := hx z
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬f (f z) = 2 * m + 1 + z
⊢ False

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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬f (f z) = 2 * m + 1 + z
⊢ False
Tactic:
rw [hf z, add_comm] at hzz
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬2 * m + 1 + z = 2 * m + 1 + z
⊢ False

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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬2 * m + 1 + z = 2 * m + 1 + z
⊢ False
Tactic:
exact (hzz rfl).elim
State after:
no goals

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)
⊢ {n | n < 2 * m + 1} ⊆ A ∪ B
Tactic:
rw [ab_union]
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)
⊢ {n | n < 2 * m + 1} ⊆ NN \ f '' (f '' NN)

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)
⊢ {n | n < 2 * m + 1} ⊆ NN \ f '' (f '' NN)
Tactic:
intro x hx
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 ∈ {n | n < 2 * m + 1}
⊢ x ∈ NN \ f '' (f '' NN)

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 ∈ {n | n < 2 * m + 1}
⊢ x ∈ NN \ f '' (f '' NN)
Tactic:
unfold_let NN A at *
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
ab_union : Set.univ \ f '' Set.univ ∪ B = Set.univ \ f '' (f '' Set.univ)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)

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
ab_union : Set.univ \ f '' Set.univ ∪ B = Set.univ \ f '' (f '' Set.univ)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)
Tactic:
aesop
State after:
no goals

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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑(A ∪ B)
Tactic:
rw [ab_range]
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑{n | n < 2 * m + 1}

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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑{n | n < 2 * m + 1}
Tactic:
exact inferInstance
State after:
no goals

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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1
Tactic:
have hc := @Fintype.card_congr' ↑(A ∪ B)
              {x | x < 2 * m + 1} _ _ (by rw [ab_range])
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
hc : Fintype.card ↑(A ∪ B) = Fintype.card ↑{x | x < 2 * m + 1}
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1

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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
hc : Fintype.card ↑(A ∪ B) = Fintype.card ↑{x | x < 2 * m + 1}
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1
Tactic:
simp only [hc, Fintype.card_ofFinset, Finset.card_range]
State after:
no goals

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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ ↑(A ∪ B) = ↑{x | x < 2 * m + 1}
Tactic:
rw [ab_range]
State after:
no goals