[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
⊢ Acc s (↑f a) → Acc r a
[PROOFSTEP]
generalize h : f a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
[PROOFSTEP]
subst h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r →r s
h : (fun o => o.toFun) f = (fun o => o.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r →r s
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h : (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ } = (fun o => o.toFun) g
⊢ { toFun := toFun✝, map_rel' := map_rel'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
map_rel'✝¹ : ∀ {a b : α}, r a b → s (toFun✝¹ a) (toFun✝¹ b)
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h :
  (fun o => o.toFun) { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } =
    (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ }
⊢ { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } = { toFun := toFun✝, map_rel' := map_rel'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
⊢ Injective f
[PROOFSTEP]
intro x y hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
rcases trichotomous_of r x y with (h | h | h)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ x = y
[PROOFSTEP]
have := hf h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ x = y
[PROOFSTEP]
rw [hxy] at this 
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ False
[PROOFSTEP]
exact irrefl_of s (f y) this
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y
[PROOFSTEP]
exact h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y
[PROOFSTEP]
have := hf h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ x = y
[PROOFSTEP]
rw [hxy] at this 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ False
[PROOFSTEP]
exact irrefl_of s (f y) this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ WellFounded r → WellFounded s
[PROOFSTEP]
refine RelHomClass.wellFounded (RelHom.mk ?_ ?_ : s →r r)
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ β → α
[PROOFSTEP]
exact Classical.choose hf.hasRightInverse
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ ∀ {a b : β}, s a b → r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
[PROOFSTEP]
intro a b h
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
[PROOFSTEP]
apply o.2
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ s (f (Classical.choose (_ : HasRightInverse f) a)) (f (Classical.choose (_ : HasRightInverse f) b))
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
iterate 2 apply Classical.choose_spec hf.hasRightInverse
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
apply Classical.choose_spec hf.hasRightInverse
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
apply Classical.choose_spec hf.hasRightInverse
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r ↪r s
h : (fun x => x.toFun) f = (fun x => x.toFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟩⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r ↪r s
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } =
    (fun x => x.toFun) g
⊢ { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } = g
[PROOFSTEP]
rcases g with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
map_rel_iff'✝¹ :
  ∀ {a b : α}, s (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } a) (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } b) ↔ r a b
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x => x.toFun) { toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =
    (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }
⊢ { toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =
    { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : s ↪r t
⊢ ∀ {a b : α},
    t (↑(Embedding.trans f.toEmbedding g.toEmbedding) a) (↑(Embedding.trans f.toEmbedding g.toEmbedding) b) ↔ r a b
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
⊢ r = ↑f ⁻¹'o s
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (↑f ⁻¹'o s) a b
[PROOFSTEP]
exact f.map_rel_iff.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
⊢ Acc s (↑f a) → Acc r a
[PROOFSTEP]
generalize h : f a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
[PROOFSTEP]
subst h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ ∀ {a b : Quotient inst✝}, r (↑(Embedding.quotientOut α) a) (↑(Embedding.quotientOut α) b) ↔ Quotient.lift₂ r H a b
[PROOFSTEP]
refine' @fun x y => Quotient.inductionOn₂ x y fun a b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ r (↑(Embedding.quotientOut α) (Quotient.mk inst✝ a)) (↑(Embedding.quotientOut α) (Quotient.mk inst✝ b)) ↔
    Quotient.lift₂ r H (Quotient.mk inst✝ a) (Quotient.mk inst✝ b)
[PROOFSTEP]
apply iff_iff_eq.2 (H _ _ _ _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ ↑(Embedding.quotientOut α) (Quotient.mk inst✝ a) ≈ a
[PROOFSTEP]
apply Quotient.mk_out
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ ↑(Embedding.quotientOut α) (Quotient.mk inst✝ b) ≈ b
[PROOFSTEP]
apply Quotient.mk_out
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) ↔ Acc r a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) → Acc r a
[PROOFSTEP]
exact RelHomClass.acc (Quotient.mkRelHom H) a
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
intro ac
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
induction' ac with _ _ IH
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
[PROOFSTEP]
refine' ⟨_, fun q h => _⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
q : Quotient inst✝
h : Quotient.lift₂ r H q (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) q
[PROOFSTEP]
obtain ⟨a', rfl⟩ := q.exists_rep
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
a' : α
h : Quotient.lift₂ r H (Quotient.mk inst✝ a') (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a')
[PROOFSTEP]
exact IH a' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r
[PROOFSTEP]
exact RelHomClass.wellFounded (Quotient.mkRelHom H)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)
[PROOFSTEP]
refine' fun wf => ⟨fun q => _⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient inst✝
⊢ Acc (Quotient.lift₂ r H) q
[PROOFSTEP]
obtain ⟨a, rfl⟩ := q.exists_rep
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
exact acc_lift₂_iff.2 (wf.apply a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s
[PROOFSTEP]
haveI := @IsAsymm.isIrrefl β s _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
⊢ r ↪r s
[PROOFSTEP]
refine' ⟨⟨f, fun a b e => _⟩, @fun a b => ⟨fun h => _, H _ _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ a = b
[PROOFSTEP]
refine' ((@trichotomous _ r _ a b).resolve_left _).resolve_right _
[GOAL]
case refine'_1.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ ¬r a b
[PROOFSTEP]
exact fun h => @irrefl _ s _ _ (by simpa [e] using H _ _ h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
h : r a b
⊢ s (?m.45031 h) (?m.45031 h)
[PROOFSTEP]
simpa [e] using H _ _ h
[GOAL]
case refine'_1.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ ¬r b a
[PROOFSTEP]
exact fun h => @irrefl _ s _ _ (by simpa [e] using H _ _ h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
h : r b a
⊢ s (?m.45243 h) (?m.45243 h)
[PROOFSTEP]
simpa [e] using H _ _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
⊢ r a b
[PROOFSTEP]
refine' (@trichotomous _ r _ a b).resolve_right (Or.rec (fun e => _) fun h' => _)
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
e : a = b
⊢ False
[PROOFSTEP]
subst e
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
h' : r b a
⊢ False
[PROOFSTEP]
exact asymm (H _ _ h') h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } a)
        (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } b) ↔
      Sum.LiftRel r t a b
[PROOFSTEP]
rintro (a | b) (c | d)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } a)
        (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } b) ↔
      Sum.Lex r t a b
[PROOFSTEP]
rintro (a | b) (c | d)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
s : β → β → Prop
a : α
h : ¬r a a
⊢ ∀ {a_1 b : β},
    Prod.Lex r s (↑{ toFun := Prod.mk a, inj' := (_ : Injective (Prod.mk a)) } a_1)
        (↑{ toFun := Prod.mk a, inj' := (_ : Injective (Prod.mk a)) } b) ↔
      s a_1 b
[PROOFSTEP]
simp [Prod.lex_def, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
b : β
h : ¬s b b
⊢ ∀ {a b_1 : α},
    Prod.Lex r s (↑{ toFun := fun a => (a, b), inj' := (_ : Injective fun a => (a, b)) } a)
        (↑{ toFun := fun a => (a, b), inj' := (_ : Injective fun a => (a, b)) } b_1) ↔
      r a b_1
[PROOFSTEP]
simp [Prod.lex_def, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u (↑{ toFun := Prod.map ↑f ↑g, inj' := (_ : Injective (Prod.map ↑f ↑g)) } a)
        (↑{ toFun := Prod.map ↑f ↑g, inj' := (_ : Injective (Prod.map ↑f ↑g)) } b) ↔
      Prod.Lex r t a b
[PROOFSTEP]
simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (↑e₁ a) (↑e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (↑e₂ a) (↑e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ r (↑f.symm a) (↑f.symm b) ↔ s a b
[PROOFSTEP]
erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : HEq r s
a b : α
⊢ s (↑(Equiv.cast h₁) a) (↑(Equiv.cast h₁) b) ↔ r a b
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : HEq r s
⊢ s (↑(Equiv.cast (_ : α = α)) a) (↑(Equiv.cast (_ : α = α)) b) ↔ r a b
[PROOFSTEP]
rw [eq_of_heq h₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : HEq r s
⊢ s (↑(Equiv.cast (_ : α = α)) a) (↑(Equiv.cast (_ : α = α)) b) ↔ s a b
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : HEq r s
h₂' : HEq s t
x : α
⊢ ↑(RelIso.trans (RelIso.cast h₁ h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ↑(RelIso.trans (RelIso.cast (_ : α = α) h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
x : α
y : β
⊢ r x (↑(RelIso.symm e) y) ↔ s (↑e x) y
[PROOFSTEP]
rw [← e.map_rel_iff, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
x : β
y : α
⊢ r (↑(RelIso.symm e) x) y ↔ s x (↑e y)
[PROOFSTEP]
rw [← e.map_rel_iff, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
⊢ Sum.Lex s₁ s₂ (↑(Equiv.sumCongr e₁.toEquiv e₂.toEquiv) a) (↑(Equiv.sumCongr e₁.toEquiv e₂.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases' e₁ with f hf
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
⊢ Sum.Lex s₁ s₂ (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv e₂.toEquiv) a)
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv e₂.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases' e₂ with g hg
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) a)
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases a
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk.inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ : α₁
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ : α₂
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.82669
α₂ : Type ?u.82677
β₁ : Type ?u.82670
β₂ : Type ?u.82678
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
⊢ ∀ {a b : α₁ × α₂},
    Prod.Lex s₁ s₂ (↑(Equiv.prodCongr e₁.toEquiv e₂.toEquiv) a) (↑(Equiv.prodCongr e₁.toEquiv e₂.toEquiv) b) ↔
      Prod.Lex r₁ r₂ a b
[PROOFSTEP]
simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff, e₁.injective.eq_iff]
