case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
⊢ Injective (inducedMap A).snd
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res ((fun a => ↑a) { val := x, property := hx }) = res ((fun a => ↑a) { val := y, property := hy })
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
refine' Subtype.coe_injective (res_injective _)
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x = res y
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res ((fun a => ↑a) { val := x, property := hx }) = res ((fun a => ↑a) { val := y, property := hy })
dsimp
case mk.mk.h
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
⊢ res x n = res y n
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x = res y
ext n : 1
case mk.mk.h.zero
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x Nat.zero = res y Nat.zero

case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ res x (Nat.succ n) = res y (Nat.succ n)
case mk.mk.h
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
⊢ res x n = res y n
induction' n with n ih
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ res x (Nat.succ n) = res y (Nat.succ n)
simp only [res_succ, cons.injEq]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n
refine' ⟨_, ih⟩
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬CantorScheme.Disjoint A
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n
contrapose hA
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x x_1 x_2, ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬CantorScheme.Disjoint A
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne.def, not_forall, exists_prop]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬_root_.Disjoint (A (x n :: res x n)) (A (y n :: res x n))
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x x_1 x_2, ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
refine' ⟨res x n, _, _, hA, _⟩
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x_1, x_1 ∈ A (x n :: res x n) ∧ x_1 ∈ A (y n :: res x n)
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬_root_.Disjoint (A (x n :: res x n)) (A (y n :: res x n))
rw [not_disjoint_iff]
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (x n :: res x n)

case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (y n :: res x n)
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x_1, x_1 ∈ A (x n :: res x n) ∧ x_1 ∈ A (y n :: res x n)
refine' ⟨(inducedMap A).2 ⟨x, hx⟩, _, _⟩
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y (Nat.succ n))
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (y n :: res x n)
rw [hxy, ih, ← res_succ]
no goals
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y (Nat.succ n))
apply map_mem
no goals
case mk.mk.h.zero
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x Nat.zero = res y Nat.zero
simp
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x (Nat.succ n))
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (x n :: res x n)
rw [← res_succ]
no goals
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x (Nat.succ n))
apply map_mem