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 α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a
have simp_rw : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
Tactic: simp_rw [inf_comm _ a, h.inf_sSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i
have rw : a ⊓ sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), a ⊓ f i
Tactic: rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : a ⊓ sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), a ⊓ f i
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i
have rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, a ⊓ b) (⨆ (i : ι), a ⊓ f i)
Tactic: rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : a ⊓ sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), a ⊓ f i
rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, a ⊓ b) (⨆ (i : ι), a ⊓ f i)
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i
have rw₂ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), a ⊓ f i) (⨆ (i : ι), a ⊓ f i)
Tactic: rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
Tactic: rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, b ⊓ a) (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ range f, b ⊓ a) (⨆ (i : ι), f i ⊓ a)
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₂ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), f i ⊓ a) (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b
have simp_rw : a ⊓ sSup s = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → a ⊓ b = ⊥
Tactic: simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
simp_rw : a ⊓ sSup s = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → a ⊓ b = ⊥
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → a ⊓ b = ⊥
Tactic: simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
have simp_rw : sSup s ⊓ a = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
Tactic: simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
simp_rw : sSup s ⊓ a = ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, b ⊓ a) ⊥ ↔ ∀ ⦃b : α⦄, b ∈ s → b ⊓ a = ⊥
Tactic: simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
have simp_rw : a ⊓ ⨆ (i : ι), f i = ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
Tactic: simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
simp_rw : a ⊓ ⨆ (i : ι), f i = ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), a ⊓ f i) ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
Tactic: simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a
have simp_rw : (⨆ (i : ι), f i) ⊓ a = ⊥ ↔ ∀ (i : ι), f i ⊓ a = ⊥
Tactic: simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
f : ι → α
inst_1 : IsCompactlyGenerated α
a : α
h : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
simp_rw : (⨆ (i : ι), f i) ⊓ a = ⊥ ↔ ∀ (i : ι), f i ⊓ a = ⊥
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (⨆ (i : ι), f i ⊓ a) ⊥ ↔ ∀ (i : ι), f i ⊓ a = ⊥
Tactic: simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
have rw : ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
Tactic: rw [le_iff_compact_le_imp]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
have hc₁ : ∀ (s : Set α), c ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ c ≤ t.sup id
Tactic: rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc
Cleared hypotheses: hc, hcinf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ⊓ sSup s
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
have hcinf₁ : c ≤ a ∧ c ≤ sSup s
Tactic: rw [le_inf_iff] at hcinf
Cleared hypotheses: hcinf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
have rcases : ∀ (t : Finset α) (ht1 : (↑t : Set α) ⊆ s) (ht2 : c ≤ t.sup id),
  c ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
Tactic: rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have refine : a ⊓ t.sup id ≤ ⨆ (t : Finset α), ⨆ (_ : (↑t : Set α) ⊆ s), a ⊓ t.sup id
Tactic: refine (le_inf hcinf.1 ht2).trans ?_
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
⊢ Disjoint a (sSup (s \ {a}))
have rw : ∀ (i : Finset α), Eq.{u_2 + 1} (α := α) (⨆ (_ : (↑i : Set α) ⊆ s \ {a}), a ⊓ i.sup id) ⊥
Tactic: rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), (↑t : Set α) ⊆ s → sSupIndep (↑t : Set α)
a : α
ha : a ∈ s
t : Finset α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (_ : (↑t : Set α) ⊆ s \ {a}), a ⊓ t.sup id) ⊥
have rw : ∀ (i : (↑t : Set α) ⊆ s \ {a}), a ⊓ sSup (↑t : Set α) = ⊥
Tactic: rw [iSup_eq_bot, Finset.sup_id_eq_sSup]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ⊓ sSup (↑t : Set α) = ⊥
have refine_2 : ∀ (h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥), a ⊓ sSup (↑t : Set α) = ⊥
Tactic: have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 α) = ⊥
⊢ a ⊓ sSup (↑t : Set α) = ⊥
have refine_1 : (↑(insert a t) : Set α) ⊆ s
Tactic: have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ⊓ sSup (↑t : Set α) = ⊥
have refine_2 : ∀ (h' : a ⊓ sSup (insert a (↑t : Set α) \ {a}) = ⊥), a ∉ (↑t : Set α)
Tactic: rwa [Finset.coe_insert, Set.insert_diff_self_of_notMem] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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}
⊢ (↑(insert a t) : Set α) ⊆ s
have refine_1 : a ∈ s ∧ (↑t : Set α) ⊆ s
Tactic: rw [Finset.coe_insert, Set.insert_subset_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ⊓ sSup (↑t : Set α) = ⊥
have refine_1 : (↑(insert a t) : Set α) ⊆ s
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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ a ⊓ sSup (↑t : Set α) = ⊥
have refine_2 : ∀ (h' : a ⊓ sSup ((↑(insert a t) : Set α) \ {a}) = ⊥), 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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
⊢ 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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ InjOn f {i : ι | f i ≠ ⊥}
have by_contra! : ∀ (hf : ¬InjOn f {i : ι | f i ≠ ⊥}), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ≠ ⊥}
⊢ False
have hf₁ : ∃ (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]
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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : ∃ (x : ι) (_ : ¬f x = ⊥) (x_1 : ι) (_ : ¬f x_1 = ⊥) (_ : f x = f x_1), ¬x = x_1
⊢ False
have obtain : ∀ (x₁ : ι) (hx₁ : ¬f x₁ = ⊥) (x₂ : ι) (hx₂ : ¬f x₂ = ⊥) (hfeq : f x₁ = f x₂) (hneq : ¬x₁ = x₂), False
Tactic: obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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₂
⊢ False
have h₁ : Finset.SupIndep {x₁, x₂} f
Tactic: specialize h ({x₁, x₂} : Finset ι)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ False
have h₁ : f x₂ = ⊥
Tactic: rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 hf : 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
-- 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 : ι
hf : InjOn f {i : ι | 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 : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i : ι | 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 : ι → α
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
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 : ι → α
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
⊢ 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 : ι → α
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 ⊥
⊢ 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 : ι → α
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
have h₁ : ∀ (a : α), a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t
Tactic: ext a
-- 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 : ι
s : Finset α
hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' (↑t : Set α))
a : α
⊢ a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t
have h₁ : (∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a) ↔ ¬a = ⊥ ∧ a ∈ s
Tactic: simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]
-- 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 : ι
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
have 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
Tactic: refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
-- 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 : ι
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
⊢ ∃ (a_1 : ι), (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a
have 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
Tactic: obtain ⟨j, hj, rfl⟩ := hs has
Cleared hypotheses: a, h_1, ha, has
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 α))
⊢ Disjoint (f i) (t.sup id)
have this : 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⟩
-- 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 : ι
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
⊢ Disjoint (f i) (t.sup id)
have rw : Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
Tactic: rw [← this, Finset.sup_image]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
have h₁ : (insert i (t.preimage f hf)).SupIndep f
Tactic: specialize h (insert i (t.preimage _ hf))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
have h₁ : ∀ 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
Cleared hypotheses: h