awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
s : Set α
hs : s = (↑L : Set α)
⊢ (↑(L.copy s hs) : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
s : Set α
hs : s = (↑L : Set α)
⊢ L.copy s hs = L

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
⊢ (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M

Tactic:
SetLike.ext

Premises used: SetLike.ext
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq.{u_2 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq.{u_2 + 1} (α := α) (↑⊤ : α) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : ↥L
⊢ (↑(a ⊔ b) : α) = (↑a : α) ⊔ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : ↥L
⊢ (↑(a ⊓ b) : α) = (↑a : α) ⊓ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : ↥L
⊢ (↑aᶜ : α) = (↑a : α)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : ↥L
⊢ (↑(a \ b) : α) = (↑a : α) \ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : ↥L
⊢ (↑(a ⇨ b) : α) = (↑a : α) ⇨ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq.{u_2 + 1} (α := ↥L) (Subtype.mk (p := fun (x : α) ↦ x ∈ L) ⊥ ⋯) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq.{u_2 + 1} (α := ↥L) (Subtype.mk (p := fun (x : α) ↦ x ∈ L) ⊤ ⋯) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha ⊔ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a ⊔ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha ⊓ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a ⊓ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : a ∈ L
⊢ (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha)ᶜ = Subtype.mk (p := fun (x : α) ↦ x ∈ L) aᶜ ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha \ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a \ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha ⇨ Subtype.mk (p := fun (x : α) ↦ x ∈ L) b hb =
    Subtype.mk (p := fun (x : α) ↦ x ∈ L) (a ⇨ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq (α := (a : ↥L) → α) (⇑L.subtype : (a : ↥L) → α) (Subtype.val (p := fun (x : α) ↦ x ∈ L))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : ↥L
⊢ (L.subtype : (a : ↥L) → α) a = (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Injective (α := ↥L) (β := α) (⇑L.subtype : (a : ↥L) → α)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
h : L ≤ M
⊢ (⇑(inclusion h) : (a : ↥L) → ↥M) = Set.inclusion (s := (↑L : Set α)) (t := (↑M : Set α)) h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
h : L ≤ M
a : ↥L
⊢ (inclusion h : (a : ↥L) → ↥M) a = Set.inclusion (s := (↑L : Set α)) (t := (↑M : Set α)) h a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
h : L ≤ M
⊢ Injective (α := ↥L) (β := ↥M) (⇑(inclusion h) : (a : ↥L) → ↥M)

Tactic:
Set.inclusion_injective h

Premises used: Set.inclusion_injective
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ Eq.{u_2 + 1} (α := BoundedLatticeHom ↥L ↥L) (inclusion ⋯) (BoundedLatticeHom.id ↥L)

Tactic:
rfl

Premises used: BoundedLatticeHom.id, LatticeHom.id, BooleanSubalgebra.inclusion, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
h : L ≤ M
⊢ M.subtype.comp (inclusion h) = L.subtype

Tactic:
rfl

Premises used: Set.Mem, BooleanSubalgebra.subtype, LatticeHom.comp, SupHom.comp, BoundedLatticeHom.comp, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b x : α
⊢ Membership.mem (γ := Set α) {⊥, ⊤} x →
    ∀ ⦃b : α⦄, Membership.mem (γ := Set α) {⊥, ⊤} b → Membership.mem (γ := Set α) {⊥, ⊤} (x ⊔ b)

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b x : α
⊢ Membership.mem (γ := Set α) {⊥, ⊤} x →
    ∀ ⦃b : α⦄, Membership.mem (γ := Set α) {⊥, ⊤} b → Membership.mem (γ := Set α) {⊥, ⊤} (x ⊓ b)

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
⊢ ∀ {a : α}, Membership.mem (γ := Set α) {⊥, ⊤} a → Membership.mem (γ := Set α) {⊥, ⊤} aᶜ

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
⊢ Membership.mem (γ := Set α) {⊥, ⊤} ⊥

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
⊢ (↑⊥ : Set α) = {⊥, ⊤}

Tactic:
rfl

Premises used: Set.insert, setOf, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
⊢ (↑(L ⊓ M) : Set α) = (↑L : Set α) ∩ (↑M : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
S : Set (BooleanSubalgebra α)
⊢ (↑(sInf S) : Set α) = ⋂ L ∈ S, (↑L : Set α)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
inst : BooleanAlgebra α
f : ι → BooleanSubalgebra α
⊢ (↑(⨅ (i : ι), f i) : Set α) = ⋂ (i : ι), (↑(f i) : Set α)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
rw₁ rw₂ : L = ⊤ ↔ L = ⊤
⊢ (↑L : Set α) = univ ↔ L = ⊤

Tactic:
rw [← coe_top, coe_inj]

Premises used: BooleanSubalgebra.coe_top, BooleanSubalgebra.coe_inj
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Membership.mem (γ := BooleanSubalgebra α) ⊥ a ↔ a = ⊥ ∨ a = ⊤

Tactic:
.rfl

Premises used: Set.insert, Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ Membership.mem (γ := BooleanSubalgebra α) ⊤ a

Tactic:
mem_univ _

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
a : α
⊢ a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
S : Set (BooleanSubalgebra α)
⊢ a ∈ (↑(sInf S) : Set α) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
inst : BooleanAlgebra α
a : α
f : ι → BooleanSubalgebra α
⊢ a ∈ (↑(⨅ (i : ι), f i) : Set α) ↔ ∀ (i : ι), a ∈ f i

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
_S : BooleanSubalgebra α
_a : α
⊢ Membership.mem (γ := BooleanSubalgebra α) ⊥ _a → _a ∈ _S

Tactic:
aesop
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
inst_3 : IsEmpty α
⊢ Subsingleton.{u_2 + 1} (BooleanSubalgebra α)

Tactic:
SetLike.coe_injective.subsingleton

Premises used: Function.Injective.subsingleton, SetLike.coe_injective
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f_1 : BoundedLatticeHom α β
s t : Set α
a b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ ∀ {a : α},
    Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (↑L : Set β)) a →
      Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (↑L : Set β)) aᶜ

Tactic:
simp [map_compl']

Premises used: map_compl'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f_1 : BoundedLatticeHom α β
s t : Set α
a b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (↑L : Set β)) ⊥

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra β
f : BoundedLatticeHom α β
⊢ (↑(comap f L) : Set α) = (⇑f : (a : α) → β) ⁻¹' (↑L : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
a : α
L : BooleanSubalgebra β
⊢ a ∈ comap f L ↔ Membership.mem (α := β) L ((f : (a : α) → β) a : β)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
⊢ Monotone (comap f)

Tactic:
fun _ _ ↦ preimage_mono

Premises used: Set.Mem, Monotone, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ comap (BoundedLatticeHom.id α) L = L

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, BooleanSubalgebra.comap, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L : BooleanSubalgebra γ
g : BoundedLatticeHom β γ
f : BoundedLatticeHom α β
⊢ comap f (comap g L) = comap (g.comp f) L

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, BoundedLatticeHom.comp, BooleanSubalgebra.comap, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f_1 : BoundedLatticeHom α β
s t : Set α
a_1 b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ (↑L : Set α)
⊢ aᶜ ∈ (↑L : Set α) ∧ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) aᶜ : β) (((f : (a : α) → β) a)ᶜ : β)

Tactic:
simpa [map_compl']

Premises used: map_compl'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f_1 : BoundedLatticeHom α β
s t : Set α
a_1 b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
a : α
ha : a ∈ (↑L : Set α)
⊢ Membership.mem.{u_3, u_3} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (((f : (a : α) → β) a)ᶜ : β)

Tactic:
exact ⟨aᶜ, by simpa [map_compl']⟩
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f_1 : BoundedLatticeHom α β
s t : Set α
a b : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ ⊥ ∈ (↑L : Set α) ∧ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
L : BooleanSubalgebra α
⊢ (↑(map f L) : Set β) = (⇑f : (a : α) → β) '' (↑L : Set α)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : BoundedLatticeHom α β
b : β
⊢ b ∈ map f L ↔ ∃ a ∈ L, (f : (a : α) → β) a = b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : BoundedLatticeHom α β
a : α
⊢ a ∈ L → Membership.mem (α := β) (map f L) ((f : (a : α) → β) a : β)

Tactic:
mem_image_of_mem f

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : BoundedLatticeHom α β
a : ↥L
⊢ Membership.mem (α := β) (map f L) ((f : (a : α) → β) (↑a : α) : β)

Tactic:
mem_map_of_mem f a.prop

Premises used: BooleanSubalgebra.mem_map_of_mem, Subtype.prop
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
⊢ Monotone (map f)

Tactic:
fun _ _ ↦ image_mono

Premises used: Set.Mem, Set.image_mono, Monotone, setOf, Set.Subset, Set.image
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ map (BoundedLatticeHom.id α) L = L

Tactic:
SetLike.coe_injective <| image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L : BooleanSubalgebra α
g : BoundedLatticeHom β γ
f : BoundedLatticeHom α β
⊢ map g (map f L) = map (g.comp f) L

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : α ≃o β
a : β
⊢ Membership.mem (γ := BooleanSubalgebra β)
      (map
        (let __src : LatticeHom α β := { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L)
      a ↔
    Membership.mem (α := α) L ((f.symm : (a : β) → α) a : α)

Tactic:
Set.mem_image_equiv

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : BoundedLatticeHom α β
a : α
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Membership.mem (α := β) (map f L) ((f : (a : α) → β) a : β) ↔ a ∈ L

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : α ≃o β
L : BooleanSubalgebra α
⊢ Eq.{u_3 + 1} (α := BooleanSubalgebra β)
    (map
      (let __src : LatticeHom α β := { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := (⇑f : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L)
    (comap
      (let __src : LatticeHom β α := { toFun := (⇑f.symm : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := (⇑f.symm : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L)

Tactic:
SetLike.coe_injective <| f.toEquiv.image_eq_preimage_symm L

Premises used: SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe, RelIso.toEquiv
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : β ≃o α
L : BooleanSubalgebra α
⊢ Eq.{u_3 + 1} (α := BooleanSubalgebra β)
    (comap
      (let __src : LatticeHom β α := { toFun := (⇑f : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := (⇑f : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L)
    (map
      (let __src : LatticeHom α β := { toFun := (⇑f.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := (⇑f.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L)

Tactic:
(map_equiv_eq_comap_symm f.symm L).symm

Premises used: BooleanSubalgebra.map_equiv_eq_comap_symm, OrderIso.symm, Eq.symm
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
simp_rw :
  (↑(map
            { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ :
              BoundedLatticeHom α β }
            L) :
        Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) =
      (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M) : Set α)
⊢ map
        (let __src : LatticeHom α β := { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      map
        (let __src : LatticeHom β α := { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M

Tactic:
simp_rw [← coe_inj]

Premises used: BooleanSubalgebra.coe_inj
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ (↑(map
            { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ :
              BoundedLatticeHom α β }
            L) :
        Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) =
      (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M) : Set α)

Tactic:
(Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Premises used: setOf, Equiv.eq_image_iff_symm_image_eq, Set.image, Iff.symm
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ (↑(map
            { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ :
              BoundedLatticeHom α β }
            L) :
        Set β) =
      (↑M : Set β) ↔
    (↑L : Set α) =
      (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M) : Set α)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Premises used: Equiv.eq_image_iff_symm_image_eq, Iff.symm
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
f : BoundedLatticeHom α β
M : BooleanSubalgebra β
⊢ map f L ≤ M ↔ L ≤ comap f M

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: BooleanSubalgebra.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: GaloisConnection.l_bot, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
L M : BooleanSubalgebra α
⊢ map f (L ⊔ M) = map f L ⊔ map f M

Tactic:
(gc_map_comap f).l_sup

Premises used: GaloisConnection.l_sup, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
L : ι → BooleanSubalgebra α
⊢ map f (⨆ (i : ι), L i) = ⨆ (i : ι), map f (L i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: GaloisConnection.l_iSup, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: GaloisConnection.u_top, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra β
f : BoundedLatticeHom α β
⊢ comap f (L ⊓ M) = comap f L ⊓ comap f M

Tactic:
(gc_map_comap f).u_inf

Premises used: GaloisConnection.u_inf, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
L : ι → BooleanSubalgebra β
⊢ comap f (⨅ (i : ι), L i) = ⨅ (i : ι), comap f (L i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: GaloisConnection.u_iInf, BooleanSubalgebra.gc_map_comap
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
⊢ map f (L ⊓ M) ≤ map f L ⊓ map f M

Tactic:
map_mono.map_inf_le _ _

Premises used: Set.Mem, BooleanSubalgebra.map_mono, Monotone.map_inf_le