awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupIndep
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)

Tactic:
h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)

Premises used: Eq.le, Disjoint.symm, iSup_le, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
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)
mpr : ∀ (j : ι) (hj : j ≠ k), t j = t i
⊢ Disjoint (t k) (⨆ (j : ι), ⨆ (_ : j ≠ k), t j)

Tactic:
refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)

Premises used: Eq.le, Disjoint.symm, iSup_le, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
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
mpr mpr₁ : t i = t i
⊢ t j = t i

Tactic:
rw [(huniv j).resolve_right hj]

Premises used: Or.resolve_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
this : ⨆ (i : Fin 3), ⨆ (_ : Membership.mem (γ := Finset (Fin 3)) Finset.univ i), f i = f 0 ⊔ f 1 ⊔ f 2
⊢ ⨆ (i : Fin 3), f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
simp [← this]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
suffices : ⨆ (i : Fin 3), ⨆ (_ : Membership.mem (γ := Finset (Fin 3)) Finset.univ i), f i = f 0 ⊔ f 1 ⊔ f 2
⊢ ⨆ (i : Fin 3), f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
suffices ⨆ i ∈ Finset.univ, f i = f 0 ⊔ f 1 ⊔ f 2 by simp [← this]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
rw : Finset.sup {0, 1, 2} f = f 0 ⊔ f 1 ⊔ f 2
⊢ ⨆ (i : Fin 3), ⨆ (_ : Membership.mem (γ := Finset (Fin 3)) Finset.univ i), f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
rw [← Finset.sup_eq_iSup, show (Finset.univ : Finset (Fin 3)) = {0, 1, 2} from rfl]

Premises used: Finset.sup_eq_iSup, rfl
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
⊢ Finset.sup {0, 1, 2} f = f 0 ⊔ f 1 ⊔ f 2

Tactic:
simp [sup_assoc]

Premises used: sup_assoc
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
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)
⊢ iSupIndep f ↔ Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
rw [iSupIndep_def, sup_comm (f 2) (f 0)]

Premises used: sup_comm, iSupIndep_def, OfNat.ofNat
-- Module: Mathlib.Order.SupIndep
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)

Tactic:
⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩

Premises used: _private.0.iSupIndep_fin_three.match_1, iSup, Disjoint, And.intro, Iff.intro
-- Module: Mathlib.Order.SupIndep
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)
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)
⊢ (∀ (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:
refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun ⟨h₀, h₁, h₂⟩ i ↦ ?_⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 0) (f 1 ⊔ f 2)

Tactic:
simpa using h 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_5
inst : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
simpa using h 2

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.SupIndep
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)
refine_4₂ :
  Disjoint (f ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩), f j)
⊢ Disjoint (f i) (⨆ (j : Fin 3), ⨆ (_ : j ≠ i), f j)

Tactic:
fin_cases i
-- Module: Mathlib.Order.SupIndep
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)
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 ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩), f j)

Tactic:
simpa
-- Module: Mathlib.Order.SupIndep
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)
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 ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩), f j)

Tactic:
simpa
-- Module: Mathlib.Order.SupIndep
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)
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 ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (⨆ (j : Fin 3), ⨆ (_ : j ≠ (fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩), f j)

Tactic:
simpa
-- Module: Mathlib.Order.SupIndep
Goal:
ι : Sort u_5
α : Type u_6
β : Type u_7
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
a : ι → α
ha : iSupIndep a
⊢ iSupIndep.{u_5, u_7} (α := β) ((⇑f : (a : α) → β) ∘ a)

Tactic:
fun i => ((ha i).map_orderIso f).mono_right (f.monotone.le_map_iSup₂ _)

Premises used: OrderIso.monotone, iSupIndep, Monotone.le_map_iSup₂, Disjoint.map_orderIso, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
ι : Sort u_5
α : Type u_6
β : Type u_7
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
a : ι → α
⊢ iSupIndep.{u_5, u_7} (α := β) ((⇑f : (a : α) → β) ∘ a) ↔ iSupIndep a

Tactic:
⟨fun h =>
    have hf : f.symm ∘ f ∘ a = a := congr_arg (· ∘ a) f.left_inv.comp_eq_id
    hf ▸ h.map_orderIso f.symm,
    fun h => h.map_orderIso f⟩

Premises used: Function.comp, Eq.rec, OrderIso.symm, congr_arg, Iff.intro, Function.LeftInverse.comp_eq_id, RelIso.toEquiv, iSupIndep.map_orderIso, Equiv.left_inv
-- Module: Mathlib.Order.SupIndep
Goal:
ι : Type u_5
α : Type u_6
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
x : ι
y : Set ι
hx : x ∉ y
⊢ Disjoint (t x) (⨆ i ∈ y, t i)

Tactic:
Disjoint.mono_right (biSup_mono fun _ hi => (ne_of_mem_of_not_mem hi hx :)) (ht x)

Premises used: biSup_mono, ne_of_mem_of_not_mem, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
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)
⊢ 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
-- Module: Mathlib.Order.SupIndep
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)
⊢ Disjoint (↑(t i) : α) (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), t i_1) : α)

Tactic:
simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht

Premises used: Set.Iic.coe_iSup, Function.comp_apply
-- Module: Mathlib.Order.SupIndep
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 (↑(t i) : α) (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), t i_1) : α)
⊢ x ≤ t i → x ≤ ⨆ (j : ι), ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
@ht x
-- Module: Mathlib.Order.SupIndep
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 (↑(t i) : α) (↑(⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), t i_1) : α)
⊢ x ≤ t i → x ≤ ⨆ (j : ι), ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
exact @ht x
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
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

Tactic:
rw [Finset.supIndep_iff_disjoint_erase]

Premises used: Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.SupIndep
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)

Tactic:
Subtype.forall.trans (forall₂_congr fun a b => ?_)

Premises used: iSupIndep, Subtype.forall, forall₂_congr, Iff.trans
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
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)
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Tactic:
refine Subtype.forall.trans (forall₂_congr fun a b => ?_)

Premises used: Subtype.forall, forall₂_congr, Iff.trans
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
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)
⊢ 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:
rw [Finset.sup_eq_iSup]

Premises used: Finset.sup_eq_iSup
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
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)
⊢ 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:
congr! 1
-- Module: Mathlib.Order.SupIndep
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)

Tactic:
iSup_subtype.trans ?_

Premises used: iSup_subtype, Eq.trans
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
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)
⊢ 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:
refine iSup_subtype.trans ?_

Premises used: iSup_subtype, Eq.trans
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
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
⊢ 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:
congr! 1
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ 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:
simp [iSup_and, @iSup_comm _ (_ ∈ s)]

Premises used: iSup_comm, iSup_and
-- Module: Mathlib.Order.SupIndep
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)
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)
a₂ :
  ∀ (a : ι) (b : a ∈ s),
    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
⊢ iSupIndep (ι := ↥s) (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ s.SupIndep 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)]

Premises used: iSup_subtype, iSup_comm, Subtype.forall, Finset.sup_eq_iSup, forall₂_congr, Finset.supIndep_iff_disjoint_erase, Iff.trans, Eq.trans, iSup_and
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
f : ι → α
s : Finset ι
h : iSupIndep f
⊢ s.SupIndep f

Tactic:
iSupIndep.supIndep (h.comp Subtype.coe_injective)

Premises used: iSupIndep.comp, iSupIndep.supIndep, Subtype.coe_injective
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : Fintype ι
f : ι → α
⊢ iSupIndep f ↔ Finset.SupIndep Finset.univ f

Tactic:
simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Premises used: iSupIndep, Finset.sup_eq_iSup, Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : Fintype ι
f : ι → α
⊢ iSupIndep f ↔ Finset.SupIndep Finset.univ f

Tactic:
classical
    simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Premises used: iSupIndep, Finset.sup_eq_iSup, Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
⊢ f ≤ g ↔ f = g

Tactic:
⟨fun h₃ ↦ funext fun i ↦ ?_, le_of_eq⟩

Premises used: funext, Iff.intro, le_of_eq
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
refine : ∀ (h₃ : f ≤ g) (i : ι), f i = g i
⊢ f ≤ g ↔ f = g

Tactic:
refine ⟨fun h₃ ↦ funext fun i ↦ ?_, le_of_eq⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
⊢ Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)

Tactic:
replace h₁ : Disjoint (⨆ (j) (_ : j ≠ i), f j) (g i) :=
    Disjoint.mono_left (iSup₂_mono fun j _ ↦ h₃ j) (h₁ i).symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
rw : f i ⊔ ⨆ (j : ι), ⨆ (_ : j ≠ i), f j = ⊤
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)

Tactic:
rw [codisjoint_iff, ← iSup_split_single f i, h₂]

Premises used: codisjoint_iff, iSup_split_single
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
⊢ Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)

Tactic:
replace h₂ : Codisjoint (f i) (⨆ (j) (_ : j ≠ i), f j) := by
    rw [codisjoint_iff, ← iSup_split_single f i, h₂]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
h₂ : Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)
⊢ f i = g i

Tactic:
(le_iff_eq_of_codisjoint_of_disjoint h₂ h₁).mp (h₃ i)

Premises used: le_iff_eq_of_codisjoint_of_disjoint, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f g : ι → α
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ (j : ι), ⨆ (_ : j ≠ i), f j) (g i)
h₂ : Codisjoint (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)
⊢ f i = g i

Tactic:
exact (le_iff_eq_of_codisjoint_of_disjoint h₂ h₁).mp (h₃ i)

Premises used: le_iff_eq_of_codisjoint_of_disjoint, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this : ∀ (s : Finset ι) (hst : Disjoint (↑s : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
⊢ ∀ (hst : Disjoint (↑(hs.toFinset (s := s)) : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ i ∈ hs.toFinset (s := s), f i) (⨆ i ∈ t, f i)

Tactic:
specialize this hs.toFinset

Premises used: Set.Finite.toFinset
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this :
  ∀ (hst : Disjoint (↑(hs.toFinset (s := s)) : Set ι) t),
    Disjoint.{u_1} (α := α) (⨆ i ∈ hs.toFinset (s := s), f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
suffices : ∀ (s : Finset ι) (hst : Disjoint (↑s : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
suffices ∀ (s : Finset ι) (hst : Disjoint ↑s t), Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i) by
    specialize this hs.toFinset
    aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
t : Set ι
hst : Disjoint (↑∅ : Set ι) t
⊢ Disjoint.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) (⨆ i ∈ t, f i)

Tactic:
simp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
⊢ j ∉ t

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
⊢ j ∉ t

Tactic:
have hjt : j ∉ t := by aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
hjt : j ∉ t
⊢ Disjoint (↑s₀ : Set ι) (insert j t)

Tactic:
aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hst : Disjoint (↑(insert j s₀) : Set ι) t
hjt : j ∉ t
⊢ Disjoint (↑s₀ : Set ι) (insert j t)

Tactic:
replace hst : Disjoint ↑s₀ (insert j t) := by aesop
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
inst_1 : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
ih : ∀ {t : Set ι} (hst : Disjoint (↑s₀ : Set ι) t), Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ t, f i)
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀ : Set ι) (insert j t)
⊢ Disjoint.{u_1} (α := α) (⨆ i ∈ s₀, f i) (⨆ i ∈ insert j t, f i)

Tactic:
specialize ih hst