-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_injOn : {x : Fin n → ℕ | ∀ i, x i < d}.InjOn (map d)

Proof state:
n d : ℕ
x₁ : Fin n → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin n), x i < d}
x₂ : Fin n → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin n), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Tactic:
induction n with
| zero => simp [eq_iff_true_of_subsingleton]
| succ n ih =>
  ext i
  have x := (map_eq_iff hx₁ hx₂).1 h
  exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

Result:
no goals

Proof state:
case zero
n d : ℕ
x₁ : Fin 0 → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin 0), x i < d}
x₂ : Fin 0 → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin 0), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
n d : ℕ
⊢ Set.InjOn ⇑(map d) {x | ∀ (i : Fin n), x i < d}

Tactic:
intro x₁ hx₁ x₂ hx₂ h

Result:
n d : ℕ
x₁ : Fin n → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin n), x i < d}
x₂ : Fin n → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin n), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Proof state:
case succ
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Tactic:
ext i

Result:
case succ.h
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
⊢ x₁ i = x₂ i

Proof state:
case succ.h
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
⊢ x₁ i = x₂ i

Tactic:
exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

Result:
no goals

Proof state:
case succ.h
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
⊢ x₁ i = x₂ i

Tactic:
have x := (map_eq_iff hx₁ hx₂).1 h

Result:
case succ.h
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
⊢ x₁ i = x₂ i