awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
set :
  let t := s.erase ⊥;
  Disjoint (f i) (t.sup id)
⊢ Disjoint (f i) ((s.erase ⊥).sup id)

Tactic:
set t := s.erase ⊥

Premises used: Bot.bot, Finset.erase
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i_1}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' (↑t : Set α)
j : ι
h_1 : j ∈ f ⁻¹' (↑t : Set α)
hij : f i = f j
⊢ i = j

Tactic:
hf ?_ ?_ hij
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i_1}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' (↑t : Set α)
j : ι
h_1 : j ∈ f ⁻¹' (↑t : Set α)
hij : f i = f j
refine_1 : Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} i
refine_2 : Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} j
⊢ i = j

Tactic:
refine hf ?_ ?_ hij
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i_1}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' (↑t : Set α)
j : ι
h_1 : j ∈ f ⁻¹' (↑t : Set α)
hij : f i = f j
⊢ Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} i

Tactic:
aesop (add norm simp [t])
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i_1}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' (↑t : Set α)
j : ι
h_1 : j ∈ f ⁻¹' (↑t : Set α)
hij : f i = f j
⊢ Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} j

Tactic:
aesop (add norm simp [t])
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
⊢ InjOn f (f ⁻¹' (↑t : Set α))

Tactic:
replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
rw rw₁ rw₂ : Disjoint (f i) ((s.erase ⊥).sup id)
rw₃ :
  let t := s.erase ⊥;
  Disjoint (f i) (t.sup id)
rw₄ :
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
rw₅ :
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t),
    Disjoint (f i) (t.sup id)
rw₆ :
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t),
    Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
rw₇ :
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t)
    (h : (insert i (t.preimage f hf)).SupIndep f), Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
rw₈ :
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t)
    (h : ∀ i_1 ∈ insert i (t.preimage f hf), Disjoint (f i_1) (((insert i (t.preimage f hf)).erase i_1).sup f)),
    Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
⊢ Disjoint (f i) (s.sup id)

Tactic:
classical
  rw [← Finset.sup_erase_bot]
  set t := s.erase ⊥
  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
  have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
    ext a
    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]
    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
    obtain ⟨j, hj, rfl⟩ := hs has
    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
  rw [← this, Finset.sup_image]
  specialize h (insert i (t.preimage _ hf))
  rw [Finset.supIndep_iff_disjoint_erase] at h
  exact h i (Finset.mem_insert_self i _)

Premises used: Finset.sup_erase_bot, Finset.supIndep_iff_disjoint_erase, Finset.sup_image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
pos : ∀ (hη : Nonempty η), sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
neg : ∀ (hη : ¬Nonempty η), sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)

Tactic:
by_cases hη : Nonempty η

Premises used: Nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
pos : ∀ (t : Finset α), (↑t : Set α) ⊆ ⋃ (i : η), s i → sSupIndep (↑t : Set α)
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)

Tactic:
rw [sSupIndep_iff_finite]

Premises used: sSupIndep_iff_finite
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : (↑t : Set α) ⊆ ⋃ (i : η), s i
pos : ∀ (I : Set η) (fi : I.Finite) (hI : (↑t : Set α) ⊆ ⋃ i ∈ I, s i), sSupIndep (↑t : Set α)
⊢ sSupIndep (↑t : Set α)

Tactic:
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht

Premises used: Set.finite_subset_iUnion, Finset.finite_toSet
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : (↑t : Set α) ⊆ ⋃ (i : η), s i
I : Set η
fi : I.Finite
hI : (↑t : Set α) ⊆ ⋃ i ∈ I, s i
pos : ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i), sSupIndep (↑t : Set α)
⊢ sSupIndep (↑t : Set α)

Tactic:
obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset

Premises used: Set.Finite.toFinset, Directed.finset_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : (↑t : Set α) ⊆ ⋃ (i : η), s i
I : Set η
fi : I.Finite
hI : (↑t : Set α) ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ sSupIndep (↑t : Set α)

Tactic:
(h i).mono
        (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, sSupIndep.mono
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : (↑t : Set α) ⊆ ⋃ (i : η), s i
I : Set η
fi : I.Finite
hI : (↑t : Set α) ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ sSupIndep (↑t : Set α)

Tactic:
exact (h i).mono
        (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, sSupIndep.mono
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w : Set α
right : a ∈ w
i : η
h_1 : (fun (i : η) ↦ s i) i = w
neg : False
⊢ Disjoint a (sSup ((⋃ (i : η), s i) \ {a}))

Tactic:
exfalso
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w : Set α
right : a ∈ w
i : η
h_1 : (fun (i : η) ↦ s i) i = w
⊢ False

Tactic:
hη ⟨i⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w : Set α
right : a ∈ w
i : η
h_1 : (fun (i : η) ↦ s i) i = w
⊢ False

Tactic:
exact hη ⟨i⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
rw : sSupIndep.{u_2} (α := α) (⋃ (i : (↑s : Type u_2)), (↑i : Set α))
⊢ sSupIndep (⋃₀ s)

Tactic:
rw [Set.sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ (i : (↑s : Type u_2)), sSupIndep (↑i : Set α)

Tactic:
simpa using h
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : (↑s : Type u_2)), (↑i : Set α))

Tactic:
exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)

Premises used: DirectedOn.directed_val, sSupIndep_iUnion_of_directed
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
simp_rw :
  ∀ (i : Finset α) (i_1 : (↑i : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)), a ⊓ i.sup id = ⊥
⊢ Disjoint (⨆ i ∈ s, f i) a

Tactic:
simp_rw [disjoint_iff, iSup_subtype', ← sSup_range, inf_comm, inf_sSup_eq_iSup_inf_sup_finset,
    iSup_eq_bot]

Premises used: iSup_subtype', disjoint_iff, inf_comm, inf_sSup_eq_iSup_inf_sup_finset, sSup_range, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
rwa rwa₁ rwa₂ rwa₃ : (↑u : Set α) ⊆ range fun (x : (↑s : Type u_3)) ↦ f (↑x : ι)
⊢ (↑u : Set α) ⊆ f '' s

Tactic:
rwa [Set.image_eq_range f s]

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
obtain : ∀ (t : Set ι) (ht : t ⊆ s) (ht' : t.Finite) (htu : f '' t = (↑u : Set α)), a ⊓ u.sup id = ⊥
⊢ a ⊓ u.sup id = ⊥

Tactic:
obtain ⟨t, ht, ht', htu⟩ : ∃ᵉ (t ⊆ s) (hu : t.Finite), f '' t = u :=
    Set.Finite.exists_subset_finite_image_eq u.finite_toSet <| by rwa [Set.image_eq_range f s]

Premises used: Set.Finite.exists_subset_finite_image_eq, Finset.finite_toSet
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : f '' t = (↑u : Set α)
⊢ u.sup id = ⨆ i ∈ t, f i

Tactic:
simp only [Finset.sup_eq_iSup, id_eq, ← Finset.mem_coe, ← htu, iSup_image]

Premises used: iSup_image, Finset.sup_eq_iSup, Finset.mem_coe, id_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : f '' t = (↑u : Set α)
⊢ u.sup id = ⨆ i ∈ t, f i

Tactic:
replace htu : u.sup id = ⨆ i ∈ t, f i := by
    simp only [Finset.sup_eq_iSup, id_eq, ← Finset.mem_coe, ← htu, iSup_image]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
rw : Disjoint (⨆ i ∈ t, f i) a
⊢ a ⊓ u.sup id = ⊥

Tactic:
rw [inf_comm, ← disjoint_iff, htu]

Premises used: disjoint_iff, inf_comm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ Disjoint (⨆ i ∈ t, f i) a

Tactic:
hs t ht ht'
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : (↑u : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ Disjoint (⨆ i ∈ t, f i) a

Tactic:
exact hs t ht ht'
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
inst_2 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
⊢ Disjoint.{u_2} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
disjoint_biSup_of_finite_disjoint_biSup fun _ h₁ h₂ ↦
    disjoint_biSup_biSup' hf (Set.disjoint_of_subset_left h₁ hst) h₂

Premises used: disjoint_biSup_of_finite_disjoint_biSup, Set.disjoint_of_subset_left, iSupIndep.disjoint_biSup_biSup'
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : WellFoundedGT α
⊢ ∀ (k : α), IsCompactElement k

Tactic:
rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h

Premises used: CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact, CompleteLattice.isSupFiniteCompact_iff_all_elements_compact
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α

Tactic:
⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩

Premises used: IsCompactlyGenerated.mk, sSup_singleton, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α

Tactic:
exact ⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
eq_top_or_exists_le_coatom : ∀ (b : (↑(Iic k) : Type u_2)), b = ⊤ ∨ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ b ≤ a
⊢ IsCoatomic.{u_2} (↑(Iic k) : Type u_2)

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
eq_top_or_exists_le_coatom :
  ∀ (h : IsCompactElement b) (hbk : b ∈ Iic b),
    Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤ ∨
      ∃ (a : (↑(Iic b) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk ≤ a
eq_top_or_exists_le_coatom₁ :
  ∀ (H : b ≠ k),
    Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk = ⊤ ∨
      ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk = ⊤ ∨
    ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a

Tactic:
obtain rfl | H := eq_or_ne b k

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
eq_top_or_exists_le_coatom : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤ ∨
    ∃ (a : (↑(Iic b) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk ≤ a

Tactic:
left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
eq_top_or_exists_le_coatom : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk) : α) = (↑⊤ : α)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤

Tactic:
ext
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk) : α) = (↑⊤ : α)

Tactic:
simp only [Set.Iic.coe_top]

Premises used: Set.Iic.coe_top
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
eq_top_or_exists_le_coatom :
  ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk = ⊤ ∨
    ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a

Tactic:
right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
eq_top_or_exists_le_coatom :
  ∀ (a : α) (ba : b ≤ a) (h : Maximal (fun (x : α) ↦ x ∈ Iio k) a),
    ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a
eq_top_or_exists_le_coatom₁ :
  ∀ c ⊆ Iio k, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ Iio k, ∀ z ∈ c, z ≤ ub
⊢ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a

Tactic:
have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun (x : α) ↦ x ∈ Iio k) a
⊢ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a

Tactic:
⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩

Premises used: Maximal.prop, le_of_lt, Subtype.mk, And.intro, by_contradiction, Exists.intro, ne_of_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun (x : α) ↦ x ∈ Iio k) a
eq_top_or_exists_le_coatom :
  ∀ (c : (↑(Iic k) : Type u_2)) (hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) a ⋯ < c) (c₀ : ¬c = ⊤), False
⊢ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a

Tactic:
refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun (x : α) ↦ x ∈ Iio k) a
c : (↑(Iic k) : Type u_2)
hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) a ⋯ < c
c₀ : ¬c = ⊤
⊢ b ≤ (↑c : α)

Tactic:
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le

Premises used: LT.lt.le, Maximal.eq_of_le, lt_of_le_of_ne, Subtype.property, Subtype.ext
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun (x : α) ↦ x ∈ Iio k) a
c : (↑(Iic k) : Type u_2)
hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) a ⋯ < c
c₀ : ¬c = ⊤
ba₁ : b ≤ (↑c : α)
⊢ Maximal (fun (x : α) ↦ x ∈ Iio k) (↑c : α)

Tactic:
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le

Premises used: LT.lt.le, Maximal.eq_of_le, lt_of_le_of_ne, Subtype.property, Subtype.ext
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun (x : α) ↦ x ∈ Iio k) a
c : (↑(Iic k) : Type u_2)
hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) a ⋯ < c
c₀ : ¬c = ⊤
ba₁ : b ≤ (↑c : α)
h₁ : Maximal (fun (x : α) ↦ x ∈ Iio k) (↑c : α)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) (↑c : α) ⋯ < c

Tactic:
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le

Premises used: LT.lt.le, Maximal.eq_of_le, lt_of_le_of_ne, Subtype.property, Subtype.ext
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : (↑(Iic k) : Type u_2)
c₀ : ¬c = ⊤
ba : b ≤ (↑c : α)
h : Maximal (fun (x : α) ↦ x ∈ Iio k) (↑c : α)
hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) (↑c : α) ⋯ < c
⊢ False

Tactic:
lt_irrefl _ hck

Premises used: lt_irrefl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h_1 : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : (↑(Iic k) : Type u_2)
c₀ : ¬c = ⊤
ba : b ≤ (↑c : α)
h : Maximal (fun (x : α) ↦ x ∈ Iio k) (↑c : α)
hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) (↑c : α) ⋯ < c
⊢ False

Tactic:
exact lt_irrefl _ hck

Premises used: lt_irrefl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) S
I : α
eq_top_or_exists_le_coatom : I ∈ S → ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
⊢ I ∈ S → ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
_
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) S
I : α
h_1 : I ∈ S
pos : ∀ (hS : S.Nonempty), ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
neg : ∀ (hS : ¬S.Nonempty), ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
by_cases hS : S.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) S
I : α
h_1 : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩

Premises used: IsChain.directedOn, And.intro, Exists.intro, CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt, SupSet.sSup