α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
⊢ ↑(map d) x₁ = ↑(map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
refine' ⟨fun h => _, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
have : x₁ 0 = x₂ 0 := by
  rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ∑ x : Fin n, x₁ (Fin.succ x) * d ^ ↑x = ∑ x : Fin n, x₂ (Fin.succ x) * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h
no goals
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ∑ x : Fin n, x₁ (Fin.succ x) * d ^ ↑x = ∑ x : Fin n, x₂ (Fin.succ x) * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩
no goals
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
⊢ ↑(map d) x₁ = ↑(map d) x₂
rw [map_succ', map_succ', h.1, h.2]
no goals
α : Type ?u.248271
β : Type ?u.248274
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ 0 = x₂ 0
rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]