-- Mathlib/Topology/MetricSpace/CantorScheme.lean
theorem Disjoint.map_injective (hA : CantorScheme.Disjoint A) : Injective (inducedMap A).2

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
⊢ res x (n + 1) = res y (n + 1)

Tactic:
simp only [res_succ, cons.injEq]

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨y, hy⟩ ∈ A (res y n.succ)

Tactic:
apply map_mem

Result:
no goals

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, hx⟩ ∈ A (x n :: res x n)

Tactic:
rw [← res_succ]

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, hx⟩ ∈ A (res x n.succ)

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ res ((fun a => ↑a) ⟨x, hx⟩) = res ((fun a => ↑a) ⟨y, hy⟩)

Tactic:
dsimp

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ res x = res y

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, hx⟩ ∈ A (res x n.succ)

Tactic:
apply map_mem

Result:
no goals

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ res x = res y

Tactic:
ext n : 1

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
⊢ res x n = res y n

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬CantorScheme.Disjoint A

Tactic:
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, 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))

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
⊢ Injective (inducedMap A).snd

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
refine Subtype.coe_injective (res_injective ?_)

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
⊢ res ((fun a => ↑a) ⟨x, hx⟩) = res ((fun a => ↑a) ⟨y, hy⟩)

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, hx⟩ ∈ A (y n :: res x n)

Tactic:
rw [hxy, ih, ← res_succ]

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨y, hy⟩ ∈ A (res y n.succ)

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x_1 ∈ A (x n :: res x n), x_1 ∈ A (y n :: res x n)

Tactic:
refine ⟨(inducedMap A).2 ⟨x, hx⟩, ?_, ?_⟩

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, 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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ (inducedMap A).snd ⟨x, hx⟩ ∈ A (y n :: res x n)

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n

Tactic:
refine ⟨?_, ih⟩

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩
n : ℕ
ih : res x n = res y n
⊢ x n = y n

Proof state:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, 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))

Tactic:
refine ⟨res x n, _, _, hA, ?_⟩

Result:
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 : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, 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))