awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.BoundedLattice
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 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedLatticeHomClass F α β
⊢ BoundedOrderHomClass F α β

Tactic:
{ show OrderHomClass F α β from inferInstance, ‹BoundedLatticeHomClass F α β› with }

Premises used: inferInstance, BoundedOrderHomClass.mk, BoundedLatticeHomClass.map_top, BoundedLatticeHomClass.map_bot
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
inst_3 : SemilatticeSup β
inst_4 : OrderBot β
inst_5 : OrderIsoClass F α β
⊢ SupBotHomClass F α β

Tactic:
{ OrderIsoClass.toSupHomClass, OrderIsoClass.toBotHomClass with }

Premises used: OrderIsoClass.toSupHomClass, OrderIsoClass.toBotHomClass, BotHomClass.map_bot, SupBotHomClass.mk
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : Lattice α
inst_2 : Lattice β
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : OrderIsoClass F α β
⊢ BoundedLatticeHomClass F α β

Tactic:
{ OrderIsoClass.toLatticeHomClass, OrderIsoClass.toBoundedOrderHomClass with }

Premises used: BoundedOrderHomClass.map_top, BoundedOrderHomClass.map_bot, OrderIsoClass.toLatticeHomClass, BoundedLatticeHomClass.mk, OrderIsoClass.toBoundedOrderHomClass
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : BotHomClass F α β
inst_6 : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) b : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) (⊥ : β)
rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) ⊥ ⊥
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

Premises used: disjoint_iff, BotHomClass.map_bot, InfHomClass.map_inf, Disjoint.eq_bot
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : FunLike F α β
inst_3 : BoundedOrder α
inst_4 : BoundedOrder β
inst_5 : BoundedLatticeHomClass F α β
a b : α
f : F
h : IsCompl a b
⊢ IsCompl.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
⟨h.1.map _, h.2.map _⟩

Premises used: Codisjoint.map, Disjoint.map, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)

Tactic:
(isCompl_compl.map _).compl_eq.symm

Premises used: IsCompl.compl_eq, IsCompl.map, isCompl_compl, Eq.symm
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⊓ bᶜ) : β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β)
    ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
    ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)

Tactic:
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

Premises used: map_compl', sdiff_eq, InfHomClass.map_inf
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : FunLike F α β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) ⊔ (f : (a : α) → β) (b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) (b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)

Tactic:
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

Premises used: SupHomClass.map_sup, map_sdiff', symmDiff
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : Max β
inst_4 : Bot β
inst_5 : Max γ
inst_6 : Bot γ
inst_7 : Max δ
inst_8 : Bot δ
f g : SupBotHom α β
h : Eq (α := (a : α) → β) ((fun (f : SupBotHom α β) ↦ f.toFun) f) ((fun (f : SupBotHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b)
    (map_bot' : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
        ((fun (f : SupBotHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : Max β
inst_4 : Bot β
inst_5 : Max γ
inst_6 : Bot γ
inst_7 : Max δ
inst_8 : Bot δ
g : SupBotHom α β
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_bot' : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
    ((fun (f : SupBotHom α β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b)
    (map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
        ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : Max β
inst_4 : Bot β
inst_5 : Max γ
inst_6 : Bot γ
inst_7 : Max δ
inst_8 : Bot δ
toFun : α → β
map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b
map_bot' : { toFun := toFun, map_sup' := map_sup' : SupHom α β }.toFun ⊥ = ⊥
toFun_1 : α → β
map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b
map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1 : SupHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' })
    ((fun (f : SupBotHom α β) ↦ f.toFun) { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_bot' := map_bot' : SupBotHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_bot' := map_bot'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toSupHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toBotHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupHom α β
hf : f.toFun ⊥ = ⊥
⊢ Eq (α := (a : α) → β) (⇑{ toSupHom := f, map_bot' := hf : SupBotHom α β } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f g : SupBotHom α β
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.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Max α
inst_1 : Bot α
⊢ Eq (α := (a : α) → α) (⇑(SupBotHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
inst : Max α
inst_1 : Bot α
a : α
⊢ (SupBotHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
f : SupBotHom β γ
g : SupBotHom α β
⊢ 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.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
f : SupBotHom β γ
g : SupBotHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
inst_6 : Max δ
inst_7 : Bot δ
f : SupBotHom γ δ
g : SupBotHom β γ
h : SupBotHom α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: SupBotHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
⊢ f.comp (SupBotHom.id α) = f

Tactic:
rfl

Premises used: SupBotHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
f : SupBotHom α β
⊢ comp (SupBotHom.id β) f = f

Tactic:
rfl

Premises used: SupBotHom.comp, SupHom.comp, rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g₁ g₂ : SupBotHom β γ
f : SupBotHom α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

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

Premises used: Iff.mpr, SupBotHom.comp, Function.Surjective.forall, SupBotHom.ext, DFunLike.ext_iff, Iff.intro, Iff.mp, rfl, congr_arg₂
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Max α
inst_1 : Bot α
inst_2 : Max β
inst_3 : Bot β
inst_4 : Max γ
inst_5 : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
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 [← comp_apply, h, comp_apply]

Premises used: SupBotHom.comp_apply
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
f g : SupBotHom α β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
⊢ Eq (α := (a : α) → β) (⇑⊥ : (a : α) → β) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
f g : SupBotHom α β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Bot α
inst_2 : SemilatticeSup β
inst_3 : OrderBot β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((⊥ : (a : α) → β) a : β) (⊥ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Max α
inst_2 : Bot α
inst_3 : SemilatticeSup β
inst_4 : OrderBot β
P : β → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this_1 : OrderBot { x : β // P x } := Subtype.orderBot (p := P) Pbot
this : SemilatticeSup { x : β // P x } := Subtype.semilatticeSup (P := P) Psup
⊢ (SupHom.subtypeVal (P := P) Psup).toFun ⊥ = ⊥

Tactic:
simp [Subtype.coe_bot Pbot]

Premises used: Subtype.coe_bot
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
β : Type u_3
inst : SemilatticeSup β
inst_1 : OrderBot β
P : β → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
x : { x : β // P x }
⊢ (subtypeVal (P := P) Pbot Psup : (a : { x : β // P x }) → β) x = (↑x : β)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
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 δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
f g : BoundedLatticeHom α β
h :
  Eq (α := (a : α) → β) ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) f) ((fun (f : BoundedLatticeHom α β) ↦ 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)
    (map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤)
    (map_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
        ((fun (f : BoundedLatticeHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
        BoundedLatticeHom α β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
-- Module: Mathlib.Order.Hom.BoundedLattice
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 δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
g : BoundedLatticeHom α β
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
map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedLatticeHom α β) ↦ 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)
    (map_top'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊤ = ⊤)
    (map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊥ = ⊥)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
        ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
            map_bot' := map_bot'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
        BoundedLatticeHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
        map_bot' := map_bot'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
      BoundedLatticeHom α β } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
-- Module: Mathlib.Order.Hom.BoundedLattice
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 δ
inst_5 : BoundedOrder α
inst_6 : BoundedOrder β
inst_7 : BoundedOrder γ
inst_8 : BoundedOrder δ
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
map_top' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊤ = ⊤
map_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥
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
map_top'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊤ = ⊤
map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊥ = ⊥
h :
  Eq (α := (a : α) → β)
    ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' })
    ((fun (f : BoundedLatticeHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
        map_bot' := map_bot'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_bot' := map_bot' :
      BoundedLatticeHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toLatticeHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toSupBotHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toBoundedOrderHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : LatticeHom α β
hf : f.toFun ⊤ = ⊤
hf' : f.toFun ⊥ = ⊥
⊢ Eq (α := (a : α) → β) (⇑{ toLatticeHom := f, map_top' := hf, map_bot' := hf' : BoundedLatticeHom α β } : (a : α) → β)
    (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f g : BoundedLatticeHom α β
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.BoundedLattice
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : BoundedLatticeHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl