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 : 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
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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)
Tactic: rw [← Finset.image_biUnion_filter_eq s (· i)]
-- 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₂
i : ι
hi : k₁ 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)
have 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)
Tactic: refine Finset.SupIndep.biUnion ?_ (by grind)
-- 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₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ 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)
have 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
Tactic: apply ((h_indep i).supIndep' _).mono
-- 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₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ (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
have 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
Tactic: simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
-- 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₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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)
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 _ _
-- 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₂
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)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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)
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 _ _
-- 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₂
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)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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
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 _ _
-- 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₂
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
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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
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 _ _
-- 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₂
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
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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)
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 _ _
-- 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)
⊢ s.SupIndep (α := α) fun (k : (i : ι) → κ i) ↦ ⨅ (i : ι), f i (k i)
have 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)
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 _ _
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have pos : ∀ (h : Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have neg : ∀ (h : ¬Subset (α := Set α) {c : α | IsCompactElement c ∧ c ≤ b} {⊥}), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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} {⊥}
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have pos : b = ⊥
Tactic: left
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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} {⊥}
⊢ b = ⊥
have pos : ∀ (a : α), Membership.mem (γ := Set α) {c : α | IsCompactElement c ∧ c ≤ b} a → a = ⊥
Tactic: rw [← sSup_compact_le_eq b, sSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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} {⊥}
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have neg : ∀ (c : α) (hcbot : c ∉ {⊥}) (hc : IsCompactElement c) (hcb : c ≤ b), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have neg : ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: right
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have hc' : IsCoatomic.{u_2} (↑(Iic c) : Type u_2)
Tactic: have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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)
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have hc'₁ : IsAtomic.{u_2} (↑(Iic c) : Type u_2)
Tactic: rw [← isAtomic_iff_isCoatomic] at hc'
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : α), IsAtom a ∧ a ≤ b
have neg : ∀
  (con :
    Eq (α := { x : α // x ∈ Iic c }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c sorry : { x : α // x ∈ Iic c })
      (⊥ : { x : α // x ∈ Iic c })),
  ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have neg₁ : ∀ (a : { x : α // x ∈ Iic c }) (ha : IsAtom a) (hac : a ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c sorry),
  ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 })
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 })
⊢ False
have neg : Membership.mem (γ := Set α) {⊥} c
Tactic: apply hcbot
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 })
⊢ Membership.mem (γ := Set α) {⊥} c
have con₁ : c = ⊥
Tactic: simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 : α), IsAtom a ∧ a ≤ b
have hac₁ : (↑a : α) ≤ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic c) c sorry : { x : α // x ∈ Iic c }) : α)
Tactic: rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
Cleared hypotheses: hac
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
⊢ b = sSup {a : α | IsAtom a ∧ a ≤ b}
have symm : sSup {a : α | IsAtom a ∧ a ≤ b} = b
Tactic: symm
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
⊢ sSup {a : α | IsAtom a ∧ a ≤ b} = b
have hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
Tactic: have hle : sSup { a : α | IsAtom a ∧ a ≤ b } ≤ b := sSup_le fun _ => And.right
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
⊢ sSup {a : α | IsAtom a ∧ a ≤ b} = b
have apply : ¬sSup {a : α | IsAtom a ∧ a ≤ b} < b
Tactic: apply (lt_or_eq_of_le hle).resolve_left _
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
⊢ False
have obtain : ∀ (c : { x : α // x ∈ Iic b })
  (hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c), False
Tactic: obtain ⟨c, hc⟩ := exists_isCompl (⟨sSup { a : α | IsAtom a ∧ a ≤ b }, hle⟩ : Set.Iic b)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
⊢ False
have inl : ∀ (hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) ⊥), False
Tactic: obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
inl : ∀ (hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) ⊥), False
⊢ False
have inr : ∀ (a : { x : α // x ∈ Iic b }) (ha : IsAtom a) (hac : a ≤ c), False
Tactic: obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ False
have inr : a = ⊥
Tactic: apply ha.1
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsModularLattice α
inst_2 : IsCompactlyGenerated α
inst_3 : ComplementedLattice α
b : α
hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a : α | IsAtom a ∧ a ≤ b} < b
c : { x : α // x ∈ Iic b }
hc : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (sSup {a : α | IsAtom a ∧ a ≤ b}) hle) c
a : { x : α // x ∈ Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a = ⊥
have inr : a ≤ ⊥
Tactic: rw [eq_bot_iff]