awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
f : ι → α
hs : s.SupIndep f
x : ι
u : Finset ι
hx : x ∉ u
ih : ∀ {v : Finset ι} (hu : u ⊆ s) (hv : v ⊆ s) (huv : Disjoint u v), Disjoint (u.sup f) (v.sup f)
v : Finset ι
hu : insert x u ⊆ s
hv : v ⊆ s
huv : Disjoint (insert x u) v
⊢ Disjoint ((insert x u).sup f) (v.sup f)

Tactic:
grind [= SupIndep, Disjoint.disjoint_sup_left_of_disjoint_sup_right]

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
f : ι → α
u v : Finset ι
hs : s.SupIndep f
hu : u ⊆ s
hv : v ⊆ s
huv : Disjoint u v
empty : ∀ {v : Finset ι} (hu : ∅ ⊆ s) (hv : v ⊆ s) (huv : Disjoint ∅ v), Disjoint (sup ∅ f) (v.sup f)
insert :
  ∀ (x : ι) (u : Finset ι) (hx : x ∉ u)
    (ih : ∀ {v : Finset ι} (hu : u ⊆ s) (hv : v ⊆ s) (huv : Disjoint u v), Disjoint (u.sup f) (v.sup f)) {v : Finset ι}
    (hu : Insert.insert x u ⊆ s) (hv : v ⊆ s) (huv : Disjoint (Insert.insert x u) v),
    Disjoint ((Insert.insert x u).sup f) (v.sup f)
⊢ Disjoint (u.sup f) (v.sup f)

Tactic:
induction u using Finset.induction generalizing v with
  | empty => simp
  | insert x u hx ih =>
    grind [= SupIndep, Disjoint.disjoint_sup_left_of_disjoint_sup_right]

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, Insert.insert, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
f : ι → α
u v : Finset ι
hs : s.SupIndep f
hu : u ⊆ s
hv : v ⊆ s
huv : Disjoint u v
empty : ∀ {v : Finset ι} (hu : ∅ ⊆ s) (hv : v ⊆ s) (huv : Disjoint ∅ v), Disjoint (sup ∅ f) (v.sup f)
insert :
  ∀ (x : ι) (u : Finset ι) (hx : x ∉ u)
    (ih : ∀ {v : Finset ι} (hu : u ⊆ s) (hv : v ⊆ s) (huv : Disjoint u v), Disjoint (u.sup f) (v.sup f)) {v : Finset ι}
    (hu : Insert.insert x u ⊆ s) (hv : v ⊆ s) (huv : Disjoint (Insert.insert x u) v),
    Disjoint ((Insert.insert x u).sup f) (v.sup f)
⊢ Disjoint (u.sup f) (v.sup f)

Tactic:
classical
  induction u using Finset.induction generalizing v with
  | empty => simp
  | insert x u hx ih =>
    grind [= SupIndep, Disjoint.disjoint_sup_left_of_disjoint_sup_right]

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, Insert.insert, Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
⊢ (s.sigma (α := β) g).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) ∧
      ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)

Tactic:
⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Finset.SupIndep.sigma
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
refine_1 :
  ∀ (h : (s.sigma (α := β) g).SupIndep f),
    ∀ t ⊆ s,
      ∀ i ∈ s,
        i ∉ t →
          Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ ((g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b) : α)) i)
            (t.sup fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))
refine_2 :
  ∀ (h : (s.sigma (α := β) g).SupIndep f),
    ∀ i ∈ s,
      ∀ t ⊆ g i,
        ∀ j ∈ g i,
          j ∉ t →
            Disjoint.{u_1} (α := α) ((fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) j)
              (t.sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))
⊢ (s.sigma (α := β) g).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) ∧
      ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)

Tactic:
refine ⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
this : Disjoint (u.sup f) (v.sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ ((g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b) : α)) i)
    (t.sup fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))

Tactic:
simpa only [sup_map, sup_biUnion, u, v]

Premises used: Finset.sup_map, Finset.sup_biUnion
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
refine_1 : Disjoint (u.sup f) (v.sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ ((g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b) : α)) i)
    (t.sup fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))

Tactic:
suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
refine_1 : u ⊆ s.sigma (α := β) g
refine_1₁ : v ⊆ s.sigma (α := β) g
refine_1₂ : Disjoint u v
⊢ Disjoint (u.sup f) (v.sup f)

Tactic:
apply SupIndep.disjoint_sup_sup h

Premises used: Finset.SupIndep.disjoint_sup_sup
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
⊢ u ⊆ s.sigma (α := β) g

Tactic:
grind [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
⊢ v ⊆ s.sigma (α := β) g

Tactic:
grind [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
t : Finset ι
h_1 : t ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ t
u : Finset ((x : ι) × β x) := map (Function.Embedding.sigmaMk (β := β) i) (g i)
v : Finset ((x : ι) × β x) := t.biUnion fun (j : ι) ↦ map (Function.Embedding.sigmaMk (β := β) j) (g j)
⊢ Disjoint u v

Tactic:
grind [disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
i : ι
h_1 : i ∈ s
t : Finset (β i)
h_2 : t ⊆ g i
j : β i
h_3 : j ∈ g i
h_4 : j ∉ t
this : Disjoint (f (Sigma.mk (β := β) i j)) (sup (image (fun (b : β i) ↦ Sigma.mk (β := β) i b) t) f)
⊢ Disjoint.{u_1} (α := α) ((fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) j)
    (t.sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))

Tactic:
simpa only [sup_image]

Premises used: Finset.sup_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
i : ι
h_1 : i ∈ s
t : Finset (β i)
h_2 : t ⊆ g i
j : β i
h_3 : j ∈ g i
h_4 : j ∉ t
refine_2 : Disjoint (f (Sigma.mk (β := β) i j)) (sup (image (fun (b : β i) ↦ Sigma.mk (β := β) i b) t) f)
⊢ Disjoint.{u_1} (α := α) ((fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) j)
    (t.sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))

Tactic:
suffices Disjoint (f ⟨i, j⟩) ((t.image fun b ↦ ⟨i, b⟩).sup f) by simpa only [sup_image]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma (α := β) g).SupIndep f
i : ι
h_1 : i ∈ s
t : Finset (β i)
h_2 : t ⊆ g i
j : β i
h_3 : j ∈ g i
h_4 : j ∉ t
⊢ Disjoint (f (Sigma.mk (β := β) i j)) (sup (image (fun (b : β i) ↦ Sigma.mk (β := β) i b) t) f)

Tactic:
grind [= SupIndep]

Premises used: Finset.SupIndep
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
refine_1 :
  ∀ (h : (s.sigma (α := β) g).SupIndep f),
    ∀ t ⊆ s,
      ∀ i ∈ s,
        i ∉ t →
          Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ ((g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b) : α)) i)
            (t.sup fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))
refine_2 refine_2₁ :
  ∀ (h : (s.sigma (α := β) g).SupIndep f),
    ∀ i ∈ s,
      ∀ t ⊆ g i,
        ∀ j ∈ g i,
          j ∉ t →
            Disjoint.{u_1} (α := α) ((fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) j)
              (t.sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))
⊢ (s.sigma (α := β) g).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) ∧
      ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)

Tactic:
classical
  refine ⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩
  · let u := (g i).map (Function.Embedding.sigmaMk i)
    let v := t.biUnion (fun j => (g j).map (Function.Embedding.sigmaMk j))
    suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]
    apply SupIndep.disjoint_sup_sup h <;> grind [disjoint_left]
  · suffices Disjoint (f ⟨i, j⟩) ((t.image fun b ↦ ⟨i, b⟩).sup f) by simpa only [sup_image]
    grind [= SupIndep]

Premises used: Finset.SupIndep, Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')) ∧
      SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')

Tactic:
⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩

Premises used: Finset.SupIndep.product, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
refine_1 :
  ∀ (h : (s.product t).SupIndep f),
    ∀ u ⊆ s,
      ∀ i ∈ s,
        i ∉ u →
          Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ (t.sup fun (i' : ι') ↦ f (i, i') : α)) i)
            (u.sup fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i'))
refine_2 :
  ∀ (h : (s.product t).SupIndep f),
    ∀ u ⊆ t,
      ∀ i ∈ t,
        i ∉ u →
          Disjoint.{u_1} (α := α) ((fun (i' : ι') ↦ (s.sup fun (i : ι) ↦ f (i, i') : α)) i)
            (u.sup fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i'))
⊢ (s.product t).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')) ∧
      SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')

Tactic:
refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
h_1 : u ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ u
this : Disjoint (sup (image (fun (x : ι') ↦ (i, x)) t) f) ((u ×ˢ t).sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ (t.sup fun (i' : ι') ↦ f (i, i') : α)) i)
    (u.sup fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i'))

Tactic:
simpa only [sup_image, sup_product_left]

Premises used: Finset.sup_product_left, Finset.sup_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
h_1 : u ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ u
refine_1 : Disjoint (sup (image (fun (x : ι') ↦ (i, x)) t) f) ((u ×ˢ t).sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ (t.sup fun (i' : ι') ↦ f (i, i') : α)) i)
    (u.sup fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i'))

Tactic:
suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
h_1 : u ⊆ s
i : ι
h_2 : i ∈ s
h_3 : i ∉ u
⊢ Disjoint (sup (image (fun (x : ι') ↦ (i, x)) t) f) ((u ×ˢ t).sup f)

Tactic:
grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Premises used: Finset.product_eq_sprod, Finset.SupIndep.disjoint_sup_sup, Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
h_1 : u ⊆ t
i : ι'
h_2 : i ∈ t
h_3 : i ∉ u
this : Disjoint (sup (image (fun (x : ι) ↦ (x, i)) s) f) ((s ×ˢ u).sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i' : ι') ↦ (s.sup fun (i : ι) ↦ f (i, i') : α)) i)
    (u.sup fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i'))

Tactic:
simpa only [sup_image, sup_product_right]

Premises used: Finset.sup_product_right, Finset.sup_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
h_1 : u ⊆ t
i : ι'
h_2 : i ∈ t
h_3 : i ∉ u
refine_2 : Disjoint (sup (image (fun (x : ι) ↦ (x, i)) s) f) ((s ×ˢ u).sup f)
⊢ Disjoint.{u_1} (α := α) ((fun (i' : ι') ↦ (s.sup fun (i : ι) ↦ f (i, i') : α)) i)
    (u.sup fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i'))

Tactic:
suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
h_1 : u ⊆ t
i : ι'
h_2 : i ∈ t
h_3 : i ∉ u
⊢ Disjoint (sup (image (fun (x : ι) ↦ (x, i)) s) f) ((s ×ˢ u).sup f)

Tactic:
grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Premises used: Finset.product_eq_sprod, Finset.SupIndep.disjoint_sup_sup, Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
refine_1 :
  ∀ (h : (s.product t).SupIndep f),
    ∀ u ⊆ s,
      ∀ i ∈ s,
        i ∉ u →
          Disjoint.{u_1} (α := α) ((fun (i : ι) ↦ (t.sup fun (i' : ι') ↦ f (i, i') : α)) i)
            (u.sup fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i'))
refine_2 refine_2₁ :
  ∀ (h : (s.product t).SupIndep f),
    ∀ u ⊆ t,
      ∀ i ∈ t,
        i ∉ u →
          Disjoint.{u_1} (α := α) ((fun (i' : ι') ↦ (s.sup fun (i : ι) ↦ f (i, i') : α)) i)
            (u.sup fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i'))
⊢ (s.product t).SupIndep f ↔
    (SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')) ∧
      SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')

Tactic:
classical
  refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
  · suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]
  · suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Premises used: Finset.product_eq_sprod, Finset.SupIndep.disjoint_sup_sup, Finset.disjoint_left
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ s ∪ t = Finset.biUnion {s, t} id

Tactic:
simp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
rw : SupIndep (Finset.biUnion {s, t} id) f
⊢ (s ∪ t).SupIndep f

Tactic:
rw [show s ∪ t = ({s, t} : Finset _).biUnion id by simp]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ SupIndep (Finset.biUnion {s, t} id) f

Tactic:
grind [SupIndep.biUnion, supIndep_pair]

Premises used: Finset.supIndep_pair, Finset.SupIndep.biUnion
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
i : ι
s : Finset ι
f : ι → α
hs : s.SupIndep f
h : Disjoint (f i) (s.sup f)
⊢ (insert i s).SupIndep f

Tactic:
grind [insert_eq, SupIndep.union, sup_singleton]

Premises used: Finset.insert_eq, Finset.sup_singleton, Finset.SupIndep.union
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
⊢ s.SupIndep f ↔ (↑s : Set ι).PairwiseDisjoint f

Tactic:
⟨SupIndep.pairwiseDisjoint, fun hs _ ht _ hi hit =>
    Finset.disjoint_sup_right.2 fun _ hj => hs hi (ht hj) (ne_of_mem_of_not_mem hj hit).symm⟩

Premises used: Iff.mpr, Ne.symm, ne_of_mem_of_not_mem, Finset.disjoint_sup_right, Iff.intro, Finset.SupIndep.pairwiseDisjoint
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ sSupIndep.{u_1} (α := α) ∅

Tactic:
fun x hx =>
  (Set.notMem_empty x hx).elim

Premises used: sSupIndep, False.elim, Set.notMem_empty
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
t : Set α
hst : t ⊆ s
⊢ sSupIndep t

Tactic:
fun _ ha =>
  (hs (hst ha)).mono_right (sSup_le_sSup (diff_subset_diff_left hst))

Premises used: sSupIndep, Set.diff_subset_diff_left, Disjoint.mono_right, sSup_le_sSup
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
⊢ s.PairwiseDisjoint id

Tactic:
fun _ hx y hy h =>
  disjoint_sSup_right (hs hx) ((mem_diff y).mpr ⟨hy, h.symm⟩)

Premises used: Iff.mpr, Set.PairwiseDisjoint, Ne.symm, Set.Pairwise, disjoint_sSup_right, Set.mem_diff, And.intro
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a i : α
hi : Membership.mem (γ := Set α) {a} i
⊢ Disjoint i (sSup ({a} \ {i}))

Tactic:
simp_all
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
hab : a ≠ b
mp : sSupIndep (α := α) {a, b} → Disjoint a b
mpr : Disjoint a b → sSupIndep (α := α) {a, b}
⊢ sSupIndep (α := α) {a, b} ↔ Disjoint a b

Tactic:
constructor
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
hab : a ≠ b
h : sSupIndep (α := α) {a, b}
⊢ Disjoint a b

Tactic:
h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab

Premises used: Set.mem_singleton, sSupIndep.pairwiseDisjoint, Set.mem_insert_of_mem, Set.mem_insert
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
hab : a ≠ b
h : sSupIndep (α := α) {a, b}
⊢ Disjoint a b

Tactic:
exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab

Premises used: Set.mem_singleton, sSupIndep.pairwiseDisjoint, Set.mem_insert_of_mem, Set.mem_insert
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c b

Tactic:
h
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
h₁ : sSup ({c, b} \ {c}) = b
⊢ Disjoint c (sSup ({c, b} \ {c}))

Tactic:
convert! h using 1
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b

Tactic:
simp [hab, sSup_singleton]

Premises used: sSup_singleton
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c a

Tactic:
h.symm

Premises used: Disjoint.symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
h₁ : sSup ({a, c} \ {c}) = a
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
convert! h.symm using 1

Premises used: Disjoint.symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a

Tactic:
simp [hab, sSup_singleton]

Premises used: sSup_singleton
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
⊢ Disjoint x (sSup (insert x y \ {x}))

Tactic:
have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)

Tactic:
rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this

Premises used: Set.mem_singleton, Set.diff_singleton_eq_self, Set.insert_diff_of_mem
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)

Tactic:
this
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)

Tactic:
exact this