awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : CoheytingAlgebra α
x : CoheytingAlgebra β
inst_2 : CoheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₂ : β
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₄ : β
rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₆ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
rw [← @sdiff_self α _ ⊤, ← sdiff_self, map_sdiff]

Premises used: sdiff_self, CoheytingHomClass.map_sdiff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₂ : β
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₄ : β
rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
rw₆ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.map_sdiff]

Premises used: BiheytingHomClass.map_sdiff, sdiff_self
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₂ : β
rw₃ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₄ : β
rw₅ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₆ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Premises used: himp_self, BiheytingHomClass.map_himp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : HeytingAlgebra α
x : HeytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
simp : EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
⊢ c ≤ (f : (a : α) → β) (a ⇨ b) ↔ c ≤ (f : (a : α) → β) a ⇨ (f : (a : α) → β) b

Tactic:
simp only [← map_inv_le_iff, le_himp_iff]

Premises used: map_inv_le_iff, le_himp_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : HeytingAlgebra α
x : HeytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
rw :
  LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f c ⊓ a) : β) ((f : (a : α) → β) b : β) ↔
    EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Premises used: OrderIsoClass.map_le_map_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : HeytingAlgebra α
x : HeytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f c ⊓ a) : β) ((f : (a : α) → β) b : β) ↔
    EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : CoheytingAlgebra α
x : CoheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
simp :
  a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)
⊢ (f : (a : α) → β) (a \ b) ≤ c ↔ (f : (a : α) → β) a \ (f : (a : α) → β) b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]

Premises used: sdiff_le_iff, le_map_inv_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : CoheytingAlgebra α
x : CoheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
rw :
  LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (b ⊔ EquivLike.inv f c) : β) ↔
    a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Premises used: OrderIsoClass.map_le_map_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : CoheytingAlgebra α
x : CoheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (b ⊔ EquivLike.inv f c) : β) ↔
    a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
simp : EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
⊢ c ≤ (f : (a : α) → β) (a ⇨ b) ↔ c ≤ (f : (a : α) → β) a ⇨ (f : (a : α) → β) b

Tactic:
simp only [← map_inv_le_iff, le_himp_iff]

Premises used: map_inv_le_iff, le_himp_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
rw :
  LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f c ⊓ a) : β) ((f : (a : α) → β) b : β) ↔
    EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Premises used: OrderIsoClass.map_le_map_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f c ⊓ a) : β) ((f : (a : α) → β) b : β) ↔
    EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
simp :
  a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)
⊢ (f : (a : α) → β) (a \ b) ≤ c ↔ (f : (a : α) → β) a \ (f : (a : α) → β) b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]

Premises used: sdiff_le_iff, le_map_inv_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
rw :
  LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (b ⊔ EquivLike.inv f c) : β) ↔
    a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)

Tactic:
rw [← OrderIsoClass.map_le_map_iff f]

Premises used: OrderIsoClass.map_le_map_iff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : EquivLike F α β
inst_1 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (b ⊔ EquivLike.inv f c) : β) ↔
    a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BooleanAlgebra α
inst_2 : BooleanAlgebra β
inst_3 : BoundedLatticeHomClass F α β
f : F
a b : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (b ⊔ aᶜ) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (b ⊔ aᶜ) : β) ((f : (a : α) → β) b ⊔ ((f : (a : α) → β) a)ᶜ : β)
rw₂ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β)
    ((f : (a : α) → β) b ⊔ ((f : (a : α) → β) a)ᶜ : β)
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β)
    ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ b) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)

Tactic:
rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]

Premises used: himp_eq, IsCompl.compl_eq, IsCompl.map, SupHomClass.map_sup, isCompl_compl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : BooleanAlgebra α
inst_2 : BooleanAlgebra β
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, (isCompl_compl.map _).compl_eq]

Premises used: sdiff_eq, IsCompl.compl_eq, IsCompl.map, InfHomClass.map_inf, isCompl_compl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingHomClass F α β
f : F
a : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ ⊥) : β) (((f : (a : α) → β) a)ᶜ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ ⊥) : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⇨ ⊥ : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)

Tactic:
rw [← himp_bot, ← himp_bot, map_himp, map_bot]

Premises used: HeytingHomClass.map_himp, himp_bot, BotHomClass.map_bot
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingHomClass F α β
f : F
a b : α
simp_rw :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((b ⇨ a) ⊓ (a ⇨ b)) : β)
    (((f : (a : α) → β) b ⇨ (f : (a : α) → β) a) ⊓ ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b) : β)
simp_rw₁ :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (b ⇨ a) ⊓ (f : (a : α) → β) (a ⇨ b) : β)
    (((f : (a : α) → β) b ⇨ (f : (a : α) → β) a) ⊓ ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇔ b) : β) ((f : (a : α) → β) a ⇔ (f : (a : α) → β) b : β)

Tactic:
simp_rw [bihimp, map_inf, map_himp]

Premises used: HeytingHomClass.map_himp, bihimp, InfHomClass.map_inf
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingHomClass F α β
f : F
a : α
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ a) : β) (￢(f : (a : α) → β) a : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ a) : β) (⊤ \ (f : (a : α) → β) a : β)
rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) a : β) (⊤ \ (f : (a : α) → β) a : β)
rw₃ rw₄ : Eq.{u_3 + 1} (α := β) (⊤ \ (f : (a : α) → β) a : β) (⊤ \ (f : (a : α) → β) a : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (￢a) : β) (￢(f : (a : α) → β) a : β)

Tactic:
rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]

Premises used: CoheytingHomClass.map_sdiff, TopHomClass.map_top, top_sdiff'
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingHomClass F α β
f : F
a b : α
simp_rw :
  Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
    ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
simp_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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)

Tactic:
simp_rw [symmDiff, map_sup, map_sdiff]

Premises used: CoheytingHomClass.map_sdiff, SupHomClass.map_sup, symmDiff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f g : HeytingHom α β
h : Eq (α := (a : α) → β) ((fun (f : HeytingHom α β) ↦ f.toFun) f) ((fun (f : HeytingHom α β) ↦ 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_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥)
    (map_himp' :
      ∀ (a b : α),
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a ⇨ b) =
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a ⇨
            { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : HeytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' })
        ((fun (f : HeytingHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' :
        HeytingHom α β } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
g : HeytingHom α β
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_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥
map_himp' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a ⇨ b) =
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a ⇨
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : HeytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' })
    ((fun (f : HeytingHom α β) ↦ 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_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊥ = ⊥)
    (map_himp'_1 :
      ∀ (a b : α),
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun (a ⇨ b) =
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun a ⇨
            { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : HeytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' })
        ((fun (f : HeytingHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_bot' := map_bot'_1,
            map_himp' := map_himp'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' :
        HeytingHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_bot' := map_bot'_1,
        map_himp' := map_himp'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' :
      HeytingHom α β } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
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_bot' : { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun ⊥ = ⊥
map_himp' :
  ∀ (a b : α),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun (a ⇨ b) =
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.toFun a ⇨
        { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf' : LatticeHom α β }.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
map_bot'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊥ = ⊥
map_himp'_1 :
  ∀ (a b : α),
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun (a ⇨ b) =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun a ⇨
        { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun b
h :
  Eq (α := (a : α) → β)
    ((fun (f : HeytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' })
    ((fun (f : HeytingHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_bot' := map_bot'_1,
        map_himp' := map_himp'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' :
      HeytingHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_bot' := map_bot'_1,
      map_himp' := map_himp'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
f : HeytingHom α β
⊢ Eq (α := (a : α) → β) (⇑f.toLatticeHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
f g : HeytingHom α β
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.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa only [h] using map_sup f

Premises used: SupHomClass.map_sup
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa only [h] using map_inf f

Premises used: InfHomClass.map_inf
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f' ⊥ = ⊥

Tactic:
simpa only [h] using map_bot f

Premises used: BotHomClass.map_bot
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
simpa only [h] using map_himp f

Premises used: HeytingHomClass.map_himp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
f : HeytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊥) ⊥

Tactic:
simp