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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have : InjOn f {i : ι | f i ≠ ⊥}
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have₅ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
  Disjoint (f i) (i_1.sup id)
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have₇ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
  Disjoint (f i) ((s.erase ⊥).sup id)
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
have₇ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) ((s.erase ⊥).sup id)
have₈ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    Disjoint (f i) (t.sup id)
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have₉ : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
  let t := s.erase ⊥;
  ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
have₇ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) ((s.erase ⊥).sup id)
have₈ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    Disjoint (f i) (t.sup id)
have₉ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have have₁₀ : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
  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)
Tactic: classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
have₇ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) ((s.erase ⊥).sup id)
have₈ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    Disjoint (f i) (t.sup id)
have₉ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
have₁₀ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    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) (sSup (f '' {j : ι | j ≠ i}))
have have₁₁ : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
  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
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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 _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
have₇ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) ((s.erase ⊥).sup id)
have₈ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    Disjoint (f i) (t.sup id)
have₉ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
have₁₀ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    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)
have₁₁ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    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) (sSup (f '' {j : ι | j ≠ i}))
have have₁₂ : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
  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
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  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: 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 ≠ ⊥}
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f
have refine : ∀ (h : ∀ (s : Finset ι), s.SupIndep f) (i : ι), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
Tactic: refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
-- 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 : ι
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have simp_rw : ∀ (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}), Disjoint (f i) (i_1.sup id)
Tactic: simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
-- 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}
⊢ Disjoint (f i) (s.sup id)
have rw : Disjoint (f i) ((s.erase ⊥).sup id)
Tactic: rw [← Finset.sup_erase_bot]
-- 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_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
have refine_1 : Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} i
Tactic: refine hf ?_ ?_ hij
-- 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_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
⊢ i = j
have refine_2 : Membership.mem (γ := Set ι) {i : ι | f i ≠ ⊥} j
Tactic: refine hf ?_ ?_ hij
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ⊥
⊢ Disjoint (f i) (t.sup id)
have hf₁ : 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])
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}
⊢ Disjoint (f i) (s.sup id)
have rw : Disjoint (f i) ((s.erase ⊥).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 _)
-- 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)
⊢ Disjoint (f i) (s.sup id)
have rw₄ : let t := s.erase ⊥;
∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.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 _)
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)
⊢ 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) (t.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 _)
Cleared hypotheses: hf