awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ Eq (α := (a : α) → β)
    ((fun (f : α →o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (p : γ →o δ) ↦ (OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)) : α →o β))
        ((fun (p : α →o β) ↦ (OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)) : γ →o δ)) p)))
    ((fun (f : α →o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) p)
have change : Eq (α := α → β)
  (Function.comp (β := β)
    (Function.comp.{u_7 + 1, u_9 + 1, u_7 + 1} (β := δ) (⇑g.symm : (a : δ) → β) (⇑g : (a : β) → δ))
    (Function.comp (β := α) (⇑p : (a : α) → β)
      (Function.comp.{u_6 + 1, u_8 + 1, u_6 + 1} (β := γ) (⇑f.symm : (a : γ) → α) (⇑f : (a : α) → γ))))
  (⇑p : (a : α) → β)
Tactic: change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ Eq (α := (a : γ) → δ)
    ((fun (f : γ →o δ) ↦ ((⇑f : (a : γ) → δ) : (a : γ) → δ))
      ((fun (p : α →o β) ↦ (OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)) : γ →o δ))
        ((fun (p : γ →o δ) ↦ (OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)) : α →o β)) p)))
    ((fun (f : γ →o δ) ↦ ((⇑f : (a : γ) → δ) : (a : γ) → δ)) p)
have change : Eq (α := γ → δ)
  (Function.comp (β := δ)
    (Function.comp.{u_9 + 1, u_7 + 1, u_9 + 1} (β := β) (⇑g : (a : β) → δ) (⇑g.symm : (a : δ) → β))
    (Function.comp (β := γ) (⇑p : (a : γ) → δ)
      (Function.comp.{u_8 + 1, u_6 + 1, u_8 + 1} (β := α) (⇑f : (a : α) → γ) (⇑f.symm : (a : γ) → α))))
  (⇑p : (a : γ) → δ)
Tactic: change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ LE.le (α := γ →o δ)
      (({ toFun := fun (p : α →o β) ↦ OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)),
              invFun := fun (p : γ →o δ) ↦ OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : α →o β) → γ →o δ)
          p :
        γ →o δ)
      (({ toFun := fun (p : α →o β) ↦ OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)),
              invFun := fun (p : γ →o δ) ↦ OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : α →o β) → γ →o δ)
          q :
        γ →o δ) ↔
    p ≤ q
have simp : (∀ (x : γ),
    LE.le.{u_7} (α := β) ((p : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)
      ((q : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)) ↔
  ∀ (x : α), LE.le.{u_7} (α := β) ((p : (a : α) → β) x : β) ((q : (a : α) → β) x : β)
Tactic: simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
x : α
y : β
⊢ x < (e.symm : (a : β) → α) y ↔ (e : (a : α) → β) x < y
have rw : LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) ((e.symm : (a : β) → α) y : α) : β) ↔
  (e : (a : α) → β) x < y
Tactic: rw [← e.lt_iff_lt, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
x : α
y : β
rw :
  LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) ((e.symm : (a : β) → α) y : α) : β) ↔
    (e : (a : α) → β) x < y
⊢ x < (e.symm : (a : β) → α) y ↔ (e : (a : α) → β) x < y
have rw₁ : (e : (a : α) → β) x < y ↔ (e : (a : α) → β) x < y
Tactic: rw [← e.lt_iff_lt, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT e.toRelIsoLT = e
have h : ∀ (x : α), Eq.{u_7 + 1} (α := β) ((ofRelIsoLT e.toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
⊢ (ofRelIsoLT e).toRelIsoLT = e
have h : ∀ (x : α), Eq.{u_7 + 1} (α := β) (((ofRelIsoLT e).toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a : α
⊢ a = g (f a)
have rw : cmp a (g (f a)) = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a : α
rw : cmp a (g (f a)) = Ordering.eq
⊢ a = g (f a)
have rw₁ : cmp (f a) (f a) = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a : α
rw : cmp a (g (f a)) = Ordering.eq
rw₁ : cmp (f a) (f a) = Ordering.eq
⊢ a = g (f a)
have rw₂ : Ordering.eq = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x : β
⊢ f (g x) = x
have rw : cmp (f (g x)) x = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x : β
rw : cmp (f (g x)) x = Ordering.eq
⊢ f (g x) = x
have rw₁ : cmp (g x) (g x) = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x : β
rw : cmp (f (g x)) x = Ordering.eq
rw₁ : cmp (g x) (g x) = Ordering.eq
⊢ f (g x) = x
have rw₂ : Ordering.eq = Ordering.eq
Tactic: rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ LE.le.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a : β)
      (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b : β) ↔
    a ≤ b
have h₁ : cmp.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := sorry, right_inv := sorry : α ≃ β } : (a : α) → β) a : β)
    (({ toFun := f, invFun := g, left_inv := sorry, right_inv := sorry : α ≃ β } : (a : α) → β) b : β) =
  cmp a b
Tactic: apply le_iff_le_of_cmp_eq_cmp
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ cmp.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a : β)
      (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b : β) =
    cmp a b
have h₁ : b = g (f b)
Tactic: convert! (h a (f b)).symm
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ (f : (a : α) → β) x = y
have refine : (f : (a : α) → β) x ≤ y
Tactic: refine le_antisymm ?_ (hy _)
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ (f : (a : α) → β) x ≤ y
have rw : x ≤ (f.symm : (a : β) → α) y
Tactic: rw [← f.apply_symm_apply y, f.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β)
have refine : LE.le.{u_3} (α := β) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β)
  ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β)
Tactic: refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
⊢ LE.le.{u_3} (α := β) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β)
    ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β)
have apply : LE.le.{u_2} (α := α)
  ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β) : α)
  ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β) : α)
Tactic: apply f.symm.le_iff_le.1
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β) ↔ IsMax x
have refine : IsMax x → IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)
Tactic: refine ⟨f.strictMono.isMax_of_apply, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
| IsMax x
have rw : IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α)
Tactic: rw [← f.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ IsMax x → IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)
have conv_lhs : IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α) →
  IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)
Tactic: conv_lhs => rw [← f.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : SemilatticeInf β
inst_3 : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) ((f : (a : α) → β) ⊥ : β)
Tactic: rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderTop α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) (a ⊔ b) : β)
Tactic: rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
⊢ ∃ (b : β), IsCompl x b
have obtain : ∀ (y : α) (hy : IsCompl ((f.symm : (a : β) → α) x) y), ∃ (b : β), IsCompl x b
Tactic: obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl ((f.symm : (a : β) → α) x) y
⊢ ∃ (b : β), IsCompl x b
have hy₁ : IsCompl.{u_2} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) ((f : (a : α) → β) y : β) : α)
Tactic: rw [← f.symm_apply_apply y] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
inst : LinearOrder X
inst_1 : DenselyOrdered X
inst_2 : Preorder Y
f : X → Y
hf : StrictMono f
⊢ DenselyOrdered.{u_7} (↑(Set.range f) : Type u_7)
have dense : ∀ (a₁ a₂ : (↑(Set.range f) : Type u_7)), a₁ < a₂ → ∃ (a : (↑(Set.range f) : Type u_7)), a₁ < a ∧ a < a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered X ↔ DenselyOrdered Y
have mp : DenselyOrdered X → DenselyOrdered Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
mp : DenselyOrdered X → DenselyOrdered Y
⊢ DenselyOrdered X ↔ DenselyOrdered Y
have mpr : DenselyOrdered Y → DenselyOrdered X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y
have mp : ∀ (a b : Y) (h : a < b), ∃ (a_1 : Y), a < a_1 ∧ a_1 < b
Tactic: refine ⟨fun a b h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
⊢ ∃ (a_1 : Y), a < a_1 ∧ a_1 < b
have mp : ∀ (c : X) (hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b), ∃ (a_1 : Y), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X
have mpr : ∀ (a b : X) (h : a < b), ∃ (a_1 : X), a < a_1 ∧ a_1 < b
Tactic: refine ⟨fun a b h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
⊢ ∃ (a_1 : X), a < a_1 ∧ a_1 < b
have mpr : ∀ (c : Y) (hc : (f : (a : X) → Y) a < c ∧ c < (f : (a : X) → Y) b), ∃ (a_1 : X), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
⊢ DenselyOrdered X ↔ DenselyOrdered Y
have rw : DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y
Tactic: rw [← denselyOrdered_orderDual]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
refine_2 : DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y
⊢ DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y
have refine_1 : ∀ {a b : Xᵒᵈ},
  LE.le.{u_7} (α := Y) ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) a : Y)
      ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) b : Y) ↔
    a ≤ b
Tactic: let e : Xᵒᵈ ≃o Y := ⟨OrderDual.ofDual.trans (f : X ≃ Y), ?_⟩
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
⊢ ∀ {a b : Xᵒᵈ},
    LE.le.{u_7} (α := Y) ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) a : Y)
        ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) b : Y) ↔
      a ≤ b
have refine_1 : ∀ (a a_1 : X), LE.le.{u_7} (α := Y) ((f : (a : X) → Y) a : Y) ((f : (a : X) → Y) a_1 : Y) ↔ a_1 ≤ a
Tactic: simp only [Equiv.trans_apply, EquivLike.coe_coe, OrderDual.forall, OrderDual.ofDual_toDual,
      OrderDual.toDual_le_toDual]
-- Lean 4 proof step from Mathlib.Order.Hom.Basic (goal)
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
a b : X
⊢ LE.le.{u_7} (α := Y) ((f : (a : X) → Y) a : Y) ((f : (a : X) → Y) b : Y) ↔ b ≤ a
have refine_1 : b ≤ a ↔ b ≤ a
Tactic: rw [hf.le_iff_ge]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : LE α
inst_2 : OrderTop α
inst_3 : PartialOrder β
inst_4 : OrderTop β
inst_5 : OrderIsoClass F α β
f : F
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (⊤ : β) ↔ a = ⊤
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) ⊤ : β) ↔ a = ⊤
Tactic: rw [← map_top f, (EquivLike.injective f).eq_iff]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : LE α
inst_2 : OrderTop α
inst_3 : PartialOrder β
inst_4 : OrderTop β
inst_5 : OrderIsoClass F α β
f : F
a : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) ⊤ : β) ↔ a = ⊤
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) (⊤ : β) ↔ a = ⊤
have rw₁ : a = ⊤ ↔ a = ⊤
Tactic: rw [← map_top f, (EquivLike.injective f).eq_iff]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → β) (map_top' : toFun ⊤ = ⊤) (h : { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun = g.toFun),
  { toFun := toFun, map_top' := map_top' : TopHom α β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
g : TopHom α β
toFun : α → β
map_top' : toFun ⊤ = ⊤
h : { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun = g.toFun
⊢ { toFun := toFun, map_top' := map_top' : TopHom α β } = g
have mk : ∀ (toFun_1 : α → β) (map_top'_1 : toFun_1 ⊤ = ⊤)
  (h :
    { toFun := toFun, map_top' := map_top' : TopHom α β }.toFun =
      { toFun := toFun_1, map_top' := map_top'_1 : TopHom α β }.toFun),
  { toFun := toFun, map_top' := map_top' : TopHom α β } = { toFun := toFun_1, map_top' := map_top'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f : TopHom β γ
g : TopHom α β
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊤) ⊤
have rw : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) ⊤ : β) : γ) (⊤ : γ)
Tactic: rw [comp_apply, map_top, map_top]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f : TopHom β γ
g : TopHom α β
rw : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) ⊤ : β) : γ) (⊤ : γ)
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊤) ⊤
have rw₁ : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ⊤ : γ) (⊤ : γ)
Tactic: rw [comp_apply, map_top, map_top]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Top α
inst_2 : Top β
inst_3 : Top γ
inst_4 : Top δ
f : TopHom β γ
g : TopHom α β
rw : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) ⊤ : β) : γ) (⊤ : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) ⊤ : γ) (⊤ : γ)
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊤) ⊤
have rw₂ : Eq.{u_4 + 1} (α := γ) ⊤ ⊤
Tactic: rw [comp_apply, map_top, map_top]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← TopHom.comp_apply, h, TopHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← TopHom.comp_apply, h, TopHom.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Bounded (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Top α
inst_1 : Top β
inst_2 : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← TopHom.comp_apply, h, TopHom.comp_apply]