-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_injective_of_injective {α} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x)
    (hx : Function.Injective x) : Function.Injective (cons x₀ x : Fin n.succ → α)

Proof state:
case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n), cons x₀ x 0 = cons x₀ x i.succ → 0 = i.succ

Tactic:
intro j h

Result:
case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
j : Fin n
h : cons x₀ x 0 = cons x₀ x j.succ
⊢ 0 = j.succ

Proof state:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
h : x i = x₀
⊢ i.succ = 0

Tactic:
exact hx₀.elim ⟨_, h⟩

Result:
no goals

Proof state:
case refine_1.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
a✝ : cons x₀ x 0 = cons x₀ x 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n) ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i.succ = cons x₀ x a₂ → i.succ = a₂

Tactic:
intro i

Result:
case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i.succ = cons x₀ x a₂ → i.succ = a₂

Proof state:
case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i j : Fin n
h : x i = x j
⊢ i.succ = j.succ

Tactic:
exact congr_arg _ (hx h)

Result:
no goals

Proof state:
case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i j : Fin n
h : cons x₀ x i.succ = cons x₀ x j.succ
⊢ i.succ = j.succ

Tactic:
rw [cons_succ, cons_succ] at h

Result:
case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i j : Fin n
h : x i = x j
⊢ i.succ = j.succ

Proof state:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ cons x₀ x i.succ = cons x₀ x 0 → i.succ = 0

Tactic:
intro h

Result:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
h : cons x₀ x i.succ = cons x₀ x 0
⊢ i.succ = 0

Proof state:
case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
j : Fin n
h : cons x₀ x 0 = cons x₀ x j.succ
⊢ 0 = j.succ

Tactic:
rw [cons_zero, cons_succ] at h

Result:
case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
j : Fin n
h : x₀ = x j
⊢ 0 = j.succ

Proof state:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
h : cons x₀ x i.succ = cons x₀ x 0
⊢ i.succ = 0

Tactic:
rw [cons_zero, cons_succ] at h

Result:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
h : x i = x₀
⊢ i.succ = 0

Proof state:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x 0 = cons x₀ x a₂ → 0 = a₂

Tactic:
refine Fin.cases ?_ ?_

Result:
case refine_1.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n), cons x₀ x 0 = cons x₀ x i.succ → 0 = i.succ

Proof state:
case refine_1.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

Tactic:
intro

Result:
case refine_1.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
a✝ : cons x₀ x 0 = cons x₀ x 0
⊢ 0 = 0

Proof state:
case refine_1.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
j : Fin n
h : x₀ = x j
⊢ 0 = j.succ

Tactic:
exact hx₀.elim ⟨_, h.symm⟩

Result:
no goals

Proof state:
case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i.succ = cons x₀ x a₂ → i.succ = a₂

Tactic:
refine Fin.cases ?_ ?_

Result:
case refine_2.refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ cons x₀ x i.succ = cons x₀ x 0 → i.succ = 0

case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ (i_1 : Fin n), cons x₀ x i.succ = cons x₀ x i_1.succ → i.succ = i_1.succ

Proof state:
case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i : Fin n
⊢ ∀ (i_1 : Fin n), cons x₀ x i.succ = cons x₀ x i_1.succ → i.succ = i_1.succ

Tactic:
intro j h

Result:
case refine_2.refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
i j : Fin n
h : cons x₀ x i.succ = cons x₀ x j.succ
⊢ i.succ = j.succ

Proof state:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)

Tactic:
refine Fin.cases ?_ ?_

Result:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x 0 = cons x₀ x a₂ → 0 = a₂

case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : x₀ ∉ Set.range x
hx : Injective x
⊢ ∀ (i : Fin n) ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i.succ = cons x₀ x a₂ → i.succ = a₂