awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
⊢ t j = ⊥
have ht₁ : Disjoint (t i) (t j)
Tactic: replace ht := (ht i).mono_right this
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
⊢ t j = ⊥
have rwa : ∀ (ht : Disjoint (t j) (t j)), t j = ⊥
Tactic: rwa [h, disjoint_self] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
ht : Disjoint (t i) (t j)
rwa : ∀ (ht : Disjoint (t j) (t j)), t j = ⊥
⊢ t j = ⊥
have rwa₁ : ∀ (ht : t j = ⊥), t j = ⊥
Tactic: rwa [h, disjoint_self] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥
have suffices : t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
Tactic: suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j ≤ ⨆ (k : ι), ⨆ (_ : k ≠ i), t k
have contra₁ : j ≠ i
Tactic: replace contra : j ≠ i := Ne.symm contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
⊢ b₁ = b₂
have by_contra : ∀ (h_ne : ¬b₁ = b₂), False
Tactic: by_contra h_ne
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
⊢ False
have obtain : ∀ (i : ι) (hi : b₁ i ≠ b₂ i), False
Tactic: obtain ⟨i, hi⟩ : ∃ i, b₁ i ≠ b₂ i := Function.ne_iff.mp h_ne
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₁
b₂ : (i : ι) → β i
hb₂ : Membership.mem (γ := Set ((i : ι) → β i)) {b : (i : ι) → β i | Ne.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b i)) ⊥} b₂
h_eq : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), t i (b₁ i)) (⨅ (i : ι), t i (b₂ i))
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
⊢ False
have this : LE.le.{u_1} (α := α) (⨅ (i : ι), t i (b₁ i)) ⊥
Tactic: have := calc
    ⨅ i, t i (b₁ i) ≤ t i (b₁ i) ⊓ t i (b₂ i) := le_inf (iInf_le ..) (h_eq ▸ iInf_le ..)
    _ = ⊥ := (ht i (b₁ i) |>.mono_right <| le_iSup₂_of_le (b₂ i) hi.symm le_rfl).eq_bot
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Injective t
have suffices : Eq.{u_3 + 1} (α := Set ι) univ {i : ι | t i ≠ ⊥}
Tactic: suffices univ = {i | t i ≠ ⊥} by simpa [← this] using ht.injOn
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep t ↔ Disjoint (t i) (t j)
have mp : iSupIndep t → Disjoint (t i) (t j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
mp : iSupIndep t → Disjoint (t i) (t j)
⊢ iSupIndep t ↔ Disjoint (t i) (t j)
have mpr : Disjoint (t i) (t j) → iSupIndep t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
have mpr : ∀ (hij : k ≠ j) (huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j) (h : Disjoint (t k) (t j)),
  Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
Tactic: obtain rfl | rfl := huniv k
Cleared hypotheses: i, hij, huniv, h
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
mpr :
  ∀ (hij : k ≠ j) (huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j) (h : Disjoint (t k) (t j)),
    Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
have mpr₁ : ∀ (hij : i ≠ k) (huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k) (h : Disjoint (t i) (t k)),
  Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
Tactic: obtain rfl | rfl := huniv k
Cleared hypotheses: j, hij, huniv, h
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
have mpr : ∀ (i : ι) (hi : i ≠ k), t i = t j
Tactic: refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j
have mpr : t j = t j
Tactic: rw [(huniv i).resolve_left hi]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)
have mpr : ∀ (j : ι) (hj : j ≠ k), t j = t i
Tactic: refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i
have mpr : t i = t i
Tactic: rw [(huniv j).resolve_right hj]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
⊢ ⨆ (i : Fin 3), f i = f 0 ⊔ f 1 ⊔ f 2
have suffices : ⨆ (i : Fin 3), ⨆ (_ : Membership.mem (γ := Finset (Fin 3)) Finset.univ i), f i = f 0 ⊔ f 1 ⊔ f 2
Tactic: suffices ⨆ i ∈ Finset.univ, f i = f 0 ⊔ f 1 ⊔ f 2 by simp [← this]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
⊢ ⨆ (i : Fin 3), ⨆ (_ : Membership.mem (γ := Finset (Fin 3)) Finset.univ i), f i = f 0 ⊔ f 1 ⊔ f 2
have rw : Finset.sup {0, 1, 2} f = f 0 ⊔ f 1 ⊔ f 2
Tactic: rw [← Finset.sup_eq_iSup, show (Finset.univ : Finset (Fin 3)) = {0, 1, 2} from rfl]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
⊢ iSupIndep f ↔ Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
have rw : (∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)) ↔
  Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
Tactic: rw [iSupIndep_def, sup_comm (f 2) (f 0)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
have refine_1 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 0) (f 1 ⊔ f 2)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
refine_1 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 0) (f 1 ⊔ f 2)
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
have refine_2 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 1) (f 0 ⊔ f 2)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
refine_1 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 0) (f 1 ⊔ f 2)
refine_2 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 1) (f 0 ⊔ f 2)
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
have refine_3 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 2) (f 0 ⊔ f 1)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
refine_1 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 0) (f 1 ⊔ f 2)
refine_2 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 1) (f 0 ⊔ f 2)
refine_3 : ∀ (h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)), Disjoint (f 2) (f 0 ⊔ f 1)
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
have refine_4 : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1) →
  ∀ (i : Fin 3) (h₀ : Disjoint (f 0) (f 1 ⊔ f 2)) (h₁ : Disjoint (f 1) (f 0 ⊔ f 2)) (h₂ : Disjoint (f 2) (f 0 ⊔ f 1)),
    Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
have refine_4 : Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨0, sorry⟩), f j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
refine_4 :
  Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩), f j)
⊢ Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
have refine_4₁ : Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨1, sorry⟩), f j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
refine_4 :
  Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩), f j)
refine_4₁ :
  Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩), f j)
⊢ Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
have refine_4₂ : Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨2, sorry⟩), f j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
a : α
t : ι → (↑(Iic a) : Type u_1)
ht : iSupIndep (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ t)
i : ι
x : (↑(Iic a) : Type u_1)
⊢ x ≤ t i → x ≤ ⨆ (j : ι), ⨆ (_ : j ≠ i), t j → x ≤ ⊥
have ht₁ : Disjoint ((Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ t) i)
  (⨆ (j : ι), ⨆ (_ : j ≠ i), (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ t) j)
Tactic: specialize ht i
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
a : α
t : ι → (↑(Iic a) : Type u_1)
i : ι
x : (↑(Iic a) : Type u_1)
ht :
  Disjoint ((Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ t) i)
    (⨆ (j : ι), ⨆ (_ : j ≠ i), (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) ∘ t) j)
⊢ x ≤ t i → x ≤ ⨆ (j : ι), ⨆ (_ : j ≠ i), t j → x ≤ ⊥
have ht₁ : Disjoint (↑(t i) : α) (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), t i_1) : α)
Tactic: simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have rw : iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
Tactic: rw [Finset.supIndep_iff_disjoint_erase]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
have refine : ∀ (a : ι) (b : a ∈ s),
  Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
    Disjoint (f a) ((s.erase a).sup f)
Tactic: refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
    Disjoint (f a) ((s.erase a).sup f)
have rw : Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
    (⨆ (j : ↥s),
      ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
  Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: rw [Finset.sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
    Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
have a₁ : Eq.{u_1 + 1} (α := α)
  (⨆ (j : ↥s), ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j)
  (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Eq.{u_1 + 1} (α := α)
    (⨆ (j : ↥s), ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j)
    (⨆ a_1 ∈ s.erase a, f a_1)
have a₁ : Eq.{u_1 + 1} (α := α)
  (⨆ (i : ι),
    ⨆ (h : i ∈ s),
      ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
  (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: refine iSup_subtype.trans ?_
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Eq.{u_1 + 1} (α := α)
    (⨆ (i : ι),
      ⨆ (h : i ∈ s),
        ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
          (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
    (⨆ a_1 ∈ s.erase a, f a_1)
have a₁ : Eq (α := ι → α)
  (fun (i : ι) ↦
    ⨆ (h : i ∈ s),
      ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
  fun (a_1 : ι) ↦ ⨆ (_ : a_1 ∈ s.erase a), f a_1
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have rw : iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
rw rw₁ rw₂ :
  iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have rw₃ : ∀ (a : ι) (b : a ∈ s),
  Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
    Disjoint (f a) ((s.erase a).sup f)
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
rw rw₁ rw₂ :
  iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
rw₃ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) ((s.erase a).sup f)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have rw₄ : ∀ (a : ι) (b : a ∈ s),
  Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
    Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
rw rw₁ rw₂ :
  iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
rw₃ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) ((s.erase a).sup f)
rw₄ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have a : ∀ (a : ι) (b : a ∈ s),
  Eq.{u_1 + 1} (α := α)
    (⨆ (j : ↥s), ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j)
    (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
rw rw₁ rw₂ :
  iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
rw₃ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) ((s.erase a).sup f)
rw₄ :
  ∀ (a : ι) (b : a ∈ s),
    Disjoint ((f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b))
        (⨆ (j : ↥s),
          ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j) ↔
      Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)
a :
  ∀ (a : ι) (b : a ∈ s),
    Eq.{u_1 + 1} (α := α)
      (⨆ (j : ↥s),
        ⨆ (_ : j ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b), (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) j)
      (⨆ a_1 ∈ s.erase a, f a_1)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep f
have a₁ : ∀ (a : ι) (b : a ∈ s),
  Eq.{u_1 + 1} (α := α)
    (⨆ (i : ι),
      ⨆ (h : i ∈ s),
        ⨆ (_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h ≠ Subtype.mk (p := fun (a : ι) ↦ a ∈ s) a b),
          (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h))
    (⨆ a_1 ∈ s.erase a, f a_1)
Tactic: classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]