[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)
[PROOFSTEP]
intro b₁ b₂ h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
[PROOFSTEP]
simpa only [true_and, Prod.mk.inj_iff, eq_self_iff_true] using h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
β : Type u_6
b : β
⊢ Function.Injective fun a => (a, b)
[PROOFSTEP]
intro b₁ b₂ h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a => (a, b)) b₁ = (fun a => (a, b)) b₂
⊢ b₁ = b₂
[PROOFSTEP]
simpa only [and_true, eq_self_iff_true, mk.inj_iff] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p q : α × β
⊢ p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
[PROOFSTEP]
rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p₁ : α
p₂ : β
q₁ : α
q₂ : β
⊢ (p₁, p₂) = (q₁, q₂) ↔ (p₁, p₂).fst = (q₁, q₂).fst ∧ (p₁, p₂).snd = (q₁, q₂).snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b : β
x : α
⊢ (a, b).fst = x ↔ (a, b) = (x, (a, b).snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : α
b x : β
⊢ (a, b).snd = x ↔ (a, b) = ((a, b).fst, x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
p q : α × β
h : Prod.Lex r s p q
⊢ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
[PROOFSTEP]
cases h
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
h✝ : r a₁✝ a₂✝
⊢ r (a₁✝, b₁✝).fst (a₂✝, b₂✝).fst ∨ (a₁✝, b₁✝).fst = (a₂✝, b₂✝).fst ∧ s (a₁✝, b₁✝).snd (a₂✝, b₂✝).snd
[PROOFSTEP]
simp [*]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
a✝ : α
b₁✝ b₂✝ : β
h✝ : s b₁✝ b₂✝
⊢ r (a✝, b₁✝).fst (a✝, b₂✝).fst ∨ (a✝, b₁✝).fst = (a✝, b₂✝).fst ∧ s (a✝, b₁✝).snd (a✝, b₂✝).snd
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b : β
c : α
d : β
e : (a, b).fst = (c, d).fst
h : s (a, b).snd (c, d).snd
⊢ Prod.Lex r s (a, b) (c, d)
[PROOFSTEP]
subst e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b d : β
h : s (a, b).snd ((a, b).fst, d).snd
⊢ Prod.Lex r s (a, b) ((a, b).fst, d)
[PROOFSTEP]
exact Lex.right _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
⊢ ∀ (a : α × β), ¬Prod.Lex r s a a
[PROOFSTEP]
rintro ⟨i, a⟩ (⟨_, _, h⟩ | ⟨_, h⟩)
[GOAL]
case mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
i : α
a : β
h : r i i
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
i : α
a : β
h : s a a
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsTotal β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsTotal β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
exact Or.inl (.left _ _ hij)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsTotal β s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)
[PROOFSTEP]
exact (total_of s a b).imp (.right _) (.right _)
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsTotal β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
exact Or.inr (.left _ _ hji)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
{exact Or.inl (Lex.left _ _ hij)
}
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
{exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)
}
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
[PROOFSTEP]
exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
{exact Or.inr (Or.inr $ Lex.left _ _ hji)
}
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : _root_.IsTrichotomous α r
inst✝ : _root_.IsTrichotomous β s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
[PROOFSTEP]
exact Or.inr (Or.inr $ Lex.left _ _ hji)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map f₁ g₁ (map f₂ g₂ a) = a
[PROOFSTEP]
rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
⊢ a₁ = a₂
[PROOFSTEP]
inhabit β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂
[PROOFSTEP]
injection @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha : _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂
[PROOFSTEP]
injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb : _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ a, f a = c
[PROOFSTEP]
inhabit δ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c
[PROOFSTEP]
obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c
[PROOFSTEP]
exact ⟨a, congr_arg Prod.fst h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ a, g a = d
[PROOFSTEP]
inhabit γ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d
[PROOFSTEP]
obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d
[PROOFSTEP]
exact ⟨b, congr_arg Prod.snd h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
[PROOFSTEP]
haveI := Nonempty.map f ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
[PROOFSTEP]
haveI := Nonempty.map g ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
[PROOFSTEP]
exact (map_injective.and map_surjective).trans (and_and_and_comm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
⊢ f₁ (f₂ b) = b
[PROOFSTEP]
inhabit δ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b
[PROOFSTEP]
exact congr_arg Prod.fst (h (b, default))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d
[PROOFSTEP]
inhabit β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d
[PROOFSTEP]
exact congr_arg Prod.snd (h (default, d))


[GOAL]
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
⊢ f ∈ sections L ↔ Forall₂ (fun x x_1 => x ∈ x_1) f L
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
h : f ∈ sections L
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f L
[PROOFSTEP]
induction L generalizing f
[GOAL]
case refine'_1.nil
α : Type u_1
β : Type u_2
f : List α
h : f ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f []
[PROOFSTEP]
cases mem_singleton.1 h
[GOAL]
case refine'_1.nil.refl
α : Type u_1
β : Type u_2
h : [] ∈ sections []
⊢ Forall₂ (fun x x_1 => x ∈ x_1) [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
case refine'_1.cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
f : List α
h : f ∈ sections (head✝ :: tail✝)
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
[PROOFSTEP]
simp only [sections, bind_eq_bind, mem_bind, mem_map] at h
[GOAL]
case refine'_1.cons
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
f : List α
h : ∃ a, a ∈ sections tail✝ ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x x_1 => x ∈ x_1) f (head✝ :: tail✝)
[PROOFSTEP]
rcases h with ⟨_, _, _, _, rfl⟩
[GOAL]
case refine'_1.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ sections tail✝ → Forall₂ (fun x x_1 => x ∈ x_1) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ sections tail✝
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x x_1 => x ∈ x_1) (w✝ :: w✝¹) (head✝ :: tail✝)
[PROOFSTEP]
simp only [*, forall₂_cons, true_and_iff]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
h : Forall₂ (fun x x_1 => x ∈ x_1) f L
⊢ f ∈ sections L
[PROOFSTEP]
induction' h with a l f L al fL fs
[GOAL]
case refine'_2.nil
α : Type u_1
β : Type u_2
L : List (List α)
f : List α
⊢ [] ∈ sections []
[PROOFSTEP]
simp only [sections, mem_singleton]
[GOAL]
case refine'_2.cons
α : Type u_1
β : Type u_2
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x x_1 => x ∈ x_1) f L
fs : f ∈ sections L
⊢ a :: f ∈ sections (l :: L)
[PROOFSTEP]
simp only [sections, bind_eq_bind, mem_bind, mem_map]
[GOAL]
case refine'_2.cons
α : Type u_1
β : Type u_2
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x x_1 => x ∈ x_1) f L
fs : f ∈ sections L
⊢ ∃ a_1, a_1 ∈ sections L ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f
[PROOFSTEP]
exact ⟨f, fs, a, al, rfl⟩


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
H : Nodup l
i : Fin (length l)
⊢ (fun x => { val := indexOf (↑x) l, isLt := (_ : indexOf (↑x) l < length l) })
      ((fun i => { val := get l i, property := (_ : get l { val := ↑i, isLt := (_ : ↑i < length l) } ∈ l) }) i) =
    i
[PROOFSTEP]
simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
H : Nodup l
x : { x // x ∈ l }
⊢ (fun i => { val := get l i, property := (_ : get l { val := ↑i, isLt := (_ : ↑i < length l) } ∈ l) })
      ((fun x => { val := indexOf (↑x) l, isLt := (_ : indexOf (↑x) l < length l) }) x) =
    x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : Nodup l
h : ∀ (x : α), x ∈ l
i : Fin (length l)
⊢ (fun a => { val := indexOf a l, isLt := (_ : indexOf a l < length l) }) ((fun i => get l i) i) = i
[PROOFSTEP]
simp [List.get_indexOf, nd]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : Nodup l
h : ∀ (x : α), x ∈ l
a : α
⊢ (fun i => get l i) ((fun a => { val := indexOf a l, isLt := (_ : indexOf a l < length l) }) a) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ l <+ l'
[PROOFSTEP]
induction' l with hd tl IH generalizing l' f
[GOAL]
case nil
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? [] ix = get? l' (↑f ix)
⊢ [] <+ l'
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
⊢ hd :: tl <+ l'
[PROOFSTEP]
have : some hd = _ := hf 0
[GOAL]
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : some hd = get? l' (↑f 0)
⊢ hd :: tl <+ l'
[PROOFSTEP]
rw [eq_comm, List.get?_eq_some] at this
[GOAL]
case cons
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
this : ∃ h, get l' { val := ↑f 0, isLt := h } = hd
⊢ hd :: tl <+ l'
[PROOFSTEP]
obtain ⟨w, h⟩ := this
[GOAL]
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
⊢ hd :: tl <+ l'
[PROOFSTEP]
let f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b =>
    by
    dsimp only
    rw [tsub_le_tsub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact b.succ_pos
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f (a + 1) - (↑f 0 + 1) ≤ ↑f (b + 1) - (↑f 0 + 1) ↔ a ≤ b
[PROOFSTEP]
rw [tsub_le_tsub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (b + 1)
[PROOFSTEP]
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
a b : ℕ
⊢ 0 < b + 1
[PROOFSTEP]
exact b.succ_pos
[GOAL]
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
⊢ hd :: tl <+ l'
[PROOFSTEP]
have : ∀ ix, tl.get? ix = (l'.drop (f 0 + 1)).get? (f' ix) :=
  by
  intro ix
  rw [List.get?_drop, OrderEmbedding.coe_ofMapLEIff, add_tsub_cancel_of_le, ← hf, List.get?]
  rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
  exact ix.succ_pos
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
⊢ ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
[PROOFSTEP]
intro ix
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
[PROOFSTEP]
rw [List.get?_drop, OrderEmbedding.coe_ofMapLEIff, add_tsub_cancel_of_le, ← hf, List.get?]
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ ↑f 0 + 1 ≤ ↑f (ix + 1)
[PROOFSTEP]
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
ix : ℕ
⊢ 0 < ix + 1
[PROOFSTEP]
exact ix.succ_pos
[GOAL]
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ hd :: tl <+ l'
[PROOFSTEP]
rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
[GOAL]
case cons.intro
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] ++ tl <+ take (↑f 0 + 1) l' ++ drop (↑f 0 + 1) l'
[PROOFSTEP]
apply List.Sublist.append _ (IH _ this)
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ [hd] <+ take (↑f 0 + 1) l'
[PROOFSTEP]
rw [List.singleton_sublist, ← h, l'.get_take _ (Nat.lt_succ_self _)]
[GOAL]
α : Type u_1
l l'✝ : List α
f✝ : ℕ ↪o ℕ
hf✝ : ∀ (ix : ℕ), get? l ix = get? l'✝ (↑f✝ ix)
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), get? tl ix = get? l' (↑f ix)) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? (hd :: tl) ix = get? l' (↑f ix)
w : ↑f 0 < length l'
h : get l' { val := ↑f 0, isLt := w } = hd
f' : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (fun i => ↑f (i + 1) - (↑f 0 + 1))
    (_ : ∀ (a b : ℕ), (fun i => ↑f (i + 1) - (↑f 0 + 1)) a ≤ (fun i => ↑f (i + 1) - (↑f 0 + 1)) b ↔ a ≤ b)
this : ∀ (ix : ℕ), get? tl ix = get? (drop (↑f 0 + 1) l') (↑f' ix)
⊢ get (take (Nat.succ (↑f 0)) l') { val := ↑f 0, isLt := (_ : ↑f 0 < length (take (Nat.succ (↑f 0)) l')) } ∈
    take (↑f 0 + 1) l'
[PROOFSTEP]
apply List.get_mem
[GOAL]
α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
l l' : List α
⊢ l <+ l' → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
[PROOFSTEP]
intro H
[GOAL]
case mp
α : Type u_1
l l' : List α
H : l <+ l'
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
[PROOFSTEP]
induction' H with xs ys y _H IH xs ys x _H IH
[GOAL]
case mp.slnil
α : Type u_1
l l' : List α
⊢ ∃ f, ∀ (ix : ℕ), get? [] ix = get? [] (↑f ix)
[PROOFSTEP]
simp
[GOAL]
case mp.cons
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
[PROOFSTEP]
obtain ⟨f, hf⟩ := IH
[GOAL]
case mp.cons.intro
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? xs ix = get? (y :: ys) (↑f ix)
[PROOFSTEP]
refine' ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), _⟩
[GOAL]
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
x✝ : ℕ
⊢ ∀ ⦃b : ℕ⦄, x✝ < b → (fun x => x + 1) x✝ < (fun x => x + 1) b
[PROOFSTEP]
simp
[GOAL]
case mp.cons.intro
α : Type u_1
l l' xs ys : List α
y : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (ix : ℕ),
    get? xs ix =
      get? (y :: ys)
        (↑(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x => x + 1) (_ : ∀ (x a : ℕ), x < a → x + 1 < a + 1)))
          ix)
[PROOFSTEP]
simpa using hf
[GOAL]
case mp.cons₂
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
IH : ∃ f, ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
[PROOFSTEP]
obtain ⟨f, hf⟩ := IH
[GOAL]
case mp.cons₂.intro
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? (x :: xs) ix = get? (x :: ys) (↑f ix)
[PROOFSTEP]
refine' ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) _, _⟩
[GOAL]
case mp.cons₂.intro.refine'_1
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (a b : ℕ),
    (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤
        (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔
      a ≤ b
[PROOFSTEP]
rintro ⟨_ | a⟩ ⟨_ | b⟩
[GOAL]
case mp.cons₂.intro.refine'_1.zero.zero
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤
      (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔
    Nat.zero ≤ Nat.zero
[PROOFSTEP]
simp [Nat.succ_le_succ_iff]
[GOAL]
case mp.cons₂.intro.refine'_1.zero.succ
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝ : ℕ
⊢ (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ≤
      (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔
    Nat.zero ≤ Nat.succ n✝
[PROOFSTEP]
simp [Nat.succ_le_succ_iff]
[GOAL]
case mp.cons₂.intro.refine'_1.succ.zero
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝ : ℕ
⊢ (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ≤
      (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) Nat.zero ↔
    Nat.succ n✝ ≤ Nat.zero
[PROOFSTEP]
simp [Nat.succ_le_succ_iff]
[GOAL]
case mp.cons₂.intro.refine'_1.succ.succ
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝¹ n✝ : ℕ
⊢ (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝¹) ≤
      (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) (Nat.succ n✝) ↔
    Nat.succ n✝¹ ≤ Nat.succ n✝
[PROOFSTEP]
simp [Nat.succ_le_succ_iff]
[GOAL]
case mp.cons₂.intro.refine'_2
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ ∀ (ix : ℕ),
    get? (x :: xs) ix =
      get? (x :: ys)
        (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
              (_ :
                ∀ (a b : ℕ),
                  (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤
                      (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔
                    a ≤ b))
          ix)
[PROOFSTEP]
rintro ⟨_ | i⟩
[GOAL]
case mp.cons₂.intro.refine'_2.zero
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
⊢ get? (x :: xs) Nat.zero =
    get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤
                    (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔
                  a ≤ b))
        Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case mp.cons₂.intro.refine'_2.succ
α : Type u_1
l l' xs ys : List α
x : α
_H : xs <+ ys
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? xs ix = get? ys (↑f ix)
n✝ : ℕ
⊢ get? (x :: xs) (Nat.succ n✝) =
    get? (x :: ys)
      (↑(OrderEmbedding.ofMapLEIff (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix)))
            (_ :
              ∀ (a b : ℕ),
                (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) a ≤
                    (fun ix => if ix = 0 then 0 else Nat.succ (↑f (Nat.pred ix))) b ↔
                  a ≤ b))
        (Nat.succ n✝))
[PROOFSTEP]
simpa using hf _
[GOAL]
case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → l <+ l'
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mpr.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ l <+ l'
[PROOFSTEP]
exact sublist_of_orderEmbedding_get?_eq f hf
[GOAL]
α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
[PROOFSTEP]
rw [sublist_iff_exists_orderEmbedding_get?_eq]
[GOAL]
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) ↔ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)) → ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
[PROOFSTEP]
have h : ∀ {i : ℕ} (_ : i < l.length), f i < l'.length :=
  by
  intro i hi
  specialize hf i
  rw [get?_eq_get hi, eq_comm, get?_eq_some] at hf
  obtain ⟨h, -⟩ := hf
  exact h
[GOAL]
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
⊢ ∀ {i : ℕ}, i < length l → ↑f i < length l'
[PROOFSTEP]
intro i hi
[GOAL]
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
i : ℕ
hi : i < length l
⊢ ↑f i < length l'
[PROOFSTEP]
specialize hf i
[GOAL]
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : get? l i = get? l' (↑f i)
⊢ ↑f i < length l'
[PROOFSTEP]
rw [get?_eq_get hi, eq_comm, get?_eq_some] at hf
[GOAL]
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
hf : ∃ h, get l' { val := ↑f i, isLt := h } = get l { val := i, isLt := hi }
⊢ ↑f i < length l'
[PROOFSTEP]
obtain ⟨h, -⟩ := hf
[GOAL]
case intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < length l
h : ↑f i < length l'
⊢ ↑f i < length l'
[PROOFSTEP]
exact h
[GOAL]
case mp.intro
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
[PROOFSTEP]
refine' ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) _, _⟩
[GOAL]
case mp.intro.refine'_1
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (a b : Fin (length l)),
    (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) a ≤
        (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') }) b ↔
      a ≤ b
[PROOFSTEP]
simp
[GOAL]
case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
⊢ ∀ (ix : Fin (length l)),
    get l ix =
      get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              (_ :
                ∀ (a a_1 : Fin (length l)),
                  { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                      { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                    a ≤ a_1))
          ix)
[PROOFSTEP]
intro i
[GOAL]
case mp.intro.refine'_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ get l i =
    get l'
      (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
            (_ :
              ∀ (a a_1 : Fin (length l)),
                { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                    { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                  a ≤ a_1))
        i)
[PROOFSTEP]
apply Option.some_injective
[GOAL]
case mp.intro.refine'_2.a
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
h : ∀ {i : ℕ}, i < length l → ↑f i < length l'
i : Fin (length l)
⊢ some (get l i) =
    some
      (get l'
        (↑(OrderEmbedding.ofMapLEIff (fun ix => { val := ↑f ↑ix, isLt := (_ : ↑f ↑ix < length l') })
              (_ :
                ∀ (a a_1 : Fin (length l)),
                  { val := ↑f ↑a, isLt := (_ : ↑f ↑a < length l') } ≤
                      { val := ↑f ↑a_1, isLt := (_ : ↑f ↑a_1 < length l') } ↔
                    a ≤ a_1))
          i))
[PROOFSTEP]
simpa [get?_eq_get i.2, get?_eq_get (h i.2)] using hf i
[GOAL]
case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)) → ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mpr.intro
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∃ f, ∀ (ix : ℕ), get? l ix = get? l' (↑f ix)
[PROOFSTEP]
refine' ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length) _, _⟩
[GOAL]
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ StrictMono fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l'
[PROOFSTEP]
intro i j h
[GOAL]
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j
[PROOFSTEP]
dsimp only
[GOAL]
case mpr.intro.refine'_1
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
⊢ (if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') <
    if hi : j < length l then ↑(↑f { val := j, isLt := hi }) else j + length l'
[PROOFSTEP]
split_ifs with hi hj hj
[GOAL]
case pos
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < ↑(↑f { val := j, isLt := hj })
[PROOFSTEP]
rwa [Fin.val_fin_lt, f.lt_iff_lt]
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < j + length l'
[PROOFSTEP]
rw [add_comm]
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : i < length l
hj : ¬j < length l
⊢ ↑(↑f { val := i, isLt := hi }) < length l' + j
[PROOFSTEP]
exact lt_add_of_lt_of_pos (Fin.is_lt _) (i.zero_le.trans_lt h)
[GOAL]
case pos
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : j < length l
⊢ i + length l' < ↑(↑f { val := j, isLt := hj })
[PROOFSTEP]
exact absurd (h.trans hj) hi
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i j : ℕ
h : i < j
hi : ¬i < length l
hj : ¬j < length l
⊢ i + length l' < j + length l'
[PROOFSTEP]
simpa using h
[GOAL]
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
⊢ ∀ (ix : ℕ),
    get? l ix =
      get? l'
        (↑(OrderEmbedding.ofStrictMono
              (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
              (_ :
                ∀ ⦃i j : ℕ⦄,
                  i < j →
                    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
                      (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j))
          ix)
[PROOFSTEP]
intro i
[GOAL]
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i =
    get? l'
      (↑(OrderEmbedding.ofStrictMono
            (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l')
            (_ :
              ∀ ⦃i j : ℕ⦄,
                i < j →
                  (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') i <
                    (fun i => if hi : i < length l then ↑(↑f { val := i, isLt := hi }) else i + length l') j))
        i)
[PROOFSTEP]
simp only [OrderEmbedding.coe_ofStrictMono]
[GOAL]
case mpr.intro.refine'_2
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
⊢ get? l i = get? l' (if h : i < length l then ↑(↑f { val := i, isLt := (_ : i < length l) }) else i + length l')
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : i < length l
⊢ get? l i = get? l' ↑(↑f { val := i, isLt := (_ : i < length l) })
[PROOFSTEP]
rw [get?_eq_get hi, get?_eq_get, ← hf]
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ get? l i = get? l' (i + length l')
[PROOFSTEP]
rw [get?_eq_none.mpr, get?_eq_none.mpr]
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l' ≤ i + length l'
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
l l' : List α
f : Fin (length l) ↪o Fin (length l')
hf : ∀ (ix : Fin (length l)), get l ix = get l' (↑f ix)
i : ℕ
hi : ¬i < length l
⊢ length l ≤ i
[PROOFSTEP]
simpa using hi
[GOAL]
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = get l n ∧ x = get l m
[PROOFSTEP]
classical
rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist, sublist_iff_exists_fin_orderEmbedding_get_eq]
constructor
· rintro ⟨f, hf⟩
  refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
  · rw [← hf, ← hf]; simp
· rintro ⟨n, m, hnm, h, h'⟩
  refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
  · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
    · simp
    · simp [hnm]
    · simp
    · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, nonpos_iff_eq_zero] at hi hj
      simp [hi, hj]
  · rintro ⟨⟨_ | i⟩, hi⟩
    · simpa using h
    · simpa using h'
[GOAL]
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = get l n ∧ x = get l m
[PROOFSTEP]
rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist, sublist_iff_exists_fin_orderEmbedding_get_eq]
[GOAL]
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) ↔
    ∃ n m x_1, x = get l n ∧ x = get l m
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)) →
    ∃ n m x_1, x = get l n ∧ x = get l m
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ ∃ n m x_1, x = get l n ∧ x = get l m
[PROOFSTEP]
refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
[GOAL]
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ 0 < length (replicate 2 x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ 1 < length (replicate 2 x)
[PROOFSTEP]
simp
[GOAL]
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get l (↑f { val := 0, isLt := (_ : 0 < Nat.succ 1) }) ∧ x = get l (↑f { val := 1, isLt := (_ : 1 < Nat.succ 1) })
[PROOFSTEP]
rw [← hf, ← hf]
[GOAL]
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (length (replicate 2 x)) ↪o Fin (length l)
hf : ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
⊢ x = get (replicate 2 x) { val := 0, isLt := (_ : 0 < Nat.succ 1) } ∧
    x = get (replicate 2 x) { val := 1, isLt := (_ : 1 < Nat.succ 1) }
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = get l n ∧ x = get l m) →
    ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
[PROOFSTEP]
rintro ⟨n, m, hnm, h, h'⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∃ f, ∀ (ix : Fin (length (replicate 2 x))), get (replicate 2 x) ix = get l (↑f ix)
[PROOFSTEP]
refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ StrictMono fun i => if ↑i = 0 then n else m
[PROOFSTEP]
rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1.mk.zero.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.zero, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }
[PROOFSTEP]
simp [hnm]
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
hj : Nat.zero < length (replicate 2 x)
⊢ { val := Nat.succ n✝, isLt := hi } < { val := Nat.zero, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.zero, isLt := hj }
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj : Nat.succ n✝ < length (replicate 2 x)
⊢ { val := Nat.succ n✝¹, isLt := hi } < { val := Nat.succ n✝, isLt := hj } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj }
[PROOFSTEP]
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, nonpos_iff_eq_zero] at hi hj
[GOAL]
case mpr.intro.intro.intro.intro.refine'_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝¹ : ℕ
hi✝ : Nat.succ n✝¹ < length (replicate 2 x)
n✝ : ℕ
hj✝ : Nat.succ n✝ < length (replicate 2 x)
hi : n✝¹ = 0
hj : n✝ = 0
⊢ { val := Nat.succ n✝¹, isLt := hi✝ } < { val := Nat.succ n✝, isLt := hj✝ } →
    (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝¹, isLt := hi✝ } <
      (fun i => if ↑i = 0 then n else m) { val := Nat.succ n✝, isLt := hj✝ }
[PROOFSTEP]
simp [hi, hj]
[GOAL]
case mpr.intro.intro.intro.intro.refine'_2
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
⊢ ∀ (ix : Fin (length (replicate 2 x))),
    get (replicate 2 x) ix =
      get l
        (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
              (_ :
                ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                  a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
          ix)
[PROOFSTEP]
rintro ⟨⟨_ | i⟩, hi⟩
[GOAL]
case mpr.intro.intro.intro.intro.refine'_2.mk.zero
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
hi : Nat.zero < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.zero, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.zero, isLt := hi })
[PROOFSTEP]
simpa using h
[GOAL]
case mpr.intro.intro.intro.intro.refine'_2.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin (length l)
hnm : n < m
h : x = get l n
h' : x = get l m
n✝ : ℕ
hi : Nat.succ n✝ < length (replicate 2 x)
⊢ get (replicate 2 x) { val := Nat.succ n✝, isLt := hi } =
    get l
      (↑(OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m)
            (_ :
              ∀ ⦃a b : Fin (length (replicate 2 x))⦄,
                a < b → (fun i => if ↑i = 0 then n else m) a < (fun i => if ↑i = 0 then n else m) b))
        { val := Nat.succ n✝, isLt := hi })
[PROOFSTEP]
simpa using h'


[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
h : Finite α
f : α ≃ β
⊢ Finite β
[PROOFSTEP]
cases' h with n e
[GOAL]
case intro
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
f : α ≃ β
n : ℕ
e : α ≃ Fin n
⊢ Finite β
[PROOFSTEP]
exact Finite.intro (f.symm.trans e)