awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Lattice
Goal:
β : Type u_3
inst : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
⊢ Eq (α := (a : { x : β // P x }) → β) (⇑(subtypeVal (P := P) Psup) : (a : { x : β // P x }) → β)
    (Subtype.val (p := fun (x : β) ↦ P x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
f g : LatticeHom α β
h : Eq (α := (a : α) → β) ((fun (f : LatticeHom α β) ↦ f.toFun) f) ((fun (f : LatticeHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
    (map_inf' :
      ∀ (a b : α),
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
          { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
            { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
        ((fun (f : LatticeHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
g : LatticeHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_inf' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
    ((fun (f : LatticeHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
    (map_inf'_1 :
      ∀ (a b : α),
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun (a ⊓ b) =
          { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun a ⊓
            { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
        ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_inf' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun a ⊓
        { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun b
toFun_1 : α → β
map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b
map_inf'_1 :
  ∀ (a b : α),
    { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun (a ⊓ b) =
      { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun a ⊓
        { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' })
    ((fun (f : LatticeHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toSupHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : SupHom α β
hf : ∀ (a b : α), f.toFun (a ⊓ b) = f.toFun a ⊓ f.toFun b
⊢ Eq (α := (a : α) → β) (⇑{ toSupHom := f, map_inf' := hf : LatticeHom α β } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f g : LatticeHom α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Lattice α
⊢ Eq (α := (a : α) → α) (⇑(LatticeHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Lattice α
a : α
⊢ (LatticeHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ Eq (α := SupHom α γ)
    { toFun := Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β), map_sup' := ⋯ }
    (SupHom.comp.{u_2, u_3, u_4} (β := β) { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯ }
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯ })

Tactic:
rfl

Premises used: SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ Eq (α := SupHom α γ) { toFun := (⇑(f.comp g) : (a : α) → γ), map_sup' := ⋯ }
    (SupHom.comp.{u_2, u_3, u_4} (β := β) { toFun := (⇑f : (a : β) → γ), map_sup' := ⋯ }
      { toFun := (⇑g : (a : α) → β), map_sup' := ⋯ })

Tactic:
rfl

Premises used: SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
inst_3 : Lattice δ
f : LatticeHom γ δ
g : LatticeHom β γ
h : LatticeHom α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ f.comp (LatticeHom.id α) = f

Tactic:
LatticeHom.ext fun _ => rfl

Premises used: LatticeHom.ext, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ comp (LatticeHom.id β) f = f

Tactic:
LatticeHom.ext fun _ => rfl

Premises used: LatticeHom.ext, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g₁ g₂ : LatticeHom β γ
f : LatticeHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => LatticeHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun h => congr_arg₂ _ h rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, LatticeHom.ext, DFunLike.ext_iff, LatticeHom.comp, Iff.intro, Iff.mp, rfl, congr_arg₂
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
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 : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]

Premises used: LatticeHom.comp_apply
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : Lattice γ
inst_4 : Lattice δ
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this : Lattice { x : β // P x } := Subtype.lattice (P := P) Psup Pinf
⊢ ∀ (a b : { x : β // P x }),
    (SupHom.subtypeVal (P := P) Psup).toFun (a ⊓ b) =
      (SupHom.subtypeVal (P := P) Psup).toFun a ⊓ (SupHom.subtypeVal (P := P) Psup).toFun b

Tactic:
simp [Subtype.coe_inf Pinf]

Premises used: Subtype.coe_inf
-- Module: Mathlib.Order.Hom.Lattice
Goal:
β : Type u_3
inst : Lattice β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
x : { x : β // P x }
⊢ (subtypeVal (P := P) Psup Pinf : (a : { x : β // P x }) → β) x = (↑x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
β : Type u_3
inst : Lattice β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
⊢ Eq (α := (a : { x : β // P x }) → β) (⇑(subtypeVal (P := P) Psup Pinf) : (a : { x : β // P x }) → β)
    (Subtype.val (p := fun (x : β) ↦ P x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
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 : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
inr :
  ∀ (h : b ≤ a), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
obtain h | h := le_total a b

Premises used: le_total
-- Module: Mathlib.Order.Hom.Lattice
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 : α) → β) b : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)
inl₁ inl₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]

Premises used: Iff.mpr, OrderHomClass.mono, sup_eq_right
-- Module: Mathlib.Order.Hom.Lattice
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 : β)
inr₁ inr₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (max a b) : β) ((f : (a : α) → β) a ⊔ (f : (a : α) → β) b : β)

Tactic:
rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]

Premises used: Iff.mpr, sup_eq_left, OrderHomClass.mono
-- Module: Mathlib.Order.Hom.Lattice
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 : β)
inr :
  ∀ (h : b ≤ a), 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 : β)

Tactic:
obtain h | h := le_total a b

Premises used: le_total
-- Module: Mathlib.Order.Hom.Lattice
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 : β)
inl₁ inl₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min a b) : β) ((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)]

Premises used: Iff.mpr, OrderHomClass.mono, inf_eq_left
-- Module: Mathlib.Order.Hom.Lattice
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 : β)
inr₁ inr₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) b : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (min 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)]

Premises used: Iff.mpr, OrderHomClass.mono, inf_eq_right
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(toLatticeHom α β f) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : LinearOrder α
inst_2 : Lattice β
inst_3 : OrderHomClass F α β
f : F
a : α
⊢ Eq.{u_3 + 1} (α := β) ((toLatticeHom α β f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Max α
⊢ Eq (α := InfHom αᵒᵈ αᵒᵈ) ((SupHom.dual : (a : SupHom α α) → InfHom αᵒᵈ αᵒᵈ) (SupHom.id α) : InfHom αᵒᵈ αᵒᵈ)
    (InfHom.id αᵒᵈ : InfHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: InfHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Max β
inst_2 : Max γ
g : SupHom β γ
f : SupHom α β
⊢ Eq (α := InfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((SupHom.dual : (a : SupHom α γ) → InfHom αᵒᵈ γᵒᵈ) (g.comp f) : InfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (InfHom.comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((SupHom.dual : (a : SupHom β γ) → InfHom βᵒᵈ γᵒᵈ) g)
        ((SupHom.dual : (a : SupHom α β) → InfHom αᵒᵈ βᵒᵈ) f) :
      InfHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: InfHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Max α
⊢ Eq.{u_2 + 1} (α := SupHom α α)
    ((Equiv.symm SupHom.dual : (a : InfHom αᵒᵈ αᵒᵈ) → SupHom α α) (InfHom.id αᵒᵈ) : SupHom α α)
    (SupHom.id α : SupHom α α)

Tactic:
rfl

Premises used: SupHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Max β
inst_2 : Max γ
g : InfHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : InfHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := SupHom α γ) ((Equiv.symm SupHom.dual : (a : InfHom αᵒᵈ γᵒᵈ) → SupHom α γ) (g.comp f) : SupHom α γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm SupHom.dual : (a : InfHom βᵒᵈ γᵒᵈ) → SupHom β γ) g)
        ((Equiv.symm SupHom.dual : (a : InfHom αᵒᵈ βᵒᵈ) → SupHom α β) f) :
      SupHom α γ)

Tactic:
rfl

Premises used: SupHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Lattice α
⊢ Eq (α := LatticeHom αᵒᵈ αᵒᵈ)
    ((LatticeHom.dual : (a : LatticeHom α α) → LatticeHom αᵒᵈ αᵒᵈ) (LatticeHom.id α) : LatticeHom αᵒᵈ αᵒᵈ)
    (LatticeHom.id αᵒᵈ : LatticeHom αᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: LatticeHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom β γ
f : LatticeHom α β
⊢ Eq (α := LatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((LatticeHom.dual : (a : LatticeHom α γ) → LatticeHom αᵒᵈ γᵒᵈ) (g.comp f) : LatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((LatticeHom.dual : (a : LatticeHom β γ) → LatticeHom βᵒᵈ γᵒᵈ) g)
        ((LatticeHom.dual : (a : LatticeHom α β) → LatticeHom αᵒᵈ βᵒᵈ) f) :
      LatticeHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
inst : Lattice α
⊢ Eq.{u_2 + 1} (α := LatticeHom α α)
    ((Equiv.symm LatticeHom.dual : (a : LatticeHom αᵒᵈ αᵒᵈ) → LatticeHom α α) (LatticeHom.id αᵒᵈ) : LatticeHom α α)
    (LatticeHom.id α : LatticeHom α α)

Tactic:
rfl

Premises used: LatticeHom.id, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
g : LatticeHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : LatticeHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := LatticeHom α γ)
    ((Equiv.symm LatticeHom.dual : (a : LatticeHom αᵒᵈ γᵒᵈ) → LatticeHom α γ) (g.comp f) : LatticeHom α γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm LatticeHom.dual : (a : LatticeHom βᵒᵈ γᵒᵈ) → LatticeHom β γ) g)
        ((Equiv.symm LatticeHom.dual : (a : LatticeHom αᵒᵈ βᵒᵈ) → LatticeHom α β) f) :
      LatticeHom α γ)

Tactic:
rfl

Premises used: LatticeHom.comp, SupHom.comp, OrderDual, rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
⊢ Eq (α := (a : α × β) → α) (⇑fst : (a : α × β) → α) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
⊢ Eq (α := (a : α × β) → β) (⇑snd : (a : α × β) → β) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
x : α × β
⊢ (fst : (a : α × β) → α) x = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
x : α × β
⊢ (snd : (a : α × β) → β) x = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Lattice (α i)
i : ι
⊢ Eq (α := (a : (i : ι) → α i) → α i) (⇑(evalLatticeHom (α := α) i) : (a : (i : ι) → α i) → α i) (eval (β := α) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lattice
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Lattice (α i)
i : ι
f : (i : ι) → α i
⊢ (evalLatticeHom (α := α) i : (a : (i : ι) → α i) → α i) f = f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : r a x
b : α
hb : r b x
⊢ r
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) a ha)))
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // r x_1 x }) (β := { x_1 : α // ¬r x_1 x }) (Subrel r fun (x_1 : α) ↦ r x_1 x)
      (Subrel r fun (x_1 : α) ↦ ¬r x_1 x) (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) a ha))
      (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) b hb))

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) a ha)))
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // r x_1 x }) (β := { x_1 : α // ¬r x_1 x }) (Subrel r fun (x_1 : α) ↦ r x_1 x)
      (Subrel r fun (x_1 : α) ↦ ¬r x_1 x) (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) a ha))
      (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) b hb))

Tactic:
simpa using trans_trichotomous_right ha hb

Premises used: trans_trichotomous_right
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) a ha)))
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // r x_1 x }) (β := { x_1 : α // ¬r x_1 x }) (Subrel r fun (x_1 : α) ↦ r x_1 x)
      (Subrel r fun (x_1 : α) ↦ ¬r x_1 x) (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) a ha))
      (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ r x_1 x) b hb))

Tactic:
simpa using fun h ↦ ha <| trans h hb

Premises used: trans
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) a ha)))
      ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α)
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // r x_1 x }) (β := { x_1 : α // ¬r x_1 x }) (Subrel r fun (x_1 : α) ↦ r x_1 x)
      (Subrel r fun (x_1 : α) ↦ ¬r x_1 x) (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) a ha))
      (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x_1 x) b hb))

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }
⊢ Eq (α := α) ((sumLexComplLeft r x : (a : { x_1 : α // r x_1 x } ⊕ { x_1 : α // ¬r x_1 x }) → α) a : α)
    ((Equiv.sumCompl fun (x_1 : α) ↦ r x_1 x : (a : { a : α // r a x } ⊕ { a : α // ¬r a x }) → α) a : α)

Tactic:
rfl

Premises used: rfl, Sum.elim