awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : ∀ z ∈ S, z ≤ sSup S
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩
-- 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
z : α
⊢ z ∈ S → z ≤ sSup S

Tactic:
apply le_sSup

Premises used: le_sSup
-- 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
⊢ ∀ z ∈ S, z ≤ b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]

Premises used: Set.not_nonempty_iff_eq_empty, forall_prop_of_false, Iff.mp, Set.mem_empty_iff_false, forall_const, not_false_iff
-- 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:
exact
      ⟨b, lt_of_le_of_ne hbk H, by
        simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsCompactElement.{u_2} (α := α) ⊤
⊢ IsCoatomic α

Tactic:
(@OrderIso.IicTop α _ _).isCoatomic_iff.mp (Iic_coatomic_of_compact_element h)

Premises used: CompleteLattice.Iic_coatomic_of_compact_element, OrderIso.isCoatomic_iff, Iff.mp, OrderIso.IicTop
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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)
rw : ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ iSupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
rw [iSupIndep_iff_supIndep]

Premises used: iSupIndep_iff_supIndep
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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)
neg : ∀ (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)

Tactic:
by_cases hs : 1 < s.card

Premises used: Finset.card
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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)
neg : ∀ (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)

Tactic:
by_cases hcard0 : s.card = 0

Premises used: Finset.card
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
hcard0 : s.card = 0
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
grind [Finset.card_eq_zero, Finset.card_eq_one]

Premises used: Finset.card_eq_one, Finset.card_eq_zero
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
hcard0 : ¬s.card = 0
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
grind [Finset.card_eq_zero, Finset.card_eq_one]

Premises used: Finset.card_eq_one, Finset.card_eq_zero
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 :
  ∀ (k₁ k₂ : (i : ι) → κ i),
    k₁ ∈ s → k₂ ∈ s → ∀ (h : k₁ ≠ k₂), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs

Premises used: Finset.one_lt_card_iff, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
⊢ ∃ (i : ι), k₁ i ≠ k₂ i

Tactic:
Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
pos : ∀ (i : ι) (hi : k₁ i ≠ k₂ i), s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f 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

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
pos :
  Finset.SupIndep (α := α)
    (Finset.biUnion (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (a : κ i) ↦ {c ∈ s | c i = a})
    fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
rw [← Finset.image_biUnion_filter_eq s (· i)]

Premises used: Finset.image_biUnion_filter_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ (i' : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i' →
      {c ∈ s | c i = i'}.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
grind
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
pos :
  Finset.SupIndep.{u_2, u_4} (α := α) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (i_1 : κ i) ↦
    {c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
⊢ Finset.SupIndep (α := α)
    (Finset.biUnion (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (a : κ i) ↦ {c ∈ s | c i = a})
    fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
refine Finset.SupIndep.biUnion ?_ (by grind)

Premises used: Finset.SupIndep.biUnion
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
pos :
  ∀ (i_1 : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i_1 →
      ({c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)) ≤ f i i_1
⊢ Finset.SupIndep.{u_2, u_4} (α := α) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (i_1 : κ i) ↦
    {c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
apply ((h_indep i).supIndep' _).mono

Premises used: Finset.SupIndep.mono, iSupIndep.supIndep'
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
pos :
  ∀ (i_1 : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i_1 →
      ∀ b ∈ s, b i = i_1 → ⨅ (i : ι), f i (b i) ≤ f i i_1
⊢ ∀ (i_1 : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i_1 →
      ({c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)) ≤ f i i_1

Tactic:
simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]

Premises used: and_imp, Finset.sup_le_iff, Finset.mem_filter
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
b : (i : ι) → κ i
h_1 : b ∈ s
h_2 : Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) (b i)
⊢ ⨅ (i : ι), f i (b i) ≤ f i (b i)

Tactic:
iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
b : (i : ι) → κ i
h_1 : b ∈ s
h_2 : Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) (b i)
⊢ ⨅ (i : ι), f i (b i) ≤ f i (b i)

Tactic:
exact iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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₂
i : ι
hi : k₁ i ≠ k₂ i
pos pos₁ pos₂ :
  Finset.SupIndep (α := α)
    (Finset.biUnion (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (a : κ i) ↦ {c ∈ s | c i = a})
    fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
pos₃ :
  Finset.SupIndep.{u_2, u_4} (α := α) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) fun (i_1 : κ i) ↦
    {c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
pos₄ :
  ∀ (i_1 : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i_1 →
      ({c ∈ s | c i = i_1}.sup fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)) ≤ f i i_1
pos₅ :
  ∀ (i_1 : κ i),
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) i_1 →
      ∀ b ∈ s, b i = i_1 → ⨅ (i : ι), f i (b i) ≤ f i i_1
pos₆ :
  ∀ b ∈ s,
    Membership.mem (γ := Finset (κ i)) (Finset.image (fun (x : (i : ι) → κ i) ↦ x i) s) (b i) →
      ⨅ (i : ι), f i (b i) ≤ f i (b i)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
classical
      rw [← Finset.image_biUnion_filter_eq s (· i)]
      refine Finset.SupIndep.biUnion ?_ (by grind)
      apply ((h_indep i).supIndep' _).mono
      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
      rintro _ _ _ _ rfl
      exact iInf_le _ _

Premises used: and_imp, Finset.SupIndep.mono, iSupIndep.supIndep', Finset.SupIndep.biUnion, Finset.sup_le_iff, Finset.mem_filter, iInf_le, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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)
H :
  ∀ (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)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)

Tactic:
induction s using Finset.strongInduction with
  | H s ih =>
    by_cases hs : 1 < s.card; swap
    · by_cases hcard0 : s.card = 0 <;> grind [Finset.card_eq_zero, Finset.card_eq_one]
    · obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs
      obtain ⟨i, hi⟩ : ∃ i : ι, k₁ i ≠ k₂ i := Function.ne_iff.mp h
      classical
      rw [← Finset.image_biUnion_filter_eq s (· i)]
      refine Finset.SupIndep.biUnion ?_ (by grind)
      apply ((h_indep i).supIndep' _).mono
      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
      rintro _ _ _ _ rfl
      exact iInf_le _ _

Premises used: Finset.card_eq_one, and_imp, Finset.card_eq_zero, Finset.SupIndep.biUnion, Finset.card, Finset.sup_le_iff, Finset.mem_filter, Finset.strongInduction, iInf_le, rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
pos : ∀ (h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
neg : ∀ (h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
pos : b = ⊥
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
left
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
pos : ∀ (a : α), Membership.mem (γ := Set α) {c : α | IsCompactElement c ∧ c ≤ b} a → a = ⊥
⊢ b = ⊥

Tactic:
rw [← sSup_compact_le_eq b, sSup_eq_bot]

Premises used: sSup_eq_bot, sSup_compact_le_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
⊢ ∀ (a : α), Membership.mem (γ := Set α) {c : α | IsCompactElement c ∧ c ≤ b} a → a = ⊥

Tactic:
h

Premises used: Set.Mem, setOf, Set.Subset, Set.singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
⊢ ∀ (a : α), Membership.mem (γ := Set α) {c : α | IsCompactElement c ∧ c ≤ b} a → a = ⊥

Tactic:
exact h
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
neg : ∀ (c : α) (hcbot : c ∉ {⊥}) (hc : IsCompactElement c) (hcb : c ≤ b), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
neg : ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
⊢ IsCoatomic.{u_2} (↑(Iic c) : Type u_2)

Tactic:
have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsCoatomic.{u_2} (↑(Iic c) : Type u_2)
⊢ IsAtomic.{u_2} (↑(Iic c) : Type u_2)

Tactic:
rw [← isAtomic_iff_isCoatomic] at hc'

Premises used: isAtomic_iff_isCoatomic
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
neg :
  ∀
    (con :
      Eq (α := { x : α // x ∈ Iic c }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c })
        (⊥ : { x : α // x ∈ Iic c })),
    ∃ (a : α), IsAtom a ∧ a ≤ b
neg₁ :
  ∀ (a : { x : α // x ∈ Iic c }) (ha : IsAtom a) (hac : a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯),
    ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)

Premises used: le_refl, IsAtomic.eq_bot_or_exists_atom_le, Subtype.mk
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
con :
  Eq (α := { x : α // x ∈ Iic c }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c })
    (⊥ : { x : α // x ∈ Iic c })
neg : False
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
exfalso
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
con :
  Eq (α := { x : α // x ∈ Iic c }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c })
    (⊥ : { x : α // x ∈ Iic c })
neg : Membership.mem (γ := Set α) {⊥} c
⊢ False

Tactic:
apply hcbot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
con :
  Eq (α := { x : α // x ∈ Iic c }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c })
    (⊥ : { x : α // x ∈ Iic c })
⊢ c = ⊥

Tactic:
simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con

Premises used: Subtype.ext_iff, Set.Iic.coe_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
con : c = ⊥
⊢ Membership.mem (γ := Set α) {⊥} c

Tactic:
con

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
con : c = ⊥
⊢ Membership.mem (γ := Set α) {⊥} c

Tactic:
exact con
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
a : { x : α // x ∈ Iic c }
ha : IsAtom a
hac : a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯
⊢ (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c ⋯ : { x : α // x ∈ Iic c }) : α)

Tactic:
rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac

Premises used: Subtype.coe_mk, Subtype.coe_le_coe