awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
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
have 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 : α)
Tactic: refine fun y hy ↦ hy ?_
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
⊢ 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
have 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 : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ b ∈ upperPolar r {a} ↔ r a b
have simp_rw : (∀ ⦃a_1 : α⦄, Membership.mem (γ := Set α) {a} a_1 → r a_1 b) ↔ r a b
Tactic: simp_rw [mem_upperPolar_iff, mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ b ∈ upperPolar r {a} ↔ r a b
have simp_rw₁ : (∀ ⦃a_1 : α⦄, a_1 = a → r a_1 b) ↔ r a b
Tactic: simp_rw [mem_upperPolar_iff, mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ a ∈ lowerPolar r {b} ↔ r a b
have simp_rw : (∀ ⦃b_1 : β⦄, Membership.mem (γ := Set β) {b} b_1 → r a b_1) ↔ r a b
Tactic: simp_rw [mem_lowerPolar_iff, mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ a ∈ lowerPolar r {b} ↔ r a b
have simp_rw₁ : (∀ ⦃b_1 : β⦄, b_1 = b → r a b_1) ↔ r a b
Tactic: simp_rw [mem_lowerPolar_iff, mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
⊢ IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')
have simp_rw : ∀ (x : Set β) (h : lowerPolar r x = s) (x : Set β) (h : lowerPolar r x = s'), ∃ (y : Set β), lowerPolar r y = s ∩ s'
Tactic: simp_rw [IsExtent, mem_range, forall_exists_index]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ s
have rw : lowerPolar r (upperPolar r s') ⊆ lowerPolar r (upperPolar r s)
Tactic: rw [← h.eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t t' : Set β
h : IsIntent r t
ht' : t' ⊆ t
⊢ upperPolar r (lowerPolar r t') ⊆ t
have rw : upperPolar r (lowerPolar r t') ⊆ upperPolar r (lowerPolar r t)
Tactic: rw [← h.eq]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.extent (r := r) = d.extent (r := r)
⊢ c = d
have obtain : ∀ (s₁ : Set α) (lowerPolar_intent : lowerPolar r (upperPolar r s₁) = s₁)
  (h : (mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r) = d.extent (r := r)),
  mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent = d
Tactic: obtain ⟨s₁, t₁, rfl, _⟩ := c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = d
have obtain : ∀ (s₂ : Set α) (lowerPolar_intent_1 : lowerPolar r (upperPolar r s₂) = s₂)
  (h :
    (mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r) =
      (mk (r := r) s₂ (upperPolar r s₂) sorry lowerPolar_intent_1).extent (r := r)),
  mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent = mk (r := r) s₂ (upperPolar r s₂) sorry lowerPolar_intent_1
Tactic: obtain ⟨s₂, t₂, rfl, _⟩ := d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ mk (r := r) s₁ (upperPolar r s₁) ⋯ lowerPolar_intent = mk (r := r) s₂ (upperPolar r s₂) ⋯ lowerPolar_intent_1
have substs : ∀
  (lowerPolar_intent_2 :
    lowerPolar r (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r))) =
      (mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r)),
  mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent =
    mk (r := r) ((mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r))
      (upperPolar r ((mk (r := r) s₁ (upperPolar r s₁) sorry lowerPolar_intent).extent (r := r))) sorry lowerPolar_intent_2
Tactic: substs h
Cleared hypotheses: s₂, lowerPolar_intent_1, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) = d.intent (r := r)
⊢ c = d
have obtain : ∀ (t₁ : Set β) (upperPolar_extent : upperPolar r (lowerPolar r t₁) = t₁)
  (h : (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r) = d.intent (r := r)),
  mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry = d
Tactic: obtain ⟨s₁, t₁, _, rfl⟩ := c
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = d
have obtain : ∀ (t₂ : Set β) (upperPolar_extent_1 : upperPolar r (lowerPolar r t₂) = t₂)
  (h :
    (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r) =
      (mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 sorry).intent (r := r)),
  mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry = mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 sorry
Tactic: obtain ⟨s₂, t₂, _, rfl⟩ := d
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent ⋯ = mk (r := r) (lowerPolar r t₂) t₂ upperPolar_extent_1 ⋯
have substs : ∀
  (upperPolar_extent_2 :
    upperPolar r (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r))) =
      (mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r)),
  mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry =
    mk (r := r) (lowerPolar r ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r)))
      ((mk (r := r) (lowerPolar r t₁) t₁ upperPolar_extent sorry).intent (r := r)) upperPolar_extent_2 sorry
Tactic: substs h
Cleared hypotheses: t₂, upperPolar_extent_1, h
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ c.copy (r := r) e i he hi = c
have h : ∀ (x : α), x ∈ (c.copy (r := r) e i he hi).extent (r := r) ↔ x ∈ c.extent (r := r)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Concept (hypothesis)
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)
⊢ r x y
have hy₁ : y ∈ upperPolar r (c.extent (r := r))
Tactic: rw [← c.upperPolar_extent] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Irrefl r'
⊢ Disjoint (c'.extent (r := r')) (c'.intent (r := r'))
have rw : ∀ ⦃a : α⦄, a ∈ c'.extent (r := r') → ∀ ⦃b : α⦄, b ∈ c'.intent (r := r') → a ≠ b
Tactic: rw [disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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 ∈ c'.extent (r := r')
have rw : y ∈ lowerPolar r' (c'.intent (r := r'))
Tactic: rw [← lowerPolar_intent]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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 ∈ c'.intent (r := r')
have rw : y ∈ upperPolar r' (c'.extent (r := r'))
Tactic: rw [← upperPolar_extent]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst : Std.Trichotomous r'
inst_1 : IsTrans α r'
⊢ Codisjoint (c'.extent (r := r')) (c'.intent (r := r'))
have rw : ⊤ ≤ c'.extent (r := r') ⊔ c'.intent (r := r')
Tactic: rw [codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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')
have refine : ∀ (x : α), Membership.mem (γ := Set α) ⊤ x → ∀ (hx : x ∉ c'.extent (r := r')), x ∈ c'.intent (r := r')
Tactic: refine fun x _ ↦ or_iff_not_imp_left.2 fun hx ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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')
⊢ x ∈ c'.intent (r := r')
have rw : x ∈ upperPolar r' (c'.extent (r := r'))
Tactic: rw [← upperPolar_extent]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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')
⊢ r' y x
have apply : ¬x = y
Tactic: apply Not.imp_symm <| Std.Trichotomous.trichotomous x y (hx <| mem_extent_of_rel_extent · hy)
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent (r := r) ⊆ d.intent (r := r) ↔ d ≤ c
have refine_1 : ∀ (h : c.intent (r := r) ⊆ d.intent (r := r)), d ≤ c
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ c.intent (r := r) ⊆ d.intent (r := r) ↔ d ≤ c
have refine_2 : ∀ (h : d ≤ c), c.intent (r := r) ⊆ d.intent (r := r)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.intent (r := r) ⊆ d.intent (r := r)
⊢ d ≤ c
have refine_1 : lowerPolar r (d.intent (r := r)) ⊆ lowerPolar r (c.intent (r := r))
Tactic: rw [← extent_subset_extent_iff, ← c.lowerPolar_intent, ← d.lowerPolar_intent]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : d ≤ c
⊢ c.intent (r := r) ⊆ d.intent (r := r)
have refine_2 : upperPolar r (c.extent (r := r)) ⊆ upperPolar r (d.extent (r := r))
Tactic: rw [← c.upperPolar_extent, ← d.upperPolar_extent]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent (r := r) ⊂ d.intent (r := r) ↔ d < c
have rw : c.intent (r := r) ⊆ d.intent (r := r) ∧ ¬d.intent (r := r) ⊆ c.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]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ c.intent (r := r) ⊂ d.intent (r := r) ↔ d < c
have rw₁ : c.intent (r := r) ⊆ d.intent (r := r) ∧ ¬d.intent (r := r) ⊆ c.intent (r := r) ↔ d ≤ c ∧ ¬c ≤ d
Tactic: rw [ssubset_iff_subset_not_subset, lt_iff_le_not_ge,
    intent_subset_intent_iff, intent_subset_intent_iff]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ c.intent (r := r) ⊂ d.intent (r := r) ↔ d < c
have rw₂ : d ≤ c ∧ ¬d.intent (r := r) ⊆ c.intent (r := r) ↔ d ≤ c ∧ ¬c ≤ d
Tactic: rw [ssubset_iff_subset_not_subset, lt_iff_le_not_ge,
    intent_subset_intent_iff, intent_subset_intent_iff]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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
⊢ c.intent (r := r) ⊂ d.intent (r := r) ↔ d < c
have rw₃ : d ≤ c ∧ ¬c ≤ d ↔ d ≤ c ∧ ¬c ≤ d
Tactic: rw [ssubset_iff_subset_not_subset, lt_iff_le_not_ge,
    intent_subset_intent_iff, intent_subset_intent_iff]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
have inl : ∀ (hb : b ≤ b) (ha : 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
Cleared hypotheses: a, hb, ha
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
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)
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
have inr : ∀ (hb : b < a), b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
Tactic: obtain rfl | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb : a ≤ b
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
⊢ b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
have inl : ∀ (hb : a ≤ a), a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
Tactic: obtain rfl | hb := hb.eq_or_lt
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb : a ≤ b
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
inl : ∀ (hb : a ≤ a), a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
⊢ b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
have inr : ∀ (hb : a < b), b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
Tactic: obtain rfl | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ c ≤ ofAttributes r t ↔ t ⊆ c.intent (r := r)
have rw : (ofAttributes r t).intent (r := r) ⊆ c.intent (r := r) ↔ t ⊆ c.intent (r := r)
Tactic: rw [← intent_subset_intent_iff]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent (r := r) ⊆ t
⊢ ofAttributes r t ≤ c
have rw : c.intent (r := r) ⊆ (ofAttributes r t).intent (r := r)
Tactic: rw [← intent_subset_intent_iff]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
⊢ IsLUB s (sSup s)
have refine_1 : ∀ (x : Concept α β r) (hc : x ∈ s), x ≤ sSup s
Tactic: refine ⟨fun _ hc ↦ ?_, fun _ hc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
refine_1 : ∀ (x : Concept α β r) (hc : x ∈ s), x ≤ sSup s
⊢ IsLUB s (sSup s)
have refine_2 : ∀ (x : Concept α β r) (hc : x ∈ upperBounds s), sSup s ≤ x
Tactic: refine ⟨fun _ hc ↦ ?_, fun _ hc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ extent (r := r) (⨆ (i : ι), f i) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
have simp_rw : extent (r := r) (sSup (range fun (i : ι) ↦ f i)) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, extent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : extent (r := r) (sSup (range fun (i : ι) ↦ f i)) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
⊢ extent (r := r) (⨆ (i : ι), f i) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
have simp_rw₁ : lowerPolar r
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r)) =
  lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, extent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : extent (r := r) (sSup (range fun (i : ι) ↦ f i)) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
simp_rw₁ :
  lowerPolar r
      (⋂ (i : Concept α β r),
        ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r)) =
    lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
⊢ extent (r := r) (⨆ (i : ι), f i) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
have simp_rw₂ : lowerPolar r
    (⨅ (i : Concept α β r),
      ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r)) =
  lowerPolar r (⨅ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, extent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ Eq.{u_3 + 1} (α := Set β) (intent (r := r) (⨆ (i : ι), f i)) (⋂ (i : ι), (f i).intent (r := r))
have simp_rw : Eq.{u_3 + 1} (α := Set β) (intent (r := r) (sSup (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, intent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_3 + 1} (α := Set β) (intent (r := r) (sSup (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).intent (r := r))
⊢ Eq.{u_3 + 1} (α := Set β) (intent (r := r) (⨆ (i : ι), f i)) (⋂ (i : ι), (f i).intent (r := r))
have simp_rw₁ : Eq.{u_3 + 1} (α := Set β)
  (⋂ (i : Concept α β r),
    ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r))
  (⋂ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, intent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_3 + 1} (α := Set β) (intent (r := r) (sSup (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).intent (r := r))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Set β)
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r))
    (⋂ (i : ι), (f i).intent (r := r))
⊢ Eq.{u_3 + 1} (α := Set β) (intent (r := r) (⨆ (i : ι), f i)) (⋂ (i : ι), (f i).intent (r := r))
have simp_rw₂ : Eq.{u_3 + 1} (α := Set β)
  (⨅ (i : Concept α β r),
    ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r))
  (⨅ (i : ι), (f i).intent (r := r))
Tactic: simp_rw [iSup, intent_sSup, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ Eq.{u_2 + 1} (α := Set α) (extent (r := r) (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).extent (r := r))
have simp_rw : Eq.{u_2 + 1} (α := Set α) (extent (r := r) (sInf (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, extent_sInf, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_2 + 1} (α := Set α) (extent (r := r) (sInf (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).extent (r := r))
⊢ Eq.{u_2 + 1} (α := Set α) (extent (r := r) (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).extent (r := r))
have simp_rw₁ : Eq.{u_2 + 1} (α := Set α)
  (⋂ (i : Concept α β r),
    ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r))
  (⋂ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, extent_sInf, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_2 + 1} (α := Set α) (extent (r := r) (sInf (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).extent (r := r))
simp_rw₁ :
  Eq.{u_2 + 1} (α := Set α)
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r))
    (⋂ (i : ι), (f i).extent (r := r))
⊢ Eq.{u_2 + 1} (α := Set α) (extent (r := r) (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).extent (r := r))
have simp_rw₂ : Eq.{u_2 + 1} (α := Set α)
  (⨅ (i : Concept α β r),
    ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r))
  (⨅ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, extent_sInf, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ intent (r := r) (⨅ (i : ι), f i) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
have simp_rw : intent (r := r) (sInf (range fun (i : ι) ↦ f i)) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, intent_sInf, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : intent (r := r) (sInf (range fun (i : ι) ↦ f i)) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
⊢ intent (r := r) (⨅ (i : ι), f i) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
have simp_rw₁ : upperPolar r
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r)) =
  upperPolar r (⋂ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, intent_sInf, ← Set.iInf_eq_iInter, iInf_range]