Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
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₂
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝¹))
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inr val✝)