awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_hnot : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
map_himp :
  ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ BiheytingAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.biheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
⊢ Eq.{u_1 + 1} (α := α) (∂ ⊤) ⊥
have rw : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ￢⊤) ⊥
Tactic: rw [boundary, hnot_top, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ￢⊤) ⊥
⊢ Eq.{u_1 + 1} (α := α) (∂ ⊤) ⊥
have rw₁ : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ⊥) ⊥
Tactic: rw [boundary, hnot_top, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
rw : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ￢⊤) ⊥
rw₁ : Eq.{u_1 + 1} (α := α) (⊤ ⊓ ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := α) (∂ ⊤) ⊥
have rw₂ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
Tactic: rw [boundary, hnot_top, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ∂ (￢￢a) = ∂ (￢a)
have simp_rw : ￢￢a ⊓ ￢￢￢a = ￢a ⊓ ￢￢a
Tactic: simp_rw [boundary, hnot_hnot_hnot, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
simp_rw : ￢￢a ⊓ ￢￢￢a = ￢a ⊓ ￢￢a
⊢ ∂ (￢￢a) = ∂ (￢a)
have simp_rw₁ : ￢￢a ⊓ ￢a = ￢a ⊓ ￢￢a
Tactic: simp_rw [boundary, hnot_hnot_hnot, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ￢∂ a = ⊤
have rw : ￢(a ⊓ ￢a) = ⊤
Tactic: rw [boundary, hnot_inf_distrib, sup_hnot_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢(a ⊓ ￢a) = ⊤
⊢ ￢∂ a = ⊤
have rw₁ : ￢a ⊔ ￢￢a = ⊤
Tactic: rw [boundary, hnot_inf_distrib, sup_hnot_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢(a ⊓ ￢a) = ⊤
rw₁ : ￢a ⊔ ￢￢a = ⊤
⊢ ￢∂ a = ⊤
have rw₂ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [boundary, hnot_inf_distrib, sup_hnot_self]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b
have unfold : a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
Tactic: unfold boundary
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
have rw : a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
Tactic: rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
have rw₁ : a ⊓ b ⊓ ￢a ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
Tactic: rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₁ : a ⊓ b ⊓ ￢a ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
have rw₂ : a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
Tactic: rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
rw : a ⊓ b ⊓ (￢a ⊔ ￢b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₁ : a ⊓ b ⊓ ￢a ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
rw₂ : a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
have rw₃ : a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b
Tactic: rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b
have rw : a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
Tactic: rw [boundary, inf_sup_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
have simp : ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
  a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Tactic: simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc,
    sup_comm _ a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_3 : a ⊓ ￢a ≤ a ⊔ b
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
refine_3 : a ⊓ ￢a ≤ a ⊔ b
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_4 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
refine_3 : a ⊓ ￢a ≤ a ⊔ b
refine_4 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_5 : a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
refine_1 : a ⊓ ￢a ≤ a ⊔ (a ⊔ b)
refine_2 : a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)
refine_3 : a ⊓ ￢a ≤ a ⊔ b
refine_4 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
refine_5 : a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_6 : a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Tactic: refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
have refine_4 : ￢a ≤ ￢(a ⊔ b) ⊔ b
Tactic: refine inf_le_of_right_le ?_
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_6 : ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Tactic: refine inf_le_of_right_le ?_
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b
have refine_4 : Codisjoint (￢(a ⊔ b)) (a ⊔ b)
Tactic: rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
have refine_6 : ￢a ≤ ￢(a ⊓ b)
Tactic: refine le_sup_of_le_right ?_
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)
have refine_6 : Codisjoint a (￢(a ⊓ b))
Tactic: rw [hnot_le_iff_codisjoint_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
have rw : ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
Tactic: rw [sup_comm a, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ∂ ∂ a = ∂ a
have rw : ∂ a ⊓ ￢∂ a = ∂ a
Tactic: rw [boundary, hnot_boundary, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ∂ a ⊓ ￢∂ a = ∂ a
⊢ ∂ ∂ a = ∂ a
have rw₁ : ∂ a ⊓ ⊤ = ∂ a
Tactic: rw [boundary, hnot_boundary, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ∂ a ⊓ ￢∂ a = ∂ a
rw₁ : ∂ a ⊓ ⊤ = ∂ a
⊢ ∂ ∂ a = ∂ a
have rw₂ : ∂ a = ∂ a
Tactic: rw [boundary, hnot_boundary, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a
have rw : ￢￢a ≤ a
Tactic: rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ a \ ∂ a = ￢￢a
have rw : (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
Tactic: rw (occs := [1]) [← hnot_hnot_sup_boundary a]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw₂ : ￢￢a \ ∂ a = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
rw₂ : ￢￢a \ ∂ a = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw₃ : ￢∂ a \ ￢a = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
rw₂ : ￢￢a \ ∂ a = ￢￢a
rw₃ : ￢∂ a \ ￢a = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw₄ : ⊤ \ ￢a = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
rw : ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
rw₁ : ￢￢a \ ∂ a ⊔ ⊥ = ￢￢a
rw₂ : ￢￢a \ ∂ a = ￢￢a
rw₃ : ￢∂ a \ ￢a = ￢￢a
rw₄ : ⊤ \ ￢a = ￢￢a
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
have rw₅ : ￢￢a = ￢￢a
Tactic: rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ ∂ a = a
have rw : a ⊓ ￢a = a
Tactic: rw [boundary, h, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
h : ￢a = ⊤
rw : a ⊓ ￢a = a
⊢ ∂ a = a
have rw₁ : a ⊓ ⊤ = a
Tactic: rw [boundary, h, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Heyting.Boundary (goal)
Goal:
α : Type u_1
inst : CoheytingAlgebra α
a : α
h : ￢a = ⊤
rw : a ⊓ ￢a = a
rw₁ : a ⊓ ⊤ = a
⊢ ∂ a = a
have rw₂ : a = a
Tactic: rw [boundary, h, inf_top_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 : HeytingAlgebra α
x : HeytingAlgebra β
inst_2 : HeytingHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 α
x : HeytingAlgebra β
inst_2 : HeytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 α
x : HeytingAlgebra β
inst_2 : HeytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₂ : β
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 α
x : HeytingAlgebra β
inst_2 : HeytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
rw₂ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 α
x : CoheytingAlgebra β
inst_2 : CoheytingHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, 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 : CoheytingAlgebra α
x : CoheytingAlgebra β
inst_2 : CoheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, 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 : 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 : α) → β) ⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₂ : β
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, 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 : 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₂ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, 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 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.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 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) (⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊤ \ ⊤) : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.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 : 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 : α) → β) ⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₂ : β
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.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 : 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₂ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) ⊤ \ (f : (a : α) → β) ⊤ : β)
Tactic: rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.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 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 : BiheytingAlgebra α
x : BiheytingAlgebra β
inst_2 : BiheytingHomClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) (⊤ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (⊥ ⇨ ⊥) : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 : 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 : α) → β) ⊥ : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₂ : β
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 : 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₂ : β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊤ : β) (⊤ : β)
have rw₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β) ((f : (a : α) → β) ⊥ ⇨ (f : (a : α) → β) ⊥ : β)
Tactic: rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
-- 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 : HeytingAlgebra α
x : HeytingAlgebra β
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 : HeytingAlgebra α
x : HeytingAlgebra β
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 : CoheytingAlgebra α
x : CoheytingAlgebra β
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 : CoheytingAlgebra α
x : CoheytingAlgebra β
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]