awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a : α
h : ∀ (x : α), x ∈ left (ofAttribute (fun (x1 x2 : α) ↦ x1 ≤ x2) a) ↔ x ∈ left (principal a)
⊢ Eq (α := Concept α α fun (x1 x2 : α) ↦ x1 ≤ x2) (ofAttribute (fun (x1 x2 : α) ↦ x1 ≤ x2) a) (principal a)

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a x : α
⊢ x ∈ left (ofAttribute (fun (x1 x2 : α) ↦ x1 ≤ x2) a) ↔ x ∈ left (principal a)

Tactic:
simp
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LE.le (α := DedekindCut α) (principal a) (principal b) ↔ a ≤ b

Tactic:
simpa using ofObject_le_ofAttribute_iff (r := (· ≤ ·)) (a := a)

Premises used: Concept.ofObject_le_ofAttribute_iff
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LT.lt (α := DedekindCut α) (principal a) (principal b) ↔ a < b

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Eq (α := DedekindCut α) (principal a) (principal b) ↔ a = b

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq.{u_1 + 1} (α := (a : α) → DedekindCut α) (⇑principalEmbedding : (a : α) → DedekindCut α) principal

Tactic:
rfl

Premises used: DedekindCut.principal, Concept.copy, rfl
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
h : right (principal (sSup A.left)) = A.right
⊢ principal (sSup A.left) = A

Tactic:
apply ext'

Premises used: DedekindCut.ext'
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
h : ∀ (x : α), x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
⊢ right (principal (sSup A.left)) = A.right

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
h₁ : sSup A.left ≤ x ↔ x ∈ A.right
h₂ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ A.right
h₃ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ upperBounds A.left
h₄ h₅ : (∀ b ∈ A.left, b ≤ x) ↔ ∀ x_1 ∈ A.left, x_1 ≤ x
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right

Tactic:
rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]

Premises used: DedekindCut.upperBounds_left, DedekindCut.right_principal, Set.mem_Ici, sSup_le_iff, mem_upperBounds
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
h : ∀ (x : α), x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
⊢ principal (sInf A.right) = A

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
h₁ : x ≤ sInf A.right ↔ x ∈ A.left
h₂ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ A.left
h₃ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ lowerBounds A.right
h₄ h₅ : (∀ b ∈ A.right, x ≤ b) ↔ ∀ x_1 ∈ A.right, x ≤ x_1
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left

Tactic:
rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]

Premises used: le_sInf_iff, mem_lowerBounds, DedekindCut.left_principal, Set.mem_Iic, DedekindCut.lowerBounds_right
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
⊢ ∀ (a b : DedekindCut β),
    LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) a)
        ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) b) ↔
      a ≤ b

Tactic:
fun A B ↦ ⟨fun h x hx ↦ ?_, fun h ↦ sSup_le_sSup (image_mono h)⟩

Premises used: Set.image_mono, Iff.intro, sSup_le_sSup
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
refine :
  ∀ (A B : DedekindCut β)
    (h :
      LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
        ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B))
    (x : β) (hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)), x ∈ B.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
⊢ ∀ (a b : DedekindCut β),
    LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) a)
        ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) b) ↔
      a ≤ b

Tactic:
refine fun A B ↦ ⟨fun h x hx ↦ ?_, fun h ↦ sSup_le_sSup (image_mono h)⟩
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h :
  LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
    ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B)
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
simp_rw : x ∈ lowerBounds B.right
⊢ x ∈ B.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)

Tactic:
simp_rw [← lowerBounds_right]

Premises used: DedekindCut.lowerBounds_right
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h :
  LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
    ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B)
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
⊢ ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
      ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b

Tactic:
simp_rw [le_sSup_iff, sSup_le_iff, forall_mem_image] at h

Premises used: le_sSup_iff, sSup_le_iff, Set.forall_mem_image
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
h :
  ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
      ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b
y : β
hy : y ∈ B.right
rw : LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)
⊢ x ≤ y

Tactic:
rw [← f.le_iff_le]

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
h :
  ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
      ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b
y : β
hy : y ∈ B.right
⊢ LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)

Tactic:
h _ (image_right_subset_upperBounds f.monotone _ (mem_image_of_mem _ hy)) hx

Premises used: OrderEmbedding.monotone, Set.mem_image_of_mem, DedekindCut.image_right_subset_upperBounds
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
h :
  ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
      ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b
y : β
hy : y ∈ B.right
⊢ LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)

Tactic:
exact h _ (image_right_subset_upperBounds f.monotone _ (mem_image_of_mem _ hy)) hx

Premises used: OrderEmbedding.monotone, Set.mem_image_of_mem, DedekindCut.image_right_subset_upperBounds
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A : DedekindCut β
⊢ Eq.{u_1 + 1} (α := α) ((factorEmbedding f : (a : DedekindCut β) → α) A : α) (sSup ((⇑f : (a : β) → α) '' A.left) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
rw : Eq.{u_1 + 1} (α := α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α) ((f : (a : β) → α) x : α)
⊢ Eq.{u_1 + 1} (α := α) ((factorEmbedding f : (a : DedekindCut β) → α) (principal x) : α) ((f : (a : β) → α) x : α)

Tactic:
rw [factorEmbedding_apply]

Premises used: DedekindCut.factorEmbedding_apply
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ LE.le.{u_1} (α := α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α) ((f : (a : β) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
apply : LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α)
⊢ Eq.{u_1 + 1} (α := α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α) ((f : (a : β) → α) x : α)

Tactic:
apply le_antisymm (by simp)

Premises used: le_antisymm
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
rw :
  ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) b → (f : (a : β) → α) x ≤ b
⊢ LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α)

Tactic:
rw [le_sSup_iff]

Premises used: le_sSup_iff
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) b → (f : (a : β) → α) x ≤ b

Tactic:
fun y hy ↦ hy ?_
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
refine :
  ∀ (y : α) (hy : Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) y),
    Membership.mem.{u_1, u_1} (α := α) (γ := Set α) ((⇑f : (a : β) → α) '' left (principal x)) ((f : (a : β) → α) x : α)
⊢ ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) b → (f : (a : β) → α) x ≤ b

Tactic:
refine fun y hy ↦ hy ?_
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
y : α
hy : Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) y
⊢ Membership.mem.{u_1, u_1} (α := α) (γ := Set α) ((⇑f : (a : β) → α) '' left (principal x)) ((f : (a : β) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
h :
  ∀ (x : β),
    Eq.{u_1 + 1} (α := α)
      ((RelEmbedding.trans (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : DedekindCut β) ↦ x1 ≤ x2) (t :=
              fun (x1 x2 : α) ↦ x1 ≤ x2) principalEmbedding (factorEmbedding f) :
            (a : β) → α)
          x :
        α)
      ((f : (a : β) → α) x : α)
⊢ RelEmbedding.trans (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : DedekindCut β) ↦ x1 ≤ x2) (t :=
      fun (x1 x2 : α) ↦ x1 ≤ x2) principalEmbedding (factorEmbedding f) =
    f

Tactic:
ext
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ Eq.{u_1 + 1} (α := α)
    ((RelEmbedding.trans (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : DedekindCut β) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : α) ↦ x1 ≤ x2) principalEmbedding (factorEmbedding f) :
          (a : β) → α)
        x :
      α)
    ((f : (a : β) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
x : DedekindCut α
⊢ Function.Embedding.toFun
      (RelEmbedding.toEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : DedekindCut α) ↦ x1 ≤ x2)
        principalEmbedding)
      ((factorEmbedding
            (RelIso.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2)
              (OrderIso.refl α)) :
          (a : DedekindCut α) → α)
        x) =
    x

Tactic:
simp [factorEmbedding]

Premises used: DedekindCut.factorEmbedding
-- Module: Mathlib.Order.Completion
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
⊢ sSup
      ((⇑(RelIso.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2) (OrderIso.refl α)) :
          (a : α) → α) ''
        A.left) =
    sSup A.left

Tactic:
simp
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
s : Set α
inst : LE α
⊢ upperPolar (fun (x1 x2 : α) ↦ x1 ≤ x2) s = upperBounds s

Tactic:
rfl

Premises used: setOf, upperBounds, rfl
-- Module: Mathlib.Order.Concept
Goal:
β : Type u_3
t : Set β
inst : LE β
⊢ lowerPolar (fun (x1 x2 : β) ↦ x1 ≤ x2) t = lowerBounds t

Tactic:
rfl

Premises used: lowerBounds, setOf, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
b : β
⊢ b ∈ upperPolar r s ↔ ∀ ⦃a : α⦄, a ∈ s → r a b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, upperPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
a : α
⊢ a ∈ lowerPolar r t ↔ ∀ ⦃b : β⦄, b ∈ t → r a b

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
t : Set β
⊢ t ⊆ upperPolar r s ↔ s ⊆ lowerPolar r t

Tactic:
⟨fun h _ ha _ hb => h hb ha, fun h _ hb _ ha => h ha hb⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ GaloisConnection (β := (Set β)ᵒᵈ) ((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ upperPolar r)
    (lowerPolar r ∘ (⇑ofDual : (a : (Set β)ᵒᵈ) → Set β))

Tactic:
fun _ _ =>
  subset_upperPolar_iff_subset_lowerPolar

Premises used: Set.Mem, setOf, upperPolar, lowerPolar, subset_upperPolar_iff_subset_lowerPolar, GaloisConnection
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ GaloisConnection (β := (Set α)ᵒᵈ) ((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ lowerPolar r)
    (upperPolar r ∘ (⇑ofDual : (a : (Set α)ᵒᵈ) → Set α))

Tactic:
fun _ _ =>
  subset_upperPolar_iff_subset_lowerPolar

Premises used: Set.Mem, setOf, upperPolar, lowerPolar, subset_upperPolar_iff_subset_lowerPolar, GaloisConnection
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ upperPolar (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r) t = lowerPolar r t

Tactic:
rfl

Premises used: setOf, lowerPolar, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ lowerPolar (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r) s = upperPolar r s

Tactic:
rfl

Premises used: setOf, upperPolar, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ upperPolar r ∅ = univ

Tactic:
eq_univ_of_forall fun _ _ => False.elim

Premises used: False.elim, Set.eq_univ_of_forall
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ lowerPolar r ∅ = univ

Tactic:
upperPolar_empty _

Premises used: setOf, upperPolar_empty, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
simp_rw : (∀ ⦃a_1 : α⦄, Membership.mem (γ := Set α) {a} a_1 → r a_1 b) ↔ r a b
simp_rw₁ : (∀ ⦃a_1 : α⦄, a_1 = a → r a_1 b) ↔ r a b
⊢ b ∈ upperPolar r {a} ↔ r a b

Tactic:
simp_rw [mem_upperPolar_iff, mem_singleton_iff, forall_eq]

Premises used: mem_upperPolar_iff, forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
simp_rw : (∀ ⦃b_1 : β⦄, Membership.mem (γ := Set β) {b} b_1 → r a b_1) ↔ r a b
simp_rw₁ : (∀ ⦃b_1 : β⦄, b_1 = b → r a b_1) ↔ r a b
⊢ a ∈ lowerPolar r {b} ↔ r a b

Tactic:
simp_rw [mem_lowerPolar_iff, mem_singleton_iff, forall_eq]

Premises used: forall_eq, Set.mem_singleton_iff, mem_lowerPolar_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ s₂ : Set α
⊢ upperPolar r (s₁ ∪ s₂) = upperPolar r s₁ ∩ upperPolar r s₂

Tactic:
ext fun _ => forall₂_or_left

Premises used: Set.ext, forall₂_or_left
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ t₂ : Set β
⊢ lowerPolar r (t₁ ∪ t₂) = lowerPolar r t₁ ∩ lowerPolar r t₂

Tactic:
upperPolar_union ..

Premises used: upperPolar_union, setOf, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Set α
⊢ upperPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), upperPolar r (f i)

Tactic:
(gc_upperPolar_lowerPolar r).l_iSup

Premises used: iInf, Set.Mem, Set.iInter, gc_upperPolar_lowerPolar, setOf, GaloisConnection.l_iSup, upperPolar, OrderDual, Set.iUnion
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Set β
⊢ lowerPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), lowerPolar r (f i)

Tactic:
upperPolar_iUnion ..

Premises used: setOf, lowerPolar, upperPolar_iUnion
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
κ : ι → Sort u_5
r : α → β → Prop
f : (i : ι) → κ i → Set α
⊢ upperPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), upperPolar r (f i j)

Tactic:
(gc_upperPolar_lowerPolar r).l_iSup₂

Premises used: iInf, Set.Mem, Set.iInter, gc_upperPolar_lowerPolar, setOf, GaloisConnection.l_iSup₂, upperPolar, OrderDual, Set.iUnion
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
κ : ι → Sort u_5
r : α → β → Prop
f : (i : ι) → κ i → Set β
⊢ lowerPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), lowerPolar r (f i j)

Tactic:
upperPolar_iUnion₂ ..

Premises used: setOf, upperPolar_iUnion₂, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ s ⊆ lowerPolar r (upperPolar r s)

Tactic:
(gc_upperPolar_lowerPolar r).le_u_l _

Premises used: Set.Mem, gc_upperPolar_lowerPolar, setOf, GaloisConnection.le_u_l, upperPolar, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ t ⊆ upperPolar r (lowerPolar r t)

Tactic:
subset_lowerPolar_upperPolar _ t

Premises used: Set.Mem, setOf, subset_lowerPolar_upperPolar, upperPolar, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ upperPolar r (lowerPolar r (upperPolar r s)) = upperPolar r s

Tactic:
(gc_upperPolar_lowerPolar r).l_u_l_eq_l _

Premises used: Set.Mem, gc_upperPolar_lowerPolar, setOf, GaloisConnection.l_u_l_eq_l, upperPolar, lowerPolar, OrderDual
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t

Tactic:
upperPolar_lowerPolar_upperPolar _ t

Premises used: Set.Mem, setOf, upperPolar_lowerPolar_upperPolar, upperPolar, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Antitone (upperPolar r)

Tactic:
(gc_upperPolar_lowerPolar r).monotone_l

Premises used: gc_upperPolar_lowerPolar, setOf, upperPolar, Antitone, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Antitone (lowerPolar r)

Tactic:
upperPolar_anti _

Premises used: setOf, lowerPolar, upperPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Monotone (lowerPolar r ∘ upperPolar r)

Tactic:
(gc_upperPolar_lowerPolar r).monotone_u_comp_l

Premises used: GaloisConnection.monotone_u_comp_l, Set.Mem, gc_upperPolar_lowerPolar, setOf, upperPolar, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Monotone (upperPolar r ∘ lowerPolar r)

Tactic:
(gc_lowerPolar_upperPolar r).monotone_u_comp_l

Premises used: GaloisConnection.monotone_u_comp_l, Set.Mem, setOf, upperPolar, lowerPolar, gc_lowerPolar_upperPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ IsExtent r (lowerPolar r t)

Tactic:
⟨_, rfl⟩

Premises used: Order.IsExtent, Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ IsExtent r s ↔ lowerPolar r (upperPolar r s) = s

Tactic:
⟨fun ⟨t, h⟩ ↦ h ▸ lowerPolar_upperPolar_lowerPolar r t, fun h ↦ ⟨_, h⟩⟩

Premises used: Eq.rec, upperPolar, Iff.intro, Exists.intro, lowerPolar, lowerPolar_upperPolar_lowerPolar, Eq, _private.0.Order.isExtent_iff.match_1
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ IsExtent r univ

Tactic:
isExtent_iff.2 (gc_upperPolar_lowerPolar r).u_l_top

Premises used: Iff.mpr, Order.isExtent_iff, gc_upperPolar_lowerPolar, GaloisConnection.u_l_top
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
simp_rw :
  ∀ (x : Set β) (h : lowerPolar r x = s) (x : Set β) (h : lowerPolar r x = s'), ∃ (y : Set β), lowerPolar r y = s ∩ s'
⊢ IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')

Tactic:
simp_rw [IsExtent, mem_range, forall_exists_index]

Premises used: Order.IsExtent, Set.mem_range, forall_exists_index
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
⊢ ∃ (y : Set β), lowerPolar r y = lowerPolar r t ∩ lowerPolar r t'

Tactic:
⟨_, lowerPolar_union r t t'⟩

Premises used: lowerPolar_union, Exists.intro
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
⊢ ∃ (y : Set β), lowerPolar r y = lowerPolar r t ∩ lowerPolar r t'

Tactic:
exact ⟨_, lowerPolar_union r t t'⟩
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Set α
hf : ∀ (i : ι), IsExtent r (f i)
⊢ IsExtent r (⋂ (i : ι), f i)

Tactic:
⟨_, (lowerPolar_iUnion ..).trans (iInter_congr fun i ↦ (hf i).eq)⟩

Premises used: Order.IsExtent.eq, Order.IsExtent, Set.Mem, Set.iInter_congr, setOf, lowerPolar_iUnion, Exists.intro, Set.range, Eq.trans
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
κ : ι → Sort u_5
r : α → β → Prop
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsExtent r (f i j)
⊢ IsExtent r (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
⟨_, (lowerPolar_iUnion₂ ..).trans (iInter₂_congr fun i j ↦ (hf i j).eq)⟩

Premises used: Order.IsExtent.eq, Order.IsExtent, lowerPolar_iUnion₂, Set.Mem, setOf, Exists.intro, Set.range, Set.iInter₂_congr, Eq.trans
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
rw : lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)
⊢ lowerPolar r (upperPolar r s') ⊆ s

Tactic:
rw [← h.eq]

Premises used: Order.IsExtent.eq
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)

Tactic:
lowerPolar_upperPolar_monotone r hs'

Premises used: setOf, lowerPolar_upperPolar_monotone, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)

Tactic:
exact lowerPolar_upperPolar_monotone r hs'

Premises used: lowerPolar_upperPolar_monotone
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ IsIntent r (upperPolar r s)

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Order.IsIntent, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ IsIntent r t ↔ upperPolar r (lowerPolar r t) = t

Tactic:
isExtent_iff

Premises used: Order.isExtent_iff, Set.Mem, setOf, upperPolar, lowerPolar, Order.IsIntent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ IsIntent r univ

Tactic:
IsExtent.univ

Premises used: Set.Mem, setOf, upperPolar, Order.IsIntent, Order.IsExtent.univ
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
⊢ IsIntent r t → IsIntent r t' → IsIntent r (t ∩ t')

Tactic:
IsExtent.inter

Premises used: Set.Mem, setOf, upperPolar, Order.IsIntent, Order.IsExtent.inter