awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β
⊢ c ≤ (f : (a : α) → β) (a ⇨ b) ↔ c ≤ (f : (a : α) → β) a ⇨ (f : (a : α) → β) b
have simp : EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
Tactic: simp only [← map_inv_le_iff, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
have rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) (EquivLike.inv f c ⊓ a) : β) ((f : (a : α) → β) b : β) ↔
  EquivLike.inv f (c ⊓ (f : (a : α) → β) a) ≤ b
Tactic: rw [← OrderIsoClass.map_le_map_iff f]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β
⊢ (f : (a : α) → β) (a \ b) ≤ c ↔ (f : (a : α) → β) a \ (f : (a : α) → β) b ≤ c
have simp : 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 only [← le_map_inv_iff, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) f ((f : (a : α) → β) b ⊔ c : β)
have 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 : β)
Tactic: rw [← OrderIsoClass.map_le_map_iff f]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ b) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (b ⊔ aᶜ) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
Tactic: rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ b) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (b ⊔ aᶜ) : β) ((f : (a : α) → β) b ⊔ ((f : (a : α) → β) a)ᶜ : β)
Tactic: rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ b) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β)
  ((f : (a : α) → β) b ⊔ ((f : (a : α) → β) a)ᶜ : β)
Tactic: rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ b) : β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β) ((f : (a : α) → β) b ⊔ (f : (a : α) → β) aᶜ : β)
Tactic: rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw : 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]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β)
  ((f : (a : α) → β) a ⊓ ((f : (a : α) → β) b)ᶜ : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b) : β) ((f : (a : α) → β) a \ (f : (a : α) → β) b : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β) ((f : (a : α) → β) a ⊓ (f : (a : α) → β) bᶜ : β)
Tactic: rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ ⊥) : β) (((f : (a : α) → β) a)ᶜ : β)
Tactic: rw [← himp_bot, ← himp_bot, map_himp, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)ᶜ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇨ ⊥) : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
Tactic: rw [← himp_bot, ← himp_bot, map_himp, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 ⇨ ⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
Tactic: rw [← himp_bot, ← himp_bot, map_himp, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 ⇨ ⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a ⇨ ⊥ : β) ((f : (a : α) → β) a ⇨ ⊥ : β)
Tactic: rw [← himp_bot, ← himp_bot, map_himp, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇔ b) : β) ((f : (a : α) → β) a ⇔ (f : (a : α) → β) b : β)
have simp_rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ((b ⇨ a) ⊓ (a ⇨ b)) : β)
  (((f : (a : α) → β) b ⇨ (f : (a : α) → β) a) ⊓ ((f : (a : α) → β) a ⇨ (f : (a : α) → β) b) : β)
Tactic: simp_rw [bihimp, map_inf, map_himp]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ⇔ b) : β) ((f : (a : α) → β) a ⇔ (f : (a : α) → β) b : β)
have 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) : β)
Tactic: simp_rw [bihimp, map_inf, map_himp]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (￢a) : β) (￢(f : (a : α) → β) a : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ a) : β) (￢(f : (a : α) → β) a : β)
Tactic: rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (￢a) : β) (￢(f : (a : α) → β) a : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ a) : β) (⊤ \ (f : (a : α) → β) a : β)
Tactic: rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (￢a) : β) (￢(f : (a : α) → β) a : β)
have rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) a : β) (⊤ \ (f : (a : α) → β) a : β)
Tactic: rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (￢a) : β) (￢(f : (a : α) → β) a : β)
have rw₃ : Eq.{u_3 + 1} (α := β) (⊤ \ (f : (a : α) → β) a : β) (⊤ \ (f : (a : α) → β) a : β)
Tactic: rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have simp_rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a \ b ⊔ b \ a) : β)
  ((f : (a : α) → β) a \ (f : (a : α) → β) b ⊔ (f : (a : α) → β) b \ (f : (a : α) → β) a : β)
Tactic: simp_rw [symmDiff, map_sup, map_sdiff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (a ∆ b) : β) ((f : (a : α) → β) a ∆ (f : (a : α) → β) b : β)
have 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 : β)
Tactic: simp_rw [symmDiff, map_sup, map_sdiff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)
⊢ { toFun := toFun, map_sup' := map_sup', map_inf' := map_inf', map_bot' := map_bot', map_himp' := map_himp' :
      HeytingHom α β } =
    g
have 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 }
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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 : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Heyting.Hom (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h