awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
rcases :
  ∀ (t : Finset α) (ht1 : (↑t : Set α) ⊆ s) (ht2 : c ≤ t.sup id),
    c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩

Premises used: And.right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : (↑t : Set α) ⊆ s
ht2 : c ≤ t.sup id
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
(le_inf hcinf.1 ht2).trans ?_

Premises used: le_inf, And.left, LE.le.trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : (↑t : Set α) ⊆ s
ht2 : c ≤ t.sup id
refine : a ⊓ t.sup id ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
refine (le_inf hcinf.1 ht2).trans ?_

Premises used: le_inf, And.left, LE.le.trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : (↑t : Set α) ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
le_iSup₂ (f := fun (t' : Finset α) (ht' : ↑t' ⊆ s) => a ⊓ t'.sup id) t ht1

Premises used: le_iSup₂
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : (↑t : Set α) ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id

Tactic:
exact le_iSup₂ (f := fun (t' : Finset α) (ht' : ↑t' ⊆ s) => a ⊓ t'.sup id) t ht1

Premises used: le_iSup₂
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
rw : ∀ (i : Finset α), Eq.{u_2 + 1} (α := α) (⨆ (_ : (↑i : Set α) ⊆ s \ {a}), a ⊓ i.sup id) ⊥
⊢ Disjoint a (sSup (s \ {a}))

Tactic:
rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]

Premises used: disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
rw : ∀ (i : (↑t : Set α) ⊆ s \ {a}), a ⊓ sSup (↑t : Set α) = ⊥
⊢ Eq.{u_2 + 1} (α := α) (⨆ (_ : (↑t : Set α) ⊆ s \ {a}), a ⊓ t.sup id) ⊥

Tactic:
rw [iSup_eq_bot, Finset.sup_id_eq_sSup]

Premises used: iSup_eq_bot, Finset.sup_id_eq_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
refine_2 : ∀ (h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥), a ⊓ sSup (↑t : Set α) = ⊥
refine_1 : (↑(insert a t) : Set α) ⊆ s
⊢ a ⊓ sSup (↑t : Set α) = ⊥

Tactic:
have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥
refine_2 : ∀ (h' : a ⊓ sSup (insert a (↑t : Set α) \ {a}) = ⊥), a ∉ (↑t : Set α)
⊢ a ⊓ sSup (↑t : Set α) = ⊥

Tactic:
rwa [Finset.coe_insert, Set.insert_diff_self_of_notMem] at h'

Premises used: Set.insert_diff_self_of_notMem, Finset.coe_insert
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
h' : a ⊓ sSup (insert a (↑t : Set α) \ {a}) = ⊥
⊢ a ∉ (↑t : Set α)

Tactic:
fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)

Premises used: Set.mem_singleton, And.right, Set.mem_diff, Iff.mp, Not
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
h' : a ⊓ sSup (insert a (↑t : Set α) \ {a}) = ⊥
⊢ a ∉ (↑t : Set α)

Tactic:
exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)

Premises used: Set.mem_singleton, And.right, Set.mem_diff, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
refine_1 : a ∈ s ∧ (↑t : Set α) ⊆ s
⊢ (↑(insert a t) : Set α) ⊆ s

Tactic:
rw [Finset.coe_insert, Set.insert_subset_iff]

Premises used: Set.insert_subset_iff, Finset.coe_insert
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
⊢ a ∈ s ∧ (↑t : Set α) ⊆ s

Tactic:
⟨ha, Set.Subset.trans ht diff_subset⟩

Premises used: Set.diff_subset, Set.Subset.trans, And.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
⊢ a ∈ s ∧ (↑t : Set α) ⊆ s

Tactic:
exact ⟨ha, Set.Subset.trans ht diff_subset⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
ht : (↑t : Set α) ⊆ s \ {a}
refine_1 : (↑(insert a t) : Set α) ⊆ s
refine_2 : ∀ (h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥), a ⊓ sSup (↑t : Set α) = ⊥
refine_1₁ : (↑(insert a t) : Set α) ⊆ s
refine_2₁ refine_2₂ : ∀ (h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥), a ⊓ sSup (↑t : Set α) = ⊥
refine_1₂ refine_1₃ : (↑(insert a t) : Set α) ⊆ s
⊢ a ⊓ sSup (↑t : Set α) = ⊥

Tactic:
classical
      have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
      · rwa [Finset.coe_insert, Set.insert_diff_self_of_notMem] at h'
        exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)
      · rw [Finset.coe_insert, Set.insert_subset_iff]
        exact ⟨ha, Set.Subset.trans ht diff_subset⟩

Premises used: Set.mem_singleton, Set.insert_subset_iff, Set.insert_diff_self_of_notMem, And.right, Set.mem_diff, Iff.mp, Finset.coe_insert
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩

Premises used: Iff.mpr, iSupIndep.supIndep', iSupIndep_def', Iff.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
refine : ∀ (h : ∀ (s : Finset ι), s.SupIndep f) (i : ι), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
by_contra! : ∀ (hf : ¬InjOn f {i : ι | f i ≠ ⊥}), False
⊢ InjOn f {i : ι | f i ≠ ⊥}

Tactic:
by_contra! hf
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : ¬InjOn f {i : ι | f i ≠ ⊥}
⊢ ∃ (x : ι) (_ : ¬f x = ⊥) (x_1 : ι) (_ : ¬f x_1 = ⊥) (_ : f x = f x_1), ¬x = x_1

Tactic:
simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]

Premises used: Set.mem_setOf_eq, ne_eq, Set.InjOn, Classical.not_forall
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : ∃ (x : ι) (_ : ¬f x = ⊥) (x_1 : ι) (_ : ¬f x_1 = ⊥) (_ : f x = f x_1), ¬x = x_1
obtain : ∀ (x₁ : ι) (hx₁ : ¬f x₁ = ⊥) (x₂ : ι) (hx₂ : ¬f x₂ = ⊥) (hfeq : f x₁ = f x₂) (hneq : ¬x₁ = x₂), False
⊢ False

Tactic:
obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
⊢ Finset.SupIndep {x₁, x₂} f

Tactic:
specialize h ({x₁, x₂} : Finset ι)

Premises used: Insert.insert, Singleton.singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
h : Finset.SupIndep {x₁, x₂} f
⊢ f x₂ = ⊥

Tactic:
rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h

Premises used: disjoint_iff, Finset.supIndep_pair, inf_idem
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i x₁ : ι
hx₁ : ¬f x₁ = ⊥
x₂ : ι
hx₂ : ¬f x₂ = ⊥
hfeq : f x₁ = f x₂
hneq : ¬x₁ = x₂
h : f x₂ = ⊥
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ InjOn f {i : ι | f i ≠ ⊥}

Tactic:
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
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
simp_rw : ∀ (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}), Disjoint (f i) (i_1.sup id)
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))

Tactic:
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]

Premises used: disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
rw : Disjoint (f i) ((s.erase ⊥).sup id)
⊢ Disjoint (f i) (s.sup id)

Tactic:
rw [← Finset.sup_erase_bot]

Premises used: Finset.sup_erase_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i : ι | 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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i_1 : ι
hf : InjOn f {i : ι | f i ≠ ⊥}
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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i : ι | 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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
h₁ : ∀ (a : α), a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t
⊢ Finset.image f ((insert i (t.preimage f hf)).erase i) = t

Tactic:
ext a
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
a : α
h₁ : (∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) ↔ ¬a = ⊥ ∧ a ∈ s
⊢ a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t

Tactic:
simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]

Premises used: Finset.mem_image, ne_eq, Finset.mem_erase, Finset.mem_preimage, Finset.erase_insert_eq_erase
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
a : α
⊢ (∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) → ¬a = ⊥ ∧ a ∈ s

Tactic:
aesop
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
a : α
h₁ : ¬a = ⊥ ∧ a ∈ s → ∀ (ha : ¬a = ⊥) (has : a ∈ s), ∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a
⊢ (∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) ↔ ¬a = ⊥ ∧ a ∈ s

Tactic:
refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
a : α
h_1 : ¬a = ⊥ ∧ a ∈ s
ha : ¬a = ⊥
has : a ∈ s
h₁ :
  ∀ (j : ι) (hj : Membership.mem (γ := Set ι) {j : ι | j ≠ i} j),
    ¬f j = ⊥ ∧ f j ∈ s → ∀ (ha : ¬f j = ⊥) (has : f j ∈ s), ∃ (a : ι), (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j
⊢ ∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a

Tactic:
obtain ⟨j, hj, rfl⟩ := hs has

Premises used: rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
j : ι
hj : Membership.mem (γ := Set ι) {j : ι | j ≠ i} j
h_1 : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ (a : ι), (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j

Tactic:
⟨j, ⟨hj, ha, has⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
j : ι
hj : Membership.mem (γ := Set ι) {j : ι | j ≠ i} j
h_1 : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ (a : ι), (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j

Tactic:
exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
⊢ Finset.image f ((insert i (t.preimage f hf)).erase i) = t

Tactic:
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⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
rw : Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
⊢ Disjoint (f i) (t.sup id)

Tactic:
rw [← this, Finset.sup_image]

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

Tactic:
specialize h (insert i (t.preimage _ hf))

Premises used: Insert.insert, Finset.preimage
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := 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
⊢ ∀ i_1 ∈ insert i (t.preimage f hf), Disjoint (f i_1) (((insert i (t.preimage f hf)).erase i_1).sup f)

Tactic:
rw [Finset.supIndep_iff_disjoint_erase] at h

Premises used: Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := 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:
h i (Finset.mem_insert_self i _)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := 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:
exact h i (Finset.mem_insert_self i _)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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

Tactic:
⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩

Premises used: Iff.mpr, iSupIndep.supIndep', iSupIndep_def', Iff.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i : ι | f i ≠ ⊥}
refine : ∀ (h : ∀ (s : Finset ι), s.SupIndep f) (i : ι), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
-- 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 : ι
simp_rw : ∀ (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}), Disjoint (f i) (i_1.sup id)
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))

Tactic:
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]

Premises used: disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot
-- 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 : Disjoint (f i) ((s.erase ⊥).sup id)
⊢ Disjoint (f i) (s.sup id)

Tactic:
rw [← Finset.sup_erase_bot]

Premises used: Finset.sup_erase_bot