case mp
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y

case mpr
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy : map f x = map f y
⊢ x = y
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
⊢ Injective (map f) ↔ Injective f
constructor <;> intro h x y hxy
case mp
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]
case mp
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y
suffices [x] = [y] by simpa using this
case mp.a
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]
case mp
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]
apply h
no goals
case mp.a
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]
simp [hxy]
no goals
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
this : [x] = [y]
⊢ x = y
simpa using this
case mpr.nil
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x✝ y : List α
hxy✝ : map f x✝ = map f y
x : List α
hxy : map f x = map f []
⊢ x = []

case mpr.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x✝ y : List α
hxy✝ : map f x✝ = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
x : List α
hxy : map f x = map f (yh :: yt)
⊢ x = yh :: yt
case mpr
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy : map f x = map f y
⊢ x = y
induction' y with yh yt y_ih generalizing x
case mpr.cons.nil
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
hxy : map f [] = map f (yh :: yt)
⊢ [] = yh :: yt

case mpr.cons.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
head✝ : α
tail✝ : List α
hxy : map f (head✝ :: tail✝) = map f (yh :: yt)
⊢ head✝ :: tail✝ = yh :: yt
case mpr.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x✝ y : List α
hxy✝ : map f x✝ = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
x : List α
hxy : map f x = map f (yh :: yt)
⊢ x = yh :: yt
cases x
no goals
case mpr.nil
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x✝ y : List α
hxy✝ : map f x✝ = map f y
x : List α
hxy : map f x = map f []
⊢ x = []
simpa using hxy
no goals
case mpr.cons.nil
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
hxy : map f [] = map f (yh :: yt)
⊢ [] = yh :: yt
simp at hxy
case mpr.cons.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
head✝ : α
tail✝ : List α
hxy : f head✝ = f yh ∧ map f tail✝ = map f yt
⊢ head✝ :: tail✝ = yh :: yt
case mpr.cons.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
head✝ : α
tail✝ : List α
hxy : map f (head✝ :: tail✝) = map f (yh :: yt)
⊢ head✝ :: tail✝ = yh :: yt
simp only [map, cons.injEq] at hxy
no goals
case mpr.cons.cons
ι : Type ?u.135734
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
h : Injective f
x y : List α
hxy✝ : map f x = map f y
yh : α
yt : List α
y_ih : ∀ ⦃x : List α⦄, map f x = map f yt → x = yt
head✝ : α
tail✝ : List α
hxy : f head✝ = f yh ∧ map f tail✝ = map f yt
⊢ head✝ :: tail✝ = yh :: yt
simp [y_ih hxy.2, h hxy.1]