awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))

Tactic:
exact ((map_sSup _).trans iSup_image).ge

Premises used: Eq.ge, iSup_image, Eq.trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
rw : f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f a ⊔ f i
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
rw [← le, ← sInf_image, map_sup, map_sInf s, minAx.sup_iInf₂_eq]

Premises used: sInf_image, Order.Coframe.MinimalAxioms.sup_iInf₂_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
simp_rw : f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f (a ⊔ i)
⊢ f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f a ⊔ f i

Tactic:
simp_rw [← map_sup]
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f (a ⊔ i)

Tactic:
((map_sInf _).trans iInf_image).le

Premises used: Eq.le, iInf_image, Eq.trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Coframe.MinimalAxioms β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ f (sInf (max a '' s)) ≤ ⨅ i ∈ s, f (a ⊔ i)

Tactic:
exact ((map_sInf _).trans iInf_image).le

Premises used: Eq.le, iInf_image, Eq.trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : Compl α
inst_9 : HImp α
inst_10 : HNot α
inst_11 : SDiff α
inst_12 : CompletelyDistribLattice β
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_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι_1 : Type u
κ_1 : ι_1 → Type u
g : (a : ι_1) → κ_1 a → α
simp_rw :
  f (sInf (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b)) =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₁ :
  ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ ⨆ (b : κ_1 a), g a b) a), f a =
    f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₂ :
  ⨅ (i : ι_1), f (⨆ (b : κ_1 i), g i b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), sInf (range fun (a : ι_1) ↦ g a (g_1 a)))
simp_rw₃ :
  ⨅ (i : ι_1), f (sSup (range fun (b : κ_1 i) ↦ g i b)) =
    f (sSup (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))))
simp_rw₄ :
  Eq.{v + 1} (α := β)
    (⨅ (i : ι_1), ⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (b : κ_1 i) ↦ g i b) a), f a)
    (⨆ (a : α),
      ⨆ (_ :
        Membership.mem (γ := Set α) (range fun (g_1 : (a : ι_1) → κ_1 a) ↦ sInf (range fun (a : ι_1) ↦ g a (g_1 a))) a),
        f a)
simp_rw₅ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), f (sInf (range fun (a : ι_1) ↦ g a (i a))))
simp_rw₆ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), ⨅ (a : α), ⨅ (_ : Membership.mem (γ := Set α) (range fun (a : ι_1) ↦ g a (i a)) a), f a)
simp_rw₇ :
  Eq.{v + 1} (α := β) (⨅ (i : ι_1), ⨆ (i_1 : κ_1 i), f (g i i_1))
    (⨆ (i : (a : ι_1) → κ_1 a), ⨅ (i_1 : ι_1), f (g i_1 (i i_1)))
⊢ f (⨅ (a : ι_1), ⨆ (b : κ_1 a), g a b) = f (⨆ (g_1 : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), g a (g_1 a))

Tactic:
simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]

Premises used: iInf, iSup, iInf_range, iSup_range, iInf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ Frame α

Tactic:
apply e.injective.frame

Premises used: Function.Injective.frame, Equiv.injective
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
s : Set α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Frame β
completeLattice : CompleteLattice α := e.completeLattice
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
map_sdiff :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
⊢ Coframe α

Tactic:
apply e.injective.coframe

Premises used: Function.Injective.coframe, Equiv.injective
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
x y : α
⊢ LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a b : α
⊢ Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply