awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
toSublattice_1 : Sublattice α
sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier
sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })
mk : toSublattice = toSublattice_1
⊢ { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } =
    { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 }

Tactic:
congr
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
toSublattice_1 : Sublattice α
sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier
sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })
⊢ toSublattice = toSublattice_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
toSublattice_1 : Sublattice α
sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier
sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })
⊢ toSublattice = toSublattice_1

Tactic:
exact SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ ⊤ ∈ L

Tactic:
simpa using L.sInfClosed' <| empty_subset _

Premises used: CompleteSublattice.sInfClosed', Set.empty_subset
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ ⊥ ∈ L

Tactic:
simpa using L.sSupClosed' <| empty_subset _

Premises used: CompleteSublattice.sSupClosed', Set.empty_subset
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
s : Set α
h : s ⊆ (↑L : Set α)
⊢ sSup s ∈ L

Tactic:
L.sSupClosed' h

Premises used: Set.Mem, CompleteSublattice.sSupClosed'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
s : Set α
h : s ⊆ (↑L : Set α)
⊢ sInf s ∈ L

Tactic:
L.sInfClosed' h

Premises used: Set.Mem, CompleteSublattice.sInfClosed'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ Eq.{u_1 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ (↑(sSup S) : α) = sSup {x : α | ∃ s ∈ S, (↑s : α) = x}

Tactic:
rfl

Premises used: Set.image, rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sSup {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨆ N ∈ S, (↑N : α))
rw₁ : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨆ N ∈ S, (↑N : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ S, (↑a : α)) (⨆ N ∈ S, (↑N : α))
⊢ (↑(sSup S) : α) = ⨆ N ∈ S, (↑N : α)

Tactic:
rw [coe_sSup, ← Set.image, sSup_image]

Premises used: CompleteSublattice.coe_sSup, sSup_image, Set.image
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ (↑(sInf S) : α) = sInf {x : α | ∃ s ∈ S, (↑s : α) = x}

Tactic:
rfl

Premises used: Set.image, rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sInf {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨅ N ∈ S, (↑N : α))
rw₁ : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨅ N ∈ S, (↑N : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨅ a ∈ S, (↑a : α)) (⨅ N ∈ S, (↑N : α))
⊢ (↑(sInf S) : α) = ⨅ N ∈ S, (↑N : α)

Tactic:
rw [coe_sInf, ← Set.image, sInf_image]

Premises used: sInf_image, Set.image, CompleteSublattice.coe_sInf
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sSup (range f)) : α) = ⨆ (i : ι), (↑(f i) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ N ∈ range f, (↑N : α)) (⨆ (i : ι), (↑(f i) : α))
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (↑(f i) : α)) (⨆ (i : ι), (↑(f i) : α))
⊢ (↑(iSup f) : α) = ⨆ (i : ι), (↑(f i) : α)

Tactic:
rw [iSup, coe_sSup', iSup_range]

Premises used: iSup, iSup_range, CompleteSublattice.coe_sSup'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sInf (range f)) : α) = ⨅ (i : ι), (↑(f i) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (⨅ N ∈ range f, (↑N : α)) (⨅ (i : ι), (↑(f i) : α))
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), (↑(f i) : α)) (⨅ (i : ι), (↑(f i) : α))
⊢ (↑(iInf f) : α) = ⨅ (i : ι), (↑(f i) : α)

Tactic:
rw [iInf, coe_sInf', iInf_range]

Premises used: iInf, iInf_range, CompleteSublattice.coe_sInf'
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ Eq (α := (a : ↥L) → α) (⇑L.subtype : (a : ↥L) → α) (Subtype.val (p := fun (x : α) ↦ x ∈ L))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : Sublattice α
a : ↥L
⊢ (L.subtype : (a : ↥L) → α) a = (↑a : α)

Tactic:
rfl

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

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
s : Set β
hs : s ⊆ (⇑f : (a : α) → β) '' (↑L : Set α)
obtain :
  ∀ (t : Set α) (ht : t ⊆ (↑L : Set α))
    (hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))),
    Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup ((⇑f : (a : α) → β) '' t))
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup s)

Tactic:
obtain ⟨t, ht, rfl⟩ := subset_image_iff.mp hs

Premises used: Set.subset_image_iff, Iff.mp, rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sSup t) : β)
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup ((⇑f : (a : α) → β) '' t))

Tactic:
rw [← map_sSup]

Premises used: sSupHomClass.map_sSup
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sSup t) : β)

Tactic:
mem_image_of_mem f (sSupClosed ht)

Premises used: Set.Mem, CompleteSublattice.sSupClosed, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sSup t) : β)

Tactic:
exact mem_image_of_mem f (sSupClosed ht)

Premises used: CompleteSublattice.sSupClosed, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
s : Set β
hs : s ⊆ (⇑f : (a : α) → β) '' (↑L : Set α)
obtain :
  ∀ (t : Set α) (ht : t ⊆ (↑L : Set α))
    (hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))),
    Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf ((⇑f : (a : α) → β) '' t))
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf s)

Tactic:
obtain ⟨t, ht, rfl⟩ := subset_image_iff.mp hs

Premises used: Set.subset_image_iff, Iff.mp, rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sInf t) : β)
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf ((⇑f : (a : α) → β) '' t))

Tactic:
rw [← map_sInf]

Premises used: sInfHomClass.map_sInf
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sInf t) : β)

Tactic:
mem_image_of_mem f (sInfClosed ht)

Premises used: Set.Mem, CompleteSublattice.sInfClosed, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sInf t) : β)

Tactic:
exact mem_image_of_mem f (sInfClosed ht)

Premises used: CompleteSublattice.sInfClosed, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
b : β
⊢ b ∈ map f L ↔ ∃ a ∈ L, (f : (a : α) → β) a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ (⇑f : (a : α) → β) ⁻¹' (↑L : Set β)
⊢ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (↑L : Set β)) (sSup s)

Tactic:
simpa only [mem_preimage, map_sSup, SetLike.mem_coe] using sSupClosed
      <| mapsTo_iff_image_subset.mp hs

Premises used: sSupHomClass.map_sSup, Set.mapsTo_iff_image_subset, CompleteSublattice.sSupClosed, SetLike.mem_coe, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ (⇑f : (a : α) → β) ⁻¹' (↑L : Set β)
⊢ Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (↑L : Set β)) (sInf s)

Tactic:
simpa only [mem_preimage, map_sInf, SetLike.mem_coe] using sInfClosed
      <| mapsTo_iff_image_subset.mp hs

Premises used: sInfHomClass.map_sInf, CompleteSublattice.sInfClosed, Set.mapsTo_iff_image_subset, SetLike.mem_coe, Iff.mp, Set.mem_preimage
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice β
a : α
⊢ a ∈ comap f L ↔ Membership.mem (α := β) L ((f : (a : α) → β) a : β)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
rw₁ : a ⊓ b = ⊥ ↔ (↑a : α) ⊓ (↑b : α) = ⊥
rw₂ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = ⊥
rw₃ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)
rw₄ rw₅ : a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)

Tactic:
rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]

Premises used: Sublattice.coe_inf, Function.Injective.eq_iff, disjoint_iff, Subtype.coe_injective, CompleteSublattice.coe_bot
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
rw₁ : a ⊔ b = ⊤ ↔ (↑a : α) ⊔ (↑b : α) = ⊤
rw₂ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = ⊤
rw₃ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = (↑⊤ : α)
rw₄ rw₅ : a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]

Premises used: codisjoint_iff, Function.Injective.eq_iff, Subtype.coe_injective, CompleteSublattice.coe_top, Sublattice.coe_sup
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : Disjoint a b ∧ Codisjoint a b ↔ IsCompl (↑a : α) (↑b : α)
rw₁ : Disjoint a b ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
rw₂ : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
rw₃ rw₄ :
  Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
⊢ IsCompl a b ↔ IsCompl (↑a : α) (↑b : α)

Tactic:
rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]

Premises used: isCompl_iff, CompleteSublattice.codisjoint_iff, CompleteSublattice.disjoint_iff
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ ComplementedLattice.{u_1} ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b

Tactic:
⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩

Premises used: ComplementedLattice.mk, _private.0.CompleteSublattice.isComplemented_iff.match_1, Membership.mem, Exists, And, IsCompl, Iff.intro, _private.0.CompleteSublattice.isComplemented_iff.match_2
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
refine_1 :
  ComplementedLattice.{u_1} ↥L → ∀ (a : α) (ha : a ∈ L) (h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b), ∃ b ∈ L, IsCompl a b
refine_2 :
  ∀ (h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b) (x : ↥L) (a : α) (ha : a ∈ L),
    ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
⊢ ComplementedLattice.{u_1} ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b

Tactic:
refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h_1 : ComplementedLattice.{u_1} ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b
refine_1 : ∀ (b : ↥L) (hb : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b), ∃ b ∈ L, IsCompl a b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
obtain ⟨b, hb⟩ := h ⟨a, ha⟩

Premises used: Subtype.mk
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h_1 : ComplementedLattice.{u_1} ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b
b : ↥L
hb : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩

Premises used: CompleteSublattice.isCompl_iff, And.intro, Exists.intro, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h_1 : ComplementedLattice.{u_1} ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b
b : ↥L
hb : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x : ↥L
a : α
ha : a ∈ L
refine_2 :
  ∀ (b : α) (hb : b ∈ L) (hb' : IsCompl a b), ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
⊢ ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b

Tactic:
obtain ⟨b, hb, hb'⟩ := h a ha
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b

Tactic:
⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

Premises used: Iff.mpr, CompleteSublattice.isCompl_iff, Subtype.mk, Exists.intro
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b

Tactic:
exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
s : Set α
hs : s = (↑L : Set α)
⊢ (↑(L.copy s hs) : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
s : Set α
hs : s = (↑L : Set α)
⊢ L.copy s hs = L

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
⊢ (↑f.range : Set β) = range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
A B : DedekindCut α
h : A.left = B.left
⊢ A = B

Tactic:
Concept.ext h

Premises used: Concept.ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
A B : DedekindCut α
h : A.right = B.right
⊢ A = B

Tactic:
Concept.ext' h

Premises used: Concept.ext'
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
A : DedekindCut α
⊢ upperBounds A.left = A.right

Tactic:
A.upperPolar_extent

Premises used: Set.Mem, setOf, upperBounds, Concept.upperPolar_extent
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
A : DedekindCut α
⊢ lowerBounds A.right = A.left

Tactic:
A.lowerPolar_intent

Premises used: Concept.lowerPolar_intent, lowerBounds, Set.Mem, setOf
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.left
y : α
hy : y ∈ A.right
⊢ f x ≤ f y

Tactic:
hf <| rel_extent_intent hx hy

Premises used: Concept.rel_extent_intent
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.left
y : α
hy : y ∈ A.right
⊢ f x ≤ f y

Tactic:
exact hf <| rel_extent_intent hx hy

Premises used: Concept.rel_extent_intent
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.right
y : α
hy : y ∈ A.left
⊢ f y ≤ f x

Tactic:
hf <| rel_extent_intent hy hx

Premises used: Concept.rel_extent_intent
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
A : DedekindCut α
x : α
hx : x ∈ A.right
y : α
hy : y ∈ A.left
⊢ f y ≤ f x

Tactic:
exact hf <| rel_extent_intent hy hx

Premises used: Concept.rel_extent_intent
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
h : ∀ (x : α), x ∈ Iic a ↔ x ∈ extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
⊢ Iic a = extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a x : α
⊢ x ∈ Iic a ↔ x ∈ extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)

Tactic:
simpa [mem_lowerPolar_iff] using forall_ge_iff_le.symm

Premises used: forall_ge_iff_le, Iff.symm, mem_lowerPolar_iff
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
h :
  ∀ (x : α),
    x ∈ Ici a ↔
      Membership.mem (γ := Set α) (intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)) x
⊢ Ici a = intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a x : α
⊢ x ∈ Ici a ↔
    Membership.mem (γ := Set α) (intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)) x

Tactic:
simp
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ left (principal a) = Iic a

Tactic:
rfl

Premises used: setOf, Set.Iic, rfl
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ right (principal a) = Ici a

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Concept α α fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a) (principal a)

Tactic:
(copy_eq ..).symm

Premises used: DedekindCut.principal, Concept.copy_eq, Eq.symm