awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelIso.Basic
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
f : α → β
g : β → α
hf : f = (⇑e : (a : α) → β)
hg : g = (⇑(e.symm (r := r) (s := s)) : (a : β) → α)
x : β
⊢ f (g x) = x

Tactic:
simp [hf, hg]
-- Module: Mathlib.Order.RelIso.Basic
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
f : α → β
g : β → α
hf : f = (⇑e : (a : α) → β)
hg : g = (⇑(e.symm (r := r) (s := s)) : (a : β) → α)
⊢ ∀ {a b : α},
    s (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a)
        (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b) ↔
      r a b

Tactic:
simp [hf, e.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = (⇑e : (a : α) → β)
hg : g = (⇑(e.symm (r := r) (s := s)) : (a : β) → α)
⊢ (⇑(e.copy (r := r) (s := s) f g hf hg) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = (⇑e : (a : α) → β)
hg : g = (⇑(e.symm (r := r) (s := s)) : (a : β) → α)
⊢ e.copy (r := r) (s := s) f g hf hg = e

Tactic:
DFunLike.coe_injective hf

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
s : β → β → Prop
a : α
⊢ Eq.{u_2 + 1} (α := β) ((RelIso.preimage f s : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
s : β → β → Prop
a : β
⊢ Eq.{u_1 + 1} (α := α) (((RelIso.preimage f s).symm (r := (⇑f : (a : α) → β) ⁻¹'o s) (s := s) : (a : β) → α) a : α)
    ((f.symm : (a : β) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α_1 → α_1 → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : β ≃ α
⊢ IsWellOrder β ((⇑f : (a : β) → α) ⁻¹'o r)

Tactic:
@RelEmbedding.isWellOrder _ _ (f ⁻¹'o r) r (RelIso.preimage f r) _

Premises used: RelEmbedding.isWellOrder, RelIso.toRelEmbedding, RelIso.preimage
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α_1 → α_1 → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ IsWellOrder (ULift.{u_5, u} α) (ULift.down ⁻¹'o r)

Tactic:
IsWellOrder.preimage r Equiv.ulift

Premises used: Equiv.ulift, RelIso.IsWellOrder.preimage, Order.Preimage
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x : r ≃r s
h :
  ∀ (x_1 : α),
    Eq.{u_2 + 1} (α := β)
      (((fun (f : { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
                ofSurjective (r := r) (s := s) (↑f : r ↪r s) ⋯)
              ((fun (f : r ≃r s) ↦
                  (Subtype.mk (p := fun (f : r ↪r s) ↦
                      Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
                      (f.toRelEmbedding (r := r) (s := s)) ⋯ :
                    { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
                x) :
            (a : α) → β)
          x_1 :
        β)
      ((x : (a : α) → β) x_1 : β)
⊢ (fun (f : { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
        ofSurjective (r := r) (s := s) (↑f : r ↪r s) ⋯)
      ((fun (f : r ≃r s) ↦
          (Subtype.mk (p := fun (f : r ↪r s) ↦ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
              (f.toRelEmbedding (r := r) (s := s)) ⋯ :
            { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x : r ≃r s
x_1 : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (f : { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }) ↦
              ofSurjective (r := r) (s := s) (↑f : r ↪r s) ⋯)
            ((fun (f : r ≃r s) ↦
                (Subtype.mk (p := fun (f : r ↪r s) ↦ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β))
                    (f.toRelEmbedding (r := r) (s := s)) ⋯ :
                  { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)

Tactic:
rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
h :
  ∀ (x : α₁),
    Eq.{u_6 + 1} (α := β₁)
      (((fun (f₂ : r₂ →r s₂) ↦
                e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r :=
                  r₁) (s := s₂) (t := s₁)
                  (f₂.comp (r := r₁) (s := r₂) (t := s₂)
                    (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
              ((fun (f₁ : r₁ →r s₁) ↦
                  e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
                    (f₁.comp (r := r₂) (s := r₁) (t := s₁)
                      (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
                f₁) :
            (a : α₁) → β₁)
          x :
        β₁)
      ((f₁ : (a : α₁) → β₁) x : β₁)
⊢ (fun (f₂ : r₂ →r s₂) ↦
        e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r := r₁) (s :=
          s₂) (t := s₁)
          (f₂.comp (r := r₁) (s := r₂) (t := s₂) (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
      ((fun (f₁ : r₁ →r s₁) ↦
          e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
            (f₁.comp (r := r₂) (s := r₁) (t := s₁)
              (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
        f₁) =
    f₁

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
x : α₁
⊢ Eq.{u_6 + 1} (α := β₁)
    (((fun (f₂ : r₂ →r s₂) ↦
              e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r := r₁)
                (s := s₂) (t := s₁)
                (f₂.comp (r := r₁) (s := r₂) (t := s₂)
                  (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
            ((fun (f₁ : r₁ →r s₁) ↦
                e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
                  (f₁.comp (r := r₂) (s := r₁) (t := s₁)
                    (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
              f₁) :
          (a : α₁) → β₁)
        x :
      β₁)
    ((f₁ : (a : α₁) → β₁) x : β₁)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
h :
  ∀ (x : α₂),
    Eq.{u_8 + 1} (α := β₂)
      (((fun (f₁ : r₁ →r s₁) ↦
                e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
                  (f₁.comp (r := r₂) (s := r₁) (t := s₁)
                    (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
              ((fun (f₂ : r₂ →r s₂) ↦
                  e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r :=
                    r₁) (s := s₂) (t := s₁)
                    (f₂.comp (r := r₁) (s := r₂) (t := s₂)
                      (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
                f₂) :
            (a : α₂) → β₂)
          x :
        β₂)
      ((f₂ : (a : α₂) → β₂) x : β₂)
⊢ (fun (f₁ : r₁ →r s₁) ↦
        e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
          (f₁.comp (r := r₂) (s := r₁) (t := s₁)
            (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
      ((fun (f₂ : r₂ →r s₂) ↦
          e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r := r₁)
            (s := s₂) (t := s₁)
            (f₂.comp (r := r₁) (s := r₂) (t := s₂)
              (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
        f₂) =
    f₂

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
x : α₂
⊢ Eq.{u_8 + 1} (α := β₂)
    (((fun (f₁ : r₁ →r s₁) ↦
              e₂.toRelEmbedding (r := s₁) (s := s₂).toRelHom (r := s₁) (s := s₂).comp (r := r₂) (s := s₁) (t := s₂)
                (f₁.comp (r := r₂) (s := r₁) (t := s₁)
                  (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).toRelHom (r := r₂) (s := r₁))))
            ((fun (f₂ : r₂ →r s₂) ↦
                e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁).toRelHom (r := s₂) (s := s₁).comp (r :=
                  r₁) (s := s₂) (t := s₁)
                  (f₂.comp (r := r₁) (s := r₂) (t := s₂)
                    (e₁.toRelEmbedding (r := r₁) (s := r₂).toRelHom (r := r₁) (s := r₂))))
              f₂) :
          (a : α₂) → β₂)
        x :
      β₂)
    ((f₂ : (a : α₂) → β₂) x : β₂)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
h :
  ∀ (x : α₁),
    Eq.{u_6 + 1} (α := β₁)
      (((fun (f₂ : r₂ ↪r s₂) ↦
                (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂)
                  (t := s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
              ((fun (f₁ : r₁ ↪r s₁) ↦
                  (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁)
                        f₁).trans
                    (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
                f₁) :
            (a : α₁) → β₁)
          x :
        β₁)
      ((f₁ : (a : α₁) → β₁) x : β₁)
⊢ (fun (f₂ : r₂ ↪r s₂) ↦
        (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t :=
          s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
      ((fun (f₁ : r₁ ↪r s₁) ↦
          (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans
            (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
        f₁) =
    f₁

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
x : α₁
⊢ Eq.{u_6 + 1} (α := β₁)
    (((fun (f₂ : r₂ ↪r s₂) ↦
              (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂)
                (t := s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
            ((fun (f₁ : r₁ ↪r s₁) ↦
                (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁)
                      f₁).trans
                  (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
              f₁) :
          (a : α₁) → β₁)
        x :
      β₁)
    ((f₁ : (a : α₁) → β₁) x : β₁)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
h :
  ∀ (x : α₂),
    Eq.{u_8 + 1} (α := β₂)
      (((fun (f₁ : r₁ ↪r s₁) ↦
                (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁)
                      f₁).trans
                  (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
              ((fun (f₂ : r₂ ↪r s₂) ↦
                  (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s :=
                    s₂) (t := s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
                f₂) :
            (a : α₂) → β₂)
          x :
        β₂)
      ((f₂ : (a : α₂) → β₂) x : β₂)
⊢ (fun (f₁ : r₁ ↪r s₁) ↦
        (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans
          (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
      ((fun (f₂ : r₂ ↪r s₂) ↦
          (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t :=
            s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
        f₂) =
    f₂

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
x : α₂
⊢ Eq.{u_8 + 1} (α := β₂)
    (((fun (f₁ : r₁ ↪r s₁) ↦
              (e₁.symm (r := r₁) (s := r₂).toRelEmbedding (r := r₂) (s := r₁).trans (r := r₂) (s := r₁) (t := s₁)
                    f₁).trans
                (r := r₂) (s := s₁) (t := s₂) (e₂.toRelEmbedding (r := s₁) (s := s₂)))
            ((fun (f₂ : r₂ ↪r s₂) ↦
                (e₁.toRelEmbedding (r := r₁) (s := r₂).trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂)
                  (t := s₁) (e₂.symm (r := s₁) (s := s₂).toRelEmbedding (r := s₂) (s := s₁)))
              f₂) :
          (a : α₂) → β₂)
        x :
      β₂)
    ((f₂ : (a : α₂) → β₂) x : β₂)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
h :
  ∀ (x : α₁),
    Eq.{u_6 + 1} (α := β₁)
      (((fun (f₂ : r₂ ≃r s₂) ↦
                (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁)
                  (e₂.symm (r := s₁) (s := s₂)))
              ((fun (f₁ : r₁ ≃r s₁) ↦
                  (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t :=
                    s₂) e₂)
                f₁) :
            (a : α₁) → β₁)
          x :
        β₁)
      ((f₁ : (a : α₁) → β₁) x : β₁)
⊢ (fun (f₂ : r₂ ≃r s₂) ↦
        (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁) (e₂.symm (r := s₁) (s := s₂)))
      ((fun (f₁ : r₁ ≃r s₁) ↦
          (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t := s₂) e₂)
        f₁) =
    f₁

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
x : α₁
⊢ Eq.{u_6 + 1} (α := β₁)
    (((fun (f₂ : r₂ ≃r s₂) ↦
              (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁)
                (e₂.symm (r := s₁) (s := s₂)))
            ((fun (f₁ : r₁ ≃r s₁) ↦
                (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t := s₂)
                  e₂)
              f₁) :
          (a : α₁) → β₁)
        x :
      β₁)
    ((f₁ : (a : α₁) → β₁) x : β₁)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ≃r s₂
h :
  ∀ (x : α₂),
    Eq.{u_8 + 1} (α := β₂)
      (((fun (f₁ : r₁ ≃r s₁) ↦
                (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t := s₂)
                  e₂)
              ((fun (f₂ : r₂ ≃r s₂) ↦
                  (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁)
                    (e₂.symm (r := s₁) (s := s₂)))
                f₂) :
            (a : α₂) → β₂)
          x :
        β₂)
      ((f₂ : (a : α₂) → β₂) x : β₂)
⊢ (fun (f₁ : r₁ ≃r s₁) ↦
        (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t := s₂) e₂)
      ((fun (f₂ : r₂ ≃r s₂) ↦
          (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁) (e₂.symm (r := s₁) (s := s₂)))
        f₂) =
    f₂

Tactic:
ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
β₁ : Type u_6
α₂ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ≃r s₂
x : α₂
⊢ Eq.{u_8 + 1} (α := β₂)
    (((fun (f₁ : r₁ ≃r s₁) ↦
              (e₁.symm (r := r₁) (s := r₂).trans (r := r₂) (s := r₁) (t := s₁) f₁).trans (r := r₂) (s := s₁) (t := s₂)
                e₂)
            ((fun (f₂ : r₂ ≃r s₂) ↦
                (e₁.trans (r := r₁) (s := r₂) (t := s₂) f₂).trans (r := r₁) (s := s₂) (t := s₁)
                  (e₂.symm (r := s₁) (s := s₂)))
              f₂) :
          (a : α₂) → β₂)
        x :
      β₂)
    ((f₂ : (a : α₂) → β₂) x : β₂)

Tactic:
simp
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
obtain :
  ∀ (f : α₁ ≃ β₁) (hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          a)
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          b) ↔
      Sum.Lex r₁ r₂ a b
⊢ Sum.Lex s₁ s₂ ((e₁.toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) : (a : α₁ ⊕ α₂) → β₁ ⊕ β₂) a)
      ((e₁.toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) : (a : α₁ ⊕ α₂) → β₁ ⊕ β₂) b) ↔
    Sum.Lex r₁ r₂ a b

Tactic:
obtain ⟨f, hf⟩ := e₁
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
obtain :
  ∀ (g : α₂ ≃ β₂) (hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          a)
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          b) ↔
      Sum.Lex r₁ r₂ a b
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        a)
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr (e₂.toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        b) ↔
    Sum.Lex r₁ r₂ a b

Tactic:
obtain ⟨g, hg⟩ := e₂
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ ((f : (a : α₁) → β₁) a) ((f : (a : α₁) → β₁) b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ ((g : (a : α₂) → β₂) a) ((g : (a : α₂) → β₂) b) ↔ r₂ a b
inl :
  ∀ (val : α₁),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          b) ↔
      Sum.Lex r₁ r₂ (Sum.inl val) b
inr :
  ∀ (val : α₂),
    Sum.Lex s₁ s₂
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inr val))
        (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
              ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
            (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          b) ↔
      Sum.Lex r₁ r₂ (Sum.inr val) b
⊢ Sum.Lex s₁ s₂
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        a)
      (((mk (r := r₁) (s := s₁) f @hf).toEquiv (r := r₁) (s := s₁).sumCongr
            ((mk (r := r₂) (s := s₂) g @hg).toEquiv (r := r₂) (s := s₂)) :
          (a : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        b) ↔
    Sum.Lex r₁ r₂ a b

Tactic:
cases a