awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ (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
have 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) sorry)
            ((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)) sorry :
                  { f : r ↪r s // Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) }))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₁
⊢ (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₁
have 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 : β₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₂
⊢ (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₂
have 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 : β₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₁
⊢ (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₁
have 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 : β₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₂
⊢ (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₂
have 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 : β₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₁
⊢ (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₁
have 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 : β₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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₂
⊢ (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₂
have 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 : β₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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 : α₁ ⊕ α₂
⊢ 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
have 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
Tactic: obtain ⟨f, hf⟩ := e₁
Cleared hypotheses: e₁
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨g, hg⟩ := e₂
Cleared hypotheses: e₂
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
⊢ 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
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
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
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
have inl : ∀ (val_1 : α₁),
  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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inl val_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
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
val : α₁
inl :
  ∀ (val_1 : α₁),
    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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inl val_1)
⊢ 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
have inl₁ : ∀ (val_1 : α₂),
  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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val) (Sum.inr val_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
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
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
have inr : ∀ (val_1 : α₁),
  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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inl val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inl val_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.RelIso.Basic (goal)
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
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
val : α₂
inr :
  ∀ (val_1 : α₁),
    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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
          (Sum.inl val_1)) ↔
      Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inl val_1)
⊢ 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
have inr₁ : ∀ (val_1 : α₂),
  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 : α₁ ⊕ α₂) → β₁ ⊕ β₂)
        (Sum.inr val_1)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val) (Sum.inr val_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.RelIso.Set (goal)
Goal:
α : Type u_1
β : Type u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → x = y
have rw : ¬Subrel r p x y → ¬Subrel r p y x → (↑x : α) = (↑y : α)
Tactic: rw [Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Order.RelIso.Set (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' t) ((⇑(e.symm (r := r) (s := s)) : (a : β) → α) '' t)
have rw : Eq.{u_1 + 1} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' t)
  ((⇑(e.symm (r := r) (s := s).symm (r := s) (s := r)) : (a : α) → β) ⁻¹' t)
Tactic: rw [e.symm.image_eq_preimage_symm]