α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) → Function.Injective f
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) ↔ Function.Injective f
refine' ⟨_, nodup_ofFn_ofInjective⟩
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0

case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
⊢ Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn f) → Function.Injective f
refine' Fin.consInduction _ (fun x₀ xs ih => _) f
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
a✝ : Nodup (ofFn Fin.elim0)
⊢ Function.Injective Fin.elim0
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
intro _
no goals
case refine'_1
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
a✝ : Nodup (ofFn Fin.elim0)
⊢ Function.Injective Fin.elim0
exact Function.injective_of_subsingleton _
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ Function.Injective (Fin.cons x₀ xs)
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
⊢ Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
intro h
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ Function.Injective (Fin.cons x₀ xs)
rw [Fin.cons_injective_iff]
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : (¬x₀ ∈ Set.range fun i => xs i) ∧ Nodup (ofFn fun i => xs i)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : Nodup (ofFn (Fin.cons x₀ xs))
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
no goals
case refine'_2
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : Nodup (ofFn xs) → Function.Injective xs
h : (¬x₀ ∈ Set.range fun i => xs i) ∧ Nodup (ofFn fun i => xs i)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
exact h.imp_right ih