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 : HeytingAlgebra α
inst_2 : HeytingAlgebra β
inst_3 : HeytingAlgebra γ
inst_4 : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
a b : α
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) (a ⇨ b))
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) a ⇨
      Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) b)

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
inst_2 : HeytingAlgebra γ
f : HeytingHom β γ
g : HeytingHom α β
⊢ 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.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
inst_2 : HeytingAlgebra γ
f : HeytingHom β γ
g : HeytingHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
ext fun _ => rfl

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

Tactic:
ext fun _ => rfl

Premises used: HeytingHom.ext, rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
inst_2 : HeytingAlgebra γ
f : HeytingHom α β
g₁ g₂ : HeytingHom β γ
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, congr_arg (fun a ↦ comp a f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, DFunLike.ext_iff, congr_arg, HeytingHom.comp, Iff.intro, HeytingHom.ext, Iff.mp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : HeytingAlgebra α
inst_1 : HeytingAlgebra β
inst_2 : HeytingAlgebra γ
f₁ f₂ : HeytingHom α β
g : HeytingHom β γ
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: HeytingHom.comp_apply
-- 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 α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f g : CoheytingHom α β
h : Eq (α := (a : α) → β) ((fun (f : CoheytingHom α β) ↦ f.toFun) f) ((fun (f : CoheytingHom α β) ↦ 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_sdiff' :
      ∀ (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 : CoheytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top',
            map_sdiff' := map_sdiff' })
        ((fun (f : CoheytingHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
        CoheytingHom α β } =
      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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
g : CoheytingHom α β
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_sdiff' :
  ∀ (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 : CoheytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' })
    ((fun (f : CoheytingHom α β) ↦ 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_sdiff'_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 : CoheytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top',
            map_sdiff' := map_sdiff' })
        ((fun (f : CoheytingHom α β) ↦ f.toFun)
          { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
            map_sdiff' := map_sdiff'_1 })),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
        CoheytingHom α β } =
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
        map_sdiff' := map_sdiff'_1 }
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
      CoheytingHom α β } =
    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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
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_sdiff' :
  ∀ (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_top'_1 : { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1 : LatticeHom α β }.toFun ⊤ = ⊤
map_sdiff'_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 : CoheytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' })
    ((fun (f : CoheytingHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
        map_sdiff' := map_sdiff'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_top' := map_top', map_sdiff' := map_sdiff' :
      CoheytingHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_top' := map_top'_1,
      map_sdiff' := map_sdiff'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
f : CoheytingHom α β
⊢ 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 : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
f g : CoheytingHom α β
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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom α β
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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom α β
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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f' ⊤ = ⊤

Tactic:
simpa only [h] using map_top f

Premises used: TopHomClass.map_top
-- 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 α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
simpa only [h] using map_sdiff f

Premises used: CoheytingHomClass.map_sdiff
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
f : CoheytingHom α β
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 : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
f : CoheytingHom α β
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 : CoheytingAlgebra α
⊢ Eq (α := (a : α) → α) (⇑(CoheytingHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a : α
⊢ (CoheytingHom.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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) ⊤) ⊤

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 : CoheytingAlgebra α
inst_2 : CoheytingAlgebra β
inst_3 : CoheytingAlgebra γ
inst_4 : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
a b : α
⊢ Eq.{u_4 + 1} (α := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) (a \ b))
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) a \
      Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β) b)

Tactic:
simp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f : CoheytingHom β γ
g : CoheytingHom α β
⊢ 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.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f : CoheytingHom β γ
g : CoheytingHom α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
ext fun _ => rfl

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

Tactic:
ext fun _ => rfl

Premises used: CoheytingHom.ext, rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f : CoheytingHom α β
g₁ g₂ : CoheytingHom β γ
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, congr_arg (fun a ↦ comp a f)⟩

Premises used: Iff.mpr, Function.Surjective.forall, CoheytingHom.comp, CoheytingHom.ext, DFunLike.ext_iff, congr_arg, Iff.intro, Iff.mp
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CoheytingAlgebra α
inst_1 : CoheytingAlgebra β
inst_2 : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
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: CoheytingHom.comp_apply
-- 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 α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
f g : BiheytingHom α β
h : Eq (α := (a : α) → β) ((fun (f : BiheytingHom α β) ↦ f.toFun) f) ((fun (f : BiheytingHom α β) ↦ 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_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)
    (map_sdiff' :
      ∀ (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 : BiheytingHom α β) ↦ f.toFun)
          { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp',
            map_sdiff' := map_sdiff' })
        ((fun (f : BiheytingHom α β) ↦ f.toFun) g)),
    { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
        BiheytingHom α β } =
      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 : BiheytingAlgebra α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
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_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
map_sdiff' :
  ∀ (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_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
map_sdiff'_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 : BiheytingHom α β) ↦ f.toFun)
      { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' })
    ((fun (f : BiheytingHom α β) ↦ f.toFun)
      { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_himp' := map_himp'_1,
        map_sdiff' := map_sdiff'_1 })
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_himp' := map_himp', map_sdiff' := map_sdiff' :
      BiheytingHom α β } =
    { toFun := toFun_1, map_sup' := map_sup'_1, map_inf' := map_inf'_1, map_himp' := map_himp'_1,
      map_sdiff' := map_sdiff'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Heyting.Hom
Goal:
α : Type u_2
β : Type u_3
inst : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
f : BiheytingHom α β
⊢ 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 : BiheytingAlgebra α
inst_1 : BiheytingAlgebra β
f g : BiheytingHom α β
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 : BiheytingAlgebra α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
f : BiheytingHom α β
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 : BiheytingAlgebra α
inst_2 : BiheytingAlgebra β
inst_3 : BiheytingAlgebra γ
inst_4 : BiheytingAlgebra δ
f : BiheytingHom α β
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