awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
b : (↑(Iic a) : Type u_2)
h : ∀ (ι : Type u_2) (s : ι → α), (↑b : α) ≤ iSup s → ∃ (t : Finset ι), (↑b : α) ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → (↑(Iic a) : Type u_2)
hb : (↑b : α) ≤ iSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s)
t : Finset ι
ht : (↑b : α) ≤ ⨆ a_1 ∈ t, (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ s) a_1
⊢ ∃ (t : Finset ι), b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
exact ⟨t, (by simpa using ht : (b : α) ≤ _)⟩
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
⊢ IsCompactlyGenerated.{u_2} (↑(Iic a) : Type u_2)

Tactic:
⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩

Premises used: IsCompactlyGenerated.mk, Exists, _private.0.Set.Iic.instIsCompactlyGenerated.match_1, And, Eq, SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
refine :
  ∀ (x : (↑(Iic a) : Type u_2)) (x : α) (hx : x ≤ a),
    ∃ (s : Set (↑(Iic a) : Type u_2)),
      (∀ x ∈ s, IsCompactElement x) ∧ sSup s = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx
⊢ IsCompactlyGenerated.{u_2} (↑(Iic a) : Type u_2)

Tactic:
refine ⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x_1 : (↑(Iic a) : Type u_2)
x : α
hx : x ≤ a
obtain :
  ∀ (s : Set α) (hs : ∀ x ∈ s, IsCompactElement x) (hx : sSup s ≤ a),
    ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
      (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx
⊢ ∃ (s : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s, IsCompactElement x) ∧ sSup s = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx

Tactic:
obtain ⟨s, hs, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq x

Premises used: IsCompactlyGenerated.exists_sSup_eq, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx : sSup s ≤ a
⊢ ∀ b ∈ s, b ≤ a

Tactic:
rw [sSup_le_iff] at hx

Premises used: sSup_le_iff
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
⊢ ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1

Tactic:
⟨range f, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Set.range
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_1 : ∀ x ∈ range f, IsCompactElement x
refine_2 : sSup (range f) = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1
⊢ ∃ (s_1 : Set (↑(Iic a) : Type u_2)),
    (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1

Tactic:
refine ⟨range f, ?_, ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
y : α
hy : y ∈ s
⊢ IsCompactElement (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy))

Tactic:
isCompactElement (hs _ hy)

Premises used: Set.Iic.isCompactElement, Set.Mem
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
y : α
hy : y ∈ s
⊢ IsCompactElement (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy))

Tactic:
exact isCompactElement (hs _ hy)

Premises used: Set.Iic.isCompactElement
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_2 : (↑(sSup (range f)) : α) = (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1) : α)
⊢ sSup (range f) = Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1

Tactic:
rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_2 : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f) = sSup s
⊢ (↑(sSup (range f)) : α) = (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (sSup s) hx_1) : α)

Tactic:
change sSup (((↑) : Iic a → α) '' (range f)) = sSup s

Premises used: Set.image, Set.range, Subtype.val, SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_2 : Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f = s
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f) = sSup s

Tactic:
congr
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
refine_2 : ∀ (b : α), b ∈ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f ↔ b ∈ s
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f = s

Tactic:
ext b
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
x : (↑(Iic a) : Type u_2)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx_1 : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : (↑s : Type u_2) → (↑(Iic a) : Type u_2) :=
  fun (y : (↑s : Type u_2)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (↑y : α) ⋯
b : α
⊢ b ∈ Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' range f ↔ b ∈ s

Tactic:
simpa [f] using hx b
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
h₁ : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
⊢ ComplementedLattice α

Tactic:
apply complementedLattice_of_sSup_atoms_eq_top

Premises used: complementedLattice_of_sSup_atoms_eq_top
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
⊢ IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)

Tactic:
replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
obtain :
  ∀ (u : Set (↑(Iic (f i)) : Type u_2)) (hu : ⊤ = sSup u) (hu' : ∀ a ∈ u, IsAtom a),
    ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))

Premises used: Top.top, eq_sSup_atoms
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
⟨(↑) '' u, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Set.image
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
refine_1 : f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
refine_2 : ∀ a ∈ Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u, IsAtom a
⊢ ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
refine ⟨(↑) '' u, ?_, ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ f i = (↑(sSup u) : α)

Tactic:
replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu' : ∀ a ∈ u, IsAtom a
hu : f i = (↑(sSup u) : α)
refine_1 : (↑(sSup u) : α) = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)
⊢ f i = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic (f i)) '' u)

Tactic:
simp_rw [hu, Iic.coe_sSup]

Premises used: Set.Iic.coe_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
a : α
ha' : a ∈ Iic (f i)
ha : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic (f i)) a ha' ∈ u
⊢ IsAtom (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic (f i)) a ha') : α)

Tactic:
IsAtom.of_isAtom_coe_Iic (hu' _ ha)

Premises used: IsAtom.of_isAtom_coe_Iic
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
i : ι
hi : i ∈ s
h : IsAtomistic.{u_2} (↑(Iic (f i)) : Type u_2)
u : Set (↑(Iic (f i)) : Type u_2)
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
a : α
ha' : a ∈ Iic (f i)
ha : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic (f i)) a ha' ∈ u
⊢ IsAtom (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic (f i)) a ha') : α)

Tactic:
exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)

Premises used: IsAtom.of_isAtom_coe_Iic
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
⊢ ∀ i ∈ s, ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦ by
    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
this : ∀ i ∈ s, ∃ (t : Set α), f i = sSup t ∧ ∀ a ∈ t, IsAtom a
h₁ :
  ∀ (t : (i : ι) → i ∈ s → Set α) (ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a))
    (ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1), Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤

Tactic:
choose t ht ht' using this
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
a : α
i : ι
hi : i ∈ s
ha : a ∈ t i hi
⊢ Membership.mem (γ := Set α) {a : α | IsAtom a} a

Tactic:
ht' i hi a ha

Premises used: Set.Mem, setOf, IsAtom
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
a : α
i : ι
hi : i ∈ s
ha : a ∈ t i hi
⊢ Membership.mem (γ := Set α) {a : α | IsAtom a} a

Tactic:
exact ht' i hi a ha
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
⊢ u ⊆ {a : α | IsAtom a}

Tactic:
have hu₁ : u ⊆ {a | IsAtom a} := by
    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
    exact ht' i hi a ha
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
simp_rw : Eq.{u_2 + 1} (α := α) (sSup (⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi)) (⨆ i ∈ s, f i)
simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), ⨆ (i_1 : i ∈ s), sSup (t i i_1)) (⨆ i ∈ s, f i)
⊢ sSup u = ⨆ i ∈ s, f i

Tactic:
simp_rw [u, sSup_iUnion, biSup_congr' ht]

Premises used: sSup_iUnion, biSup_congr'
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
⊢ sSup u = ⨆ i ∈ s, f i

Tactic:
have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
h₁ : sSup u ≤ sSup {a : α | IsAtom a}
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsAtom a}) ⊤

Tactic:
rw [eq_top_iff, ← h', ← hu₂]

Premises used: eq_top_iff
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup u ≤ sSup {a : α | IsAtom a}

Tactic:
sSup_le_sSup hu₁

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Intervals
Goal:
ι : Type u_1
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice.{u_2} (↑(Iic (f i)) : Type u_2)
h' : Eq.{u_2 + 1} (α := α) (⨆ i ∈ s, f i) ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ (i : ι), ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a : α | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup u ≤ sSup {a : α | IsAtom a}

Tactic:
exact sSup_le_sSup hu₁

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : r a b
⊢ CompRel r a b

Tactic:
SymmGen.of_rel h

Premises used: CompRel, Relation.SymmGen.of_rel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : r b a
⊢ CompRel r a b

Tactic:
SymmGen.of_rel_symm h

Premises used: CompRel, Relation.SymmGen.of_rel_symm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
⊢ CompRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) = CompRel r

Tactic:
symmGen_swap r

Premises used: CompRel, Relation.symmGen_swap
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ CompRel (swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ CompRel r a b

Tactic:
symmGen_swap_apply r

Premises used: CompRel, Relation.symmGen_swap_apply
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ CompRel r a a

Tactic:
SymmGen.refl r a

Premises used: CompRel, Relation.SymmGen.refl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a : α
r : α → α → Prop
inst : Std.Refl r
⊢ CompRel r a a

Tactic:
SymmGen.rfl

Premises used: Relation.SymmGen.rfl, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c d : α
r : α → α → Prop
inst : Std.Refl r
⊢ Std.Refl (CompRel r)

Tactic:
SymmGen.instRefl

Premises used: CompRel, Relation.SymmGen.instRefl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ CompRel r a b → CompRel r b a

Tactic:
SymmGen.symm

Premises used: Relation.SymmGen.symm, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c d : α
r : α → α → Prop
⊢ Std.Symm (CompRel r)

Tactic:
SymmGen.instSymm

Premises used: CompRel, Relation.SymmGen.instSymm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ CompRel r a b ↔ CompRel r b a

Tactic:
symmGen_comm

Premises used: CompRel, Relation.symmGen_comm
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
h : AntisymmRel r a b
⊢ CompRel r a b

Tactic:
AntisymmRel.symmGen h

Premises used: CompRel, AntisymmRel.symmGen
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ CompRel r a b

Tactic:
symmGen_of_total a b

Premises used: Relation.symmGen_of_total, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : LE α
h : a ≤ b
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
SymmGen.of_le h

Premises used: CompRel, Relation.SymmGen.of_le
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : LE α
h : b ≤ a
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
SymmGen.of_ge h

Premises used: CompRel, Relation.SymmGen.of_ge
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : a < b
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
SymmGen.of_lt h

Premises used: Relation.SymmGen.of_lt, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
inst : Preorder α
h : b < a
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
SymmGen.of_gt h

Premises used: Relation.SymmGen.of_gt, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
SymmGen.of_symmGen_of_antisymmRel h₁ h₂

Premises used: CompRel, Relation.SymmGen.of_symmGen_of_antisymmRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
SymmGen.of_antisymmRel_of_symmGen h₁ h₂

Premises used: CompRel, Relation.SymmGen.of_antisymmRel_of_symmGen
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c d : α
inst : Preorder α
h₁ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) c d
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b d

Tactic:
AntisymmRel.symmGen_congr h₁ h₂

Premises used: AntisymmRel.symmGen_congr, CompRel
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c ↔ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c

Tactic:
AntisymmRel.symmGen_congr_left h

Premises used: CompRel, AntisymmRel.symmGen_congr_left
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ↔ CompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a c

Tactic:
AntisymmRel.symmGen_congr_right h

Premises used: CompRel, AntisymmRel.symmGen_congr_right
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
r : α → α → Prop
⊢ AntisymmRel rᶜ = IncompRel r

Tactic:
rfl

Premises used: IncompRel, AntisymmRel, rfl
-- Module: Mathlib.Order.Comparable
Goal:
α : Type u_1
a b : α
r : α → α → Prop
⊢ AntisymmRel rᶜ a b ↔ IncompRel r a b

Tactic:
.rfl

Premises used: Iff.rfl, IncompRel, AntisymmRel