case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
d : Nodup (map f [])
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → f x = f y → x = y

case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : Nodup (map f (hd :: tl))
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d : Nodup (map f l)
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y
induction' l with hd tl ih
no goals
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
d : Nodup (map f [])
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → f x = f y → x = y
simp
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : Nodup (map f (hd :: tl))
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.def] at d
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y
simp only [mem_cons]
case cons.inl.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f y✝ = f y✝
⊢ y✝ = y✝

case cons.inl.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ Nodup (map f tl)
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

case cons.inr.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

case cons.inr.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
⊢ ∀ ⦃x : α⦄, x = hd ∨ x ∈ tl → ∀ ⦃y : α⦄, y = hd ∨ y ∈ tl → f x = f y → x = y
rintro _ (rfl | h₁) _ (rfl | h₂) h₃
no goals
case cons.inl.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f y✝ = f y✝
⊢ y✝ = y✝
rfl
no goals
case cons.inl.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ Nodup (map f tl)
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
apply (d.1 _ h₂ h₃.symm).elim
no goals
case cons.inr.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ Nodup (map f tl)
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
apply (d.1 _ h₁ h₃).elim
no goals
case cons.inr.inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
f : α → β
l : List α
d✝ : Nodup (map f l)
hd : α
tl : List α
ih : Nodup (map f tl) → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ Nodup (map f tl)
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
apply ih d.2 h₁ h₂ h₃