awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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)
⊢ Disjoint (f i) (s.sup id)
have 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))
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 _)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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))
⊢ Disjoint (f i) (s.sup id)
have 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))
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 _)
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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))
⊢ Disjoint (f i) (s.sup id)
have 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))
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 _)
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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)
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
have pos : ∀ (hη : Nonempty η), sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
Tactic: by_cases hη : Nonempty η
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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)
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
have neg : ∀ (hη : ¬Nonempty η), sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
Tactic: by_cases hη : Nonempty η
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 η
⊢ sSupIndep.{u_2} (α := α) (⋃ (i : η), s i)
have pos : ∀ (t : Finset α), (↑t : Set α) ⊆ ⋃ (i : η), s i → sSupIndep (↑t : Set α)
Tactic: rw [sSupIndep_iff_finite]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ sSupIndep (↑t : Set α)
have pos : ∀ (I : Set η) (fi : I.Finite) (hI : (↑t : Set α) ⊆ ⋃ i ∈ I, s i), sSupIndep (↑t : Set α)
Tactic: obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ sSupIndep (↑t : Set α)
have pos : ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i), sSupIndep (↑t : Set α)
Tactic: obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Disjoint a (sSup ((⋃ (i : η), s i) \ {a}))
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 (⋃₀ s)
have rw : sSupIndep.{u_2} (α := α) (⋃ (i : (↑s : Type u_2)), (↑i : Set α))
Tactic: rw [Set.sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Disjoint (⨆ i ∈ s, f i) a
have simp_rw : ∀ (i : Finset α) (i_1 : (↑i : Set α) ⊆ range fun (x : Subtype (Membership.mem s)) ↦ f (↑x : ι)), a ⊓ i.sup id = ⊥
Tactic: simp_rw [disjoint_iff, iSup_subtype', ← sSup_range, inf_comm, inf_sSup_eq_iSup_inf_sup_finset,
    iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ι)
⊢ (↑u : Set α) ⊆ f '' s
have rwa : (↑u : Set α) ⊆ range fun (x : (↑s : Type u_3)) ↦ f (↑x : ι)
Tactic: rwa [Set.image_eq_range f s]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ι)
⊢ a ⊓ u.sup id = ⊥
have obtain : ∀ (t : Set ι) (ht : t ⊆ s) (ht' : t.Finite) (htu : f '' t = (↑u : Set α)), 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]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 α)
⊢ a ⊓ u.sup id = ⊥
have htu₁ : 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]
Cleared hypotheses: htu
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ a ⊓ u.sup id = ⊥
have rw : Disjoint (⨆ i ∈ t, f i) a
Tactic: rw [inf_comm, ← disjoint_iff, htu]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
h : WellFoundedGT α
⊢ IsCompactlyGenerated α
have h₁ : ∀ (k : α), IsCompactElement k
Tactic: rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
⊢ IsCoatomic.{u_2} (↑(Iic k) : Type u_2)
have eq_top_or_exists_le_coatom : ∀ (b : (↑(Iic k) : Type u_2)), b = ⊤ ∨ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ b ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic 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
have 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
Tactic: obtain rfl | H := eq_or_ne b k
Cleared hypotheses: k, h, hbk
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ 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
have 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
Tactic: obtain rfl | H := eq_or_ne b k
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
b : α
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
have eq_top_or_exists_le_coatom : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤
Tactic: left
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk = ⊤
have eq_top_or_exists_le_coatom : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) b hbk) : α) = (↑⊤ : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
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
have 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
Tactic: right
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a
have 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
Tactic: have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (a : (↑(Iic k) : Type u_2)), IsCoatom a ∧ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) b hbk ≤ a
have 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
Tactic: have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have eq_top_or_exists_le_coatom : ∀ (c : (↑(Iic k) : Type u_2)) (hck : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) a sorry < c) (c₀ : ¬c = ⊤), False
Tactic: refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 = ⊤
⊢ False
have ba₁ : 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
Cleared hypotheses: a, ba, h, hck
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 : α)
⊢ False
have h₁ : 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
Cleared hypotheses: a, ba, h, hck
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 : α)
⊢ False
have hck₁ : Subtype.mk (p := fun (x : α) ↦ x ∈ Iic k) (↑c : α) sorry < 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
Cleared hypotheses: a, ba, h, hck
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
have pos : ∀ (hS : S.Nonempty), ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
have neg : ∀ (hS : ¬S.Nonempty), ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have pos : ∀ z ∈ S, z ≤ sSup S
Tactic: refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ iSupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have rw : ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: rw [iSupIndep_iff_supIndep]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have pos : ∀ (hs : 1 < s.card), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: by_cases hs : 1 < s.card
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
pos : ∀ (hs : 1 < s.card), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have neg : ∀ (hs : ¬1 < s.card), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: by_cases hs : 1 < s.card
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
hs : ¬1 < s.card
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have pos : ∀ (hcard0 : s.card = 0), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: by_cases hcard0 : s.card = 0
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
hs : ¬1 < s.card
pos : ∀ (hcard0 : s.card = 0), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have neg : ∀ (hcard0 : ¬s.card = 0), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: by_cases hcard0 : s.card = 0
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
hs : 1 < s.card
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have pos : ∀ (k₁ k₂ : (i : ι) → κ i),
  k₁ ∈ s → k₂ ∈ s → ∀ (h : k₁ ≠ k₂), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left : k₁ ∈ s
left_1 : k₂ ∈ s
h : k₁ ≠ k₂
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have pos : ∀ (i : ι) (hi : k₁ i ≠ k₂ i), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
Tactic: obtain ⟨i, hi⟩ : ∃ i : ι, k₁ i ≠ k₂ i := Function.ne_iff.mp h