awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Set β
hf : ∀ (i : ι), IsIntent r (f i)
⊢ IsIntent r (⋂ (i : ι), f i)

Tactic:
IsExtent.iInter _ hf

Premises used: Set.Mem, setOf, upperPolar, Order.IsExtent.iInter, Order.IsIntent
-- 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), IsIntent r (f i j)
⊢ IsIntent r (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
IsExtent.iInter₂ _ hf

Premises used: Order.IsExtent.iInter₂, Set.Mem, setOf, upperPolar, Order.IsIntent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
rw : upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)
⊢ upperPolar r (lowerPolar r t') ⊆ t

Tactic:
rw [← h.eq]

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

Tactic:
upperPolar_lowerPolar_monotone r ht'

Premises used: setOf, upperPolar, upperPolar_lowerPolar_monotone
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)

Tactic:
exact upperPolar_lowerPolar_monotone r ht'

Premises used: upperPolar_lowerPolar_monotone
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.extent (r := r) = d.extent (r := r)
obtain :
  ∀ (s₁ : Set α) (lowerPolar_intent : lowerPolar r (upperPolar r s₁) = s₁)
    (h : (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r) = d.extent (r := r)),
    mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = d
⊢ c = d

Tactic:
obtain ⟨s₁, t₁, rfl, _⟩ := c

Premises used: rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
d : Concept α β r
s₁ : Set α
lowerPolar_intent : lowerPolar r (upperPolar r s₁) = s₁
h : (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r) = d.extent (r := r)
obtain :
  ∀ (s₂ : Set α) (lowerPolar_intent_1 : lowerPolar r (upperPolar r s₂) = s₂)
    (h :
      (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r) =
        (mk (r := r) s₂ (upperPolar r s₂) ⋯ lowerPolar_intent_1).extent (r := r)),
    mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = mk (r := r) s₂ (upperPolar r s₂) ⋯ lowerPolar_intent_1
⊢ mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = d

Tactic:
obtain ⟨s₂, t₂, rfl, _⟩ := d

Premises used: rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
lowerPolar_intent : lowerPolar r (upperPolar r s₁) = s₁
s₂ : Set α
lowerPolar_intent_1 : lowerPolar r (upperPolar r s₂) = s₂
h :
  (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r) =
    (mk (r := r) s₂ (upperPolar r s₂) ⋯ lowerPolar_intent_1).extent (r := r)
substs :
  ∀
    (lowerPolar_intent_2 :
      lowerPolar r (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))) =
        (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r)),
    mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent =
      mk (r := r) ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))
        (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))) ⋯ lowerPolar_intent_2
⊢ mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = mk (r := r) s₂ (upperPolar r s₂) ⋯ lowerPolar_intent_1

Tactic:
substs h
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
lowerPolar_intent : lowerPolar r (upperPolar r s₁) = s₁
lowerPolar_intent_1 :
  lowerPolar r (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))) =
    (mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r)
⊢ mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent =
    mk (r := r) ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))
      (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent).extent (r := r))) ⋯ lowerPolar_intent_1

Tactic:
rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) = d.intent (r := r)
obtain :
  ∀ (t₁ : Set β) (upperPolar_extent : upperPolar r (lowerPolar r t₁) = t₁)
    (h : (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r) = d.intent (r := r)),
    mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = d
⊢ c = d

Tactic:
obtain ⟨s₁, t₁, _, rfl⟩ := c

Premises used: rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
d : Concept α β r
t₁ : Set β
upperPolar_extent : upperPolar r (lowerPolar r t₁) = t₁
h : (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r) = d.intent (r := r)
obtain :
  ∀ (t₂ : Set β) (upperPolar_extent_1 : upperPolar r (lowerPolar r t₂) = t₂)
    (h :
      (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r) =
        (mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 ⋯).intent (r := r)),
    mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 ⋯
⊢ mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = d

Tactic:
obtain ⟨s₂, t₂, _, rfl⟩ := d

Premises used: rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
upperPolar_extent : upperPolar r (lowerPolar r t₁) = t₁
t₂ : Set β
upperPolar_extent_1 : upperPolar r (lowerPolar r t₂) = t₂
h :
  (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r) =
    (mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 ⋯).intent (r := r)
substs :
  ∀
    (upperPolar_extent_2 :
      upperPolar r (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r))) =
        (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)),
    mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ =
      mk (r := r) (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)))
        ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)) upperPolar_extent_2 ⋯
⊢ mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 ⋯

Tactic:
substs h
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
upperPolar_extent : upperPolar r (lowerPolar r t₁) = t₁
upperPolar_extent_1 :
  upperPolar r (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r))) =
    (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)
⊢ mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ =
    mk (r := r) (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)))
      ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯).intent (r := r)) upperPolar_extent_1 ⋯

Tactic:
rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Injective (α := Concept α β r) (extent (r := r))

Tactic:
fun _ _ => ext

Premises used: Concept.ext, Function.Injective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Injective (α := Concept α β r) (intent (r := r))

Tactic:
fun _ _ => ext'

Premises used: Concept.ext', Function.Injective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
e : Set α
i : Set β
he : e = c.extent (r := r)
hi : i = c.intent (r := r)
h : ∀ (x : α), x ∈ (c.copy (r := r) e i he hi).extent (r := r) ↔ x ∈ c.extent (r := r)
⊢ c.copy (r := r) e i he hi = c

Tactic:
ext
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
e : Set α
i : Set β
he : e = c.extent (r := r)
hi : i = c.intent (r := r)
x : α
⊢ x ∈ (c.copy (r := r) e i he hi).extent (r := r) ↔ x ∈ c.extent (r := r)

Tactic:
simp_all
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
⊢ IsExtent r (c.extent (r := r))

Tactic:
lowerPolar_intent c ▸ isExtent_lowerPolar

Premises used: Concept.lowerPolar_intent, Eq.rec, Order.isExtent_lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
⊢ IsExtent r s ↔ ∃ (c : Concept α β r), c.extent (r := r) = s

Tactic:
⟨fun h ↦ ⟨ofIsExtent _ _ h, rfl⟩, fun ⟨c, h⟩ ↦ h ▸ c.isExtent_extent⟩

Premises used: Order.IsExtent, Eq.rec, Concept.ofIsExtent, _private.0.Concept.isExtent_iff_exists_concept.match_1, Iff.intro, Exists.intro, rfl, Concept.isExtent_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
⊢ IsIntent r (c.intent (r := r))

Tactic:
upperPolar_extent c ▸ isIntent_upperPolar

Premises used: Eq.rec, Order.isIntent_upperPolar, Concept.upperPolar_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
⊢ IsIntent r t ↔ ∃ (c : Concept α β r), c.intent (r := r) = t

Tactic:
⟨fun h ↦ ⟨ofIsIntent _ _ h, rfl⟩, fun ⟨c, h⟩ ↦ h ▸ c.isIntent_intent⟩

Premises used: _private.0.Concept.isIntent_iff_exists_concept.match_1, Concept.isIntent_intent, Eq.rec, Concept.ofIsIntent, Iff.intro, Exists.intro, Order.IsIntent, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
⊢ ofObjects r (c.extent (r := r)) = c

Tactic:
intent_injective c.upperPolar_extent

Premises used: Concept.upperPolar_extent, Concept.intent_injective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
hs : IsExtent r s
⊢ (ofObjects r s).extent (r := r) = s

Tactic:
hs.eq

Premises used: Order.IsExtent.eq, setOf, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ LeftInverse (ofObjects r) (extent (r := r))

Tactic:
fun _ ↦ ofObjects_extent

Premises used: Concept.ofObjects_extent, Function.LeftInverse
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ LeftInvOn (extent (r := r)) (ofObjects r) {s : Set α | IsExtent r s}

Tactic:
fun _ ↦ IsExtent.eq

Premises used: Order.IsExtent.eq, Order.IsExtent, Set.LeftInvOn, Set.Mem, setOf, Set.range, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Surjective (ofObjects r)

Tactic:
leftInverse_ofObjects_extent.surjective

Premises used: Function.LeftInverse.surjective, Concept.leftInverse_ofObjects_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
⊢ ofAttributes r (c.intent (r := r)) = c

Tactic:
extent_injective c.lowerPolar_intent

Premises used: Concept.lowerPolar_intent, Concept.extent_injective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
hs : IsIntent r t
⊢ (ofAttributes r t).intent (r := r) = t

Tactic:
hs.eq

Premises used: setOf, upperPolar, Order.IsIntent.eq
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ LeftInverse (ofAttributes r) (intent (r := r))

Tactic:
fun c ↦ extent_injective c.lowerPolar_intent

Premises used: Concept.lowerPolar_intent, Function.LeftInverse, Concept.extent_injective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ LeftInvOn (intent (r := r)) (ofAttributes r) {s : Set β | IsIntent r s}

Tactic:
fun _ ↦ IsIntent.eq

Premises used: Set.LeftInvOn, Set.Mem, setOf, upperPolar, Order.IsIntent.eq, Set.range, Order.IsIntent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ Surjective (ofAttributes r)

Tactic:
leftInverse_ofAttributes_extent.surjective

Premises used: Concept.leftInverse_ofAttributes_extent, Function.LeftInverse.surjective
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
x : α
y : β
hx : x ∈ c.extent (r := r)
hy : y ∈ c.intent (r := r)
⊢ y ∈ upperPolar r (c.extent (r := r))

Tactic:
rw [← c.upperPolar_extent] at hy

Premises used: Concept.upperPolar_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
x : α
y : β
hx : x ∈ c.extent (r := r)
hy : y ∈ upperPolar r (c.extent (r := r))
⊢ r x y

Tactic:
hy hx
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
x : α
y : β
hx : x ∈ c.extent (r := r)
hy : y ∈ upperPolar r (c.extent (r := r))
⊢ r x y

Tactic:
exact hy hx
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Irrefl r'
rw : ∀ ⦃a : α⦄, a ∈ c'.extent (r := r') → ∀ ⦃b : α⦄, b ∈ c'.intent (r := r') → a ≠ b
⊢ Disjoint (c'.extent (r := r')) (c'.intent (r := r'))

Tactic:
rw [disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Irrefl r'
x : α
hx : x ∈ c'.extent (r := r')
hx' : x ∈ c'.intent (r := r')
⊢ False

Tactic:
irrefl x (rel_extent_intent hx hx')

Premises used: irrefl, Concept.rel_extent_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Irrefl r'
x : α
hx : x ∈ c'.extent (r := r')
hx' : x ∈ c'.intent (r := r')
⊢ False

Tactic:
exact irrefl x (rel_extent_intent hx hx')

Premises used: irrefl, Concept.rel_extent_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent (r := r')
rw : y ∈ lowerPolar r' (c'.intent (r := r'))
⊢ y ∈ c'.extent (r := r')

Tactic:
rw [← lowerPolar_intent]

Premises used: Concept.lowerPolar_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent (r := r')
⊢ y ∈ lowerPolar r' (c'.intent (r := r'))

Tactic:
fun z hz ↦ _root_.trans hy (rel_extent_intent hx hz)

Premises used: trans, Set.Mem, setOf, Concept.rel_extent_intent, lowerPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent (r := r')
⊢ y ∈ lowerPolar r' (c'.intent (r := r'))

Tactic:
exact fun z hz ↦ _root_.trans hy (rel_extent_intent hx hz)

Premises used: trans, Concept.rel_extent_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent (r := r')
rw : y ∈ upperPolar r' (c'.extent (r := r'))
⊢ y ∈ c'.intent (r := r')

Tactic:
rw [← upperPolar_extent]

Premises used: Concept.upperPolar_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent (r := r')
⊢ y ∈ upperPolar r' (c'.extent (r := r'))

Tactic:
fun z hz ↦ _root_.trans (rel_extent_intent hz hx) hy

Premises used: trans, Set.Mem, setOf, Concept.rel_extent_intent, upperPolar
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent (r := r')
⊢ y ∈ upperPolar r' (c'.extent (r := r'))

Tactic:
exact fun z hz ↦ _root_.trans (rel_extent_intent hz hx) hy

Premises used: trans, Concept.rel_extent_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
rw : ⊤ ≤ c'.extent (r := r') ⊔ c'.intent (r := r')
⊢ Codisjoint (c'.extent (r := r')) (c'.intent (r := r'))

Tactic:
rw [codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_sup
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
⊢ ⊤ ≤ c'.extent (r := r') ⊔ c'.intent (r := r')

Tactic:
fun x _ ↦ or_iff_not_imp_left.2 fun hx ↦ ?_

Premises used: Iff.mpr, Set.union, Set.Mem, setOf, Set.Subset, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
refine : ∀ (x : α), Membership.mem (γ := Set α) ⊤ x → ∀ (hx : x ∉ c'.extent (r := r')), x ∈ c'.intent (r := r')
⊢ ⊤ ≤ c'.extent (r := r') ⊔ c'.intent (r := r')

Tactic:
refine fun x _ ↦ or_iff_not_imp_left.2 fun hx ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
x : α
h : Membership.mem (γ := Set α) ⊤ x
hx : x ∉ c'.extent (r := r')
rw : x ∈ upperPolar r' (c'.extent (r := r'))
⊢ x ∈ c'.intent (r := r')

Tactic:
rw [← upperPolar_extent]

Premises used: Concept.upperPolar_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
x : α
h : Membership.mem (γ := Set α) ⊤ x
hx : x ∉ c'.extent (r := r')
y : α
hy : y ∈ c'.extent (r := r')
apply : ¬x = y
⊢ r' y x

Tactic:
apply Not.imp_symm <| Std.Trichotomous.trichotomous x y (hx <| mem_extent_of_rel_extent · hy)

Premises used: Concept.mem_extent_of_rel_extent, Not.imp_symm, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
x : α
h : Membership.mem (γ := Set α) ⊤ x
hx : x ∉ c'.extent (r := r')
y : α
hy : y ∈ c'.extent (r := r')
⊢ ¬x = y

Tactic:
(hx <| · ▸ hy)

Premises used: Eq.rec, Eq.symm, Not
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
x : α
h : Membership.mem (γ := Set α) ⊤ x
hx : x ∉ c'.extent (r := r')
y : α
hy : y ∈ c'.extent (r := r')
⊢ ¬x = y

Tactic:
exact (hx <| · ▸ hy)
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
inst : IsStrictTotalOrder α r'
c' : Concept α α r'
⊢ IsCompl (c'.extent (r := r')) (c'.intent (r := r'))

Tactic:
⟨c'.disjoint_extent_intent, c'.codisjoint_extent_intent⟩

Premises used: Concept.codisjoint_extent_intent, IsCompl.mk, Concept.disjoint_extent_intent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
inst : IsStrictTotalOrder α r'
c' : Concept α α r'
⊢ (c'.extent (r := r'))ᶜ = c'.intent (r := r')

Tactic:
c'.isCompl_extent_intent.compl_eq

Premises used: Concept.isCompl_extent_intent, IsCompl.compl_eq
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
r' : α → α → Prop
inst : IsStrictTotalOrder α r'
c' : Concept α α r'
⊢ (c'.intent (r := r'))ᶜ = c'.extent (r := r')

Tactic:
c'.isCompl_extent_intent.symm.compl_eq

Premises used: Concept.isCompl_extent_intent, IsCompl.compl_eq, IsCompl.symm
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.extent (r := r) ⊆ d.extent (r := r) ↔ c ≤ d

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.extent (r := r) ⊂ d.extent (r := r) ↔ c < d

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent (r := r) ⊆ d.intent (r := r) ↔ d ≤ c

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
refine_1 : ∀ (h : c.intent (r := r) ⊆ d.intent (r := r)), d ≤ c
refine_2 : ∀ (h : d ≤ c), c.intent (r := r) ⊆ d.intent (r := r)
⊢ c.intent (r := r) ⊆ d.intent (r := r) ↔ d ≤ c

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) ⊆ d.intent (r := r)
refine_1 : lowerPolar r (d.intent (r := r)) ⊆ lowerPolar r (c.intent (r := r))
⊢ d ≤ c

Tactic:
rw [← extent_subset_extent_iff, ← c.lowerPolar_intent, ← d.lowerPolar_intent]

Premises used: Concept.lowerPolar_intent, Concept.extent_subset_extent_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) ⊆ d.intent (r := r)
⊢ lowerPolar r (d.intent (r := r)) ⊆ lowerPolar r (c.intent (r := r))

Tactic:
lowerPolar_anti _ h

Premises used: lowerPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) ⊆ d.intent (r := r)
⊢ lowerPolar r (d.intent (r := r)) ⊆ lowerPolar r (c.intent (r := r))

Tactic:
exact lowerPolar_anti _ h

Premises used: lowerPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
refine_2 : upperPolar r (c.extent (r := r)) ⊆ upperPolar r (d.extent (r := r))
⊢ c.intent (r := r) ⊆ d.intent (r := r)

Tactic:
rw [← c.upperPolar_extent, ← d.upperPolar_extent]

Premises used: Concept.upperPolar_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ upperPolar r (c.extent (r := r)) ⊆ upperPolar r (d.extent (r := r))

Tactic:
upperPolar_anti _ h

Premises used: upperPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ upperPolar r (c.extent (r := r)) ⊆ upperPolar r (d.extent (r := r))

Tactic:
exact upperPolar_anti _ h

Premises used: upperPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
rw : c.intent (r := r) ⊆ d.intent (r := r) ∧ ¬d.intent (r := r) ⊆ c.intent (r := r) ↔ d < c
rw₁ : c.intent (r := r) ⊆ d.intent (r := r) ∧ ¬d.intent (r := r) ⊆ c.intent (r := r) ↔ d ≤ c ∧ ¬c ≤ d
rw₂ : d ≤ c ∧ ¬d.intent (r := r) ⊆ c.intent (r := r) ↔ d ≤ c ∧ ¬c ≤ d
rw₃ rw₄ : d ≤ c ∧ ¬c ≤ d ↔ d ≤ c ∧ ¬c ≤ d
⊢ c.intent (r := r) ⊂ d.intent (r := r) ↔ d < c

Tactic:
rw [ssubset_iff_subset_not_subset, lt_iff_le_not_ge,
    intent_subset_intent_iff, intent_subset_intent_iff]

Premises used: lt_iff_le_not_ge, Concept.intent_subset_intent_iff, ssubset_iff_subset_not_subset
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ StrictMono (α := Concept α β r) (extent (r := r))

Tactic:
fun _ _ =>
  extent_ssubset_extent_iff.2

Premises used: Iff.mpr, StrictMono, Concept.extent_ssubset_extent_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
⊢ StrictAnti (α := Concept α β r) (intent (r := r))

Tactic:
fun _ _ =>
  intent_ssubset_intent_iff.2

Premises used: Iff.mpr, Concept.intent_ssubset_intent_iff, StrictAnti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : Preorder α
c : Concept α α fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ IsLowerSet (c.extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2))

Tactic:
@mem_extent_of_rel_extent _ _ _ _

Premises used: Set.Mem, Concept.mem_extent_of_rel_extent, IsLowerSet
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : Preorder α
c : Concept α α fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ IsUpperSet (c.intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2))

Tactic:
@mem_intent_of_intent_rel _ _ _ _

Premises used: Set.Mem, IsUpperSet, Concept.mem_intent_of_intent_rel
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb : b ≤ a
ha : a ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
inl : ∀ (hb : b ≤ b) (ha : b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)), b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
inr : ∀ (hb : b < a), b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
obtain rfl | hb := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
b : α
hb : b ≤ b
ha : b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
assumption
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb_1 : b ≤ a
ha : a ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
hb : b < a
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
mem_extent_of_rel_extent hb ha

Premises used: Concept.mem_extent_of_rel_extent