case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ ¬x₀ ∈ Set.range x

case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ ¬x₀ ∈ Set.range x ∧ Injective x
refine' ⟨fun h ↦ ⟨_, _⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
case refine'_1
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ ¬x₀ ∈ Set.range x
rintro ⟨i, hi⟩
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x (succ i) = cons x₀ x 0 → succ i = 0
⊢ False
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
i : Fin n
hi : x i = x₀
⊢ False
replace h := @h i.succ 0
no goals
case refine'_1.intro
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i✝ : Fin n
y : α✝ (succ i✝)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
i : Fin n
hi : x i = x₀
h : cons x₀ x (succ i) = cons x₀ x 0 → succ i = 0
⊢ False
simp [hi, succ_ne_zero] at h
no goals
case refine'_2
m n : ℕ
α✝ : Fin (n + 1) → Type u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (succ i)
i : Fin n
y : α✝ (succ i)
z : α✝ 0
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x
simpa [Function.comp] using h.comp (Fin.succ_injective _)