awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
inr : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
have inr₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inl : ∀ (h : a ≤ b), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
inl :
  ∀ (h : a ≤ b), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inr : ∀ (h : b ≤ a), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inl : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
Tactic: rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
inl : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inl₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inr : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
Tactic: rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lattice (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
inr : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β)
have inr₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
Tactic: rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ Ici x = {y : α | ¬y < x}
have h : ∀ (x_1 : α), x_1 ∈ Ici x ↔ Membership.mem (γ := Set α) {y : α | ¬y < x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y < x
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
have rw : y =
  (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
Tactic: rw [symm_apply_eq, sumLexIioIci_apply_inl]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y < x
rw :
  y =
    (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
have rw₁ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h) : α)
Tactic: rw [symm_apply_eq, sumLexIioIci_apply_inl]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x ≤ y
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
have rw : y =
  (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
Tactic: rw [symm_apply_eq, sumLexIioIci_apply_inr]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x ≤ y
rw :
  y =
    (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
have rw₁ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h) : α)
Tactic: rw [symm_apply_eq, sumLexIioIci_apply_inr]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ Iic x = {y : α | ¬x < y}
have h : ∀ (x_1 : α), x_1 ∈ Iic x ↔ Membership.mem (γ := Set α) {y : α | ¬x < y} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y ≤ x
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
have rw : y =
  (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
Tactic: rw [symm_apply_eq, sumLexIicIoi_apply_inl]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y ≤ x
rw :
  y =
    (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
have rw₁ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h) : α)
Tactic: rw [symm_apply_eq, sumLexIicIoi_apply_inl]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x < y
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
have rw : y =
  (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
Tactic: rw [symm_apply_eq, sumLexIicIoi_apply_inr]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x < y
rw :
  y =
    (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
have rw₁ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h) : α)
Tactic: rw [symm_apply_eq, sumLexIicIoi_apply_inr]
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (hypothesis)
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
a_1 b_1 : Lex (α × β)
a b : α × β
⊢ LE.le.{u_3} (α := β)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2,
              invFun := fun (x : β) ↦ (toLex : (a : α × β) → Lex (α × β)) (default, x), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → β)
          ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β)) :
        β)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2,
              invFun := fun (x : β) ↦ (toLex : (a : α × β) → Lex (α × β)) (default, x), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → β)
          ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β)) :
        β) ↔
    LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β))
have heq : a.1 = b.1
Tactic: have heq : a.1 = b.1 := Subsingleton.allEq _ _
-- Lean 4 proof step from Mathlib.Order.Hom.Lex (goal)
Goal:
α_1 : Type u_1
α_2 : Type u_2
β_1 : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    LE.le (α := Lex (α × Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.prodAssoc α β γ).trans (Equiv.trans ((Equiv.refl α).prodCongr toLex) toLex))) :
              (a : Lex (Lex (α × β) × γ)) → Lex (α × Lex (β × γ)))
            a :
          Lex (α × Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.prodAssoc α β γ).trans (Equiv.trans ((Equiv.refl α).prodCongr toLex) toLex))) :
              (a : Lex (Lex (α × β) × γ)) → Lex (α × Lex (β × γ)))
            b :
          Lex (α × Lex (β × γ))) ↔
      a ≤ b
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
      Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
⊢ Eq (α := (a : α) → β) (⇑(⨅ (i : ι), f i) : (a : α) → β) (⨅ (i : ι), (⇑(f i) : (a : α) → β))
have h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((⨅ (i : ι), f i : (a : α) → β) x : β) ((⨅ (i : ι), (⇑(f i) : (a : α) → β)) x : β)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
⊢ Eq (α := (a : α) → β) (⇑(⨆ (i : ι), f i) : (a : α) → β) (⨆ (i : ι), (⇑(f i) : (a : α) → β))
have h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((⨆ (i : ι), f i : (a : α) → β) x : β) ((⨆ (i : ι), (⇑(f i) : (a : α) → β)) x : β)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
have mp : (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
    (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) →
  ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
mp :
  (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
have mpr : (∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)) →
  ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
    (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁) ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
have rw : (⇑f : (a : α) → α)^[n.succ] a₁ ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
Tactic: rw [← Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f : (a : α) → α)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
have f₁ : (⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁) ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
Tactic: calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
⊢ ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
have zero : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[0] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[0] a₁ ⊔ a₂
Tactic: induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
zero : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[0] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[0] a₁ ⊔ a₂
⊢ ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
have succ : ∀ (n : ℕ) (ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂) (a₁ a₂ : α),
  (⇑f : (a : α) → α)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
Tactic: induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Hom.Order (hypothesis)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
have h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
Tactic: have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
      intro n
      induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂)) =
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
have rw : (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁)) =
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] a₂ ⊔ a₁) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)
have rw : (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Hom.Order (goal)
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
have f₁ : (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂)) =
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
Tactic: calc
      f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) :=
        Function.iterate_add_apply f n₁ n₂ _
      _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
      _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
      _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
      _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _