awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b
have rw : Codisjoint (a ⊔ b) (￢(a ⊔ b))
Tactic: rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff,
    codisjoint_left_comm, codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b
have a₁ : ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
a₁ : ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b
have a₂ : ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
have a₁ : ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
Tactic: refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
have a₁ : ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b
Tactic: rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ←
      hnot_le_iff_codisjoint_right]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
α : Type u_2
inst : CoheytingAlgebra α
a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
have a₁ : ￢￢a ≤ ￢￢(b ⊔ a \ b)
Tactic: rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CoheytingAlgebra α
a_1 b_1 : α
a b c : αᵒᵈ
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ a ⊓ b ≤ c
have rw : a ≤ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) c \ (ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ⊓ a ≤ c
Tactic: rw [inf_comm]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c
have pos : ∀ (h : b ≤ c), a ≤ ⊤ ↔ min a b ≤ c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
pos : ∀ (h : b ≤ c), a ≤ ⊤ ↔ min a b ≤ c
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c
have neg : ∀ (h : ¬b ≤ c), a ≤ c ↔ min a b ≤ c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c
have neg : a ≤ c ↔ a ≤ c ∨ b ≤ c
Tactic: rw [inf_le_iff, or_iff_left h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬b ≤ c
neg : a ≤ c ↔ a ≤ c ∨ b ≤ c
⊢ a ≤ c ↔ min a b ≤ c
have neg₁ : a ≤ c ↔ a ≤ c
Tactic: rw [inf_le_iff, or_iff_left h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ max b c
have pos : ∀ (h : a ≤ b), ⊥ ≤ c ↔ a ≤ max b c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
pos : ∀ (h : a ≤ b), ⊥ ≤ c ↔ a ≤ max b c
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ max b c
have neg : ∀ (h : ¬a ≤ b), a ≤ c ↔ a ≤ max b c
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c
have neg : a ≤ c ↔ a ≤ b ∨ a ≤ c
Tactic: rw [le_sup_iff, or_iff_right h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : BoundedOrder α
a b c : α
h : ¬a ≤ b
neg : a ≤ c ↔ a ≤ b ∨ a ≤ c
⊢ a ≤ c ↔ a ≤ max b c
have neg₁ : a ≤ c ↔ a ≤ c
Tactic: rw [le_sup_iff, or_iff_right h]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ a ≤ ⊤
have rw : f a ≤ ⊤
Tactic: rw [← le, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
Tactic: rw [← le, ← le, map_himp, map_inf, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw₁ : f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
Tactic: rw [← le, ← le, map_himp, map_inf, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
rw₁ : f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw₂ : f a ≤ f b ⇨ f c ↔ f (a ⊓ b) ≤ f c
Tactic: rw [← le, ← le, map_himp, map_inf, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
rw₁ : f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
rw₂ : f a ≤ f b ⇨ f c ↔ f (a ⊓ b) ≤ f c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw₃ : f a ≤ f b ⇨ f c ↔ f a ⊓ f b ≤ f c
Tactic: rw [← le, ← le, map_himp, map_inf, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : HImp α
inst_6 : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b c : α
rw : f a ≤ f (b ⇨ c) ↔ a ⊓ b ≤ c
rw₁ : f a ≤ f (b ⇨ c) ↔ f (a ⊓ b) ≤ f c
rw₂ : f a ≤ f b ⇨ f c ↔ f (a ⊓ b) ≤ f c
rw₃ : f a ≤ f b ⇨ f c ↔ f a ⊓ f b ≤ f c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw₄ : f a ⊓ f b ≤ f c ↔ f a ⊓ f b ≤ f c
Tactic: rw [← le, ← le, map_himp, map_inf, le_himp_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ a
have rw : ⊥ ≤ f a
Tactic: rw [← le, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
have rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
Tactic: rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
have rw₁ : f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
Tactic: rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
rw₁ : f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
have rw₂ : f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)
Tactic: rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
rw₁ : f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
rw₂ : f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
have rw₃ : f a \ f b ≤ f c ↔ f a ≤ f b ⊔ f c
Tactic: rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Bot α
inst_5 : SDiff α
inst_6 : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
rw : f (a \ b) ≤ f c ↔ a ≤ b ⊔ c
rw₁ : f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)
rw₂ : f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)
rw₃ : f a \ f b ≤ f c ↔ f a ≤ f b ⊔ f c
⊢ a \ b ≤ c ↔ a ≤ b ⊔ c
have rw₄ : f a ≤ f b ⊔ f c ↔ f a ≤ f b ⊔ f c
Tactic: rw [← le, ← le, map_sdiff, map_sup, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊥ ≤ a
have rw : ⊥ ≤ f a
Tactic: rw [← le, map_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f (a ⇨ ⊥) = f aᶜ
have rw : f a ⇨ f ⊥ = f aᶜ
Tactic: rw [map_himp, map_compl, map_bot, himp_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⇨ f ⊥ = f aᶜ
⊢ f (a ⇨ ⊥) = f aᶜ
have rw₁ : f a ⇨ f ⊥ = (f a)ᶜ
Tactic: rw [map_himp, map_compl, map_bot, himp_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⇨ f ⊥ = f aᶜ
rw₁ : f a ⇨ f ⊥ = (f a)ᶜ
⊢ f (a ⇨ ⊥) = f aᶜ
have rw₂ : f a ⇨ ⊥ = (f a)ᶜ
Tactic: rw [map_himp, map_compl, map_bot, himp_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : Compl α
inst_7 : HImp α
inst_8 : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
rw : f a ⇨ f ⊥ = f aᶜ
rw₁ : f a ⇨ f ⊥ = (f a)ᶜ
rw₂ : f a ⇨ ⊥ = (f a)ᶜ
⊢ f (a ⇨ ⊥) = f aᶜ
have rw₃ : (f a)ᶜ = (f a)ᶜ
Tactic: rw [map_himp, map_compl, map_bot, himp_bot]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : HNot α
inst_7 : SDiff α
inst_8 : CoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ a ≤ ⊤
have rw : f a ≤ ⊤
Tactic: rw [← le, map_top]
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : HNot α
inst_7 : SDiff α
inst_8 : CoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ f (⊤ \ a) = f (￢a)
have rw : f ⊤ \ f a = f (￢a)
Tactic: rw [map_sdiff, map_hnot, map_top, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : HNot α
inst_7 : SDiff α
inst_8 : CoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
rw : f ⊤ \ f a = f (￢a)
⊢ f (⊤ \ a) = f (￢a)
have rw₁ : f ⊤ \ f a = ￢f a
Tactic: rw [map_sdiff, map_hnot, map_top, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : HNot α
inst_7 : SDiff α
inst_8 : CoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
rw : f ⊤ \ f a = f (￢a)
rw₁ : f ⊤ \ f a = ￢f a
⊢ f (⊤ \ a) = f (￢a)
have rw₂ : ⊤ \ f a = ￢f a
Tactic: rw [map_sdiff, map_hnot, map_top, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : Top α
inst_5 : Bot α
inst_6 : HNot α
inst_7 : SDiff α
inst_8 : CoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
rw : f ⊤ \ f a = f (￢a)
rw₁ : f ⊤ \ f a = ￢f a
rw₂ : ⊤ \ f a = ￢f a
⊢ f (⊤ \ a) = f (￢a)
have rw₃ : ￢f a = ￢f a
Tactic: rw [map_sdiff, map_hnot, map_top, top_sdiff']
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
⊢ GeneralizedHeytingAlgebra α
have le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ GeneralizedHeytingAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
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
⊢ GeneralizedHeytingAlgebra α
have map_sup : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
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 : β)
⊢ GeneralizedHeytingAlgebra α
have map_inf : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
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 : β)
⊢ GeneralizedHeytingAlgebra α
have map_top : Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
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 : α) → β) ⊤ : β) (⊤ : β)
⊢ GeneralizedHeytingAlgebra α
have map_himp : ∀ (a b : α), Eq.{u_3 + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.generalizedHeytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
⊢ GeneralizedCoheytingAlgebra α
have le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.generalizedCoheytingAlgebra
-- Lean 4 proof step from Mathlib.Order.Heyting.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
le : ∀ {x y : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ GeneralizedCoheytingAlgebra α
have lt : ∀ {x y : α}, LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.generalizedCoheytingAlgebra