awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
refine_1 :
  ∀ (hs : (map g s).SupIndep f) (t : Finset ι') (ht : t ⊆ s) (i : ι') (hi : i ∈ s) (hit : i ∉ t),
    Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) (t.sup (f ∘ (⇑g : (a : ι') → ι)))
refine_2 : ∀ (hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))), (map g s).SupIndep f
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ (⇑g : (a : ι') → ι))

Tactic:
refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
refine_1 : Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) ((map g t).sup f)
⊢ Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) (t.sup (f ∘ (⇑g : (a : ι') → ι)))

Tactic:
rw [← sup_map]

Premises used: Finset.sup_map
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit rwa rwa₁ rwa₂ rwa₃ : i ∉ t
⊢ ((g : (a : ι') → ι) i : ι) ∉ map g t

Tactic:
rwa [mem_map']

Premises used: Finset.mem_map'
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ (⇑g : (a : ι') → ι)) i) ((map g t).sup f)

Tactic:
exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])

Premises used: Iff.mpr, Finset.mem_map', Finset.map_subset_map
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
refine_2 : SupIndep (image (⇑g : (a : ι') → ι) s) f
⊢ (map g s).SupIndep f

Tactic:
rw [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
⊢ SupIndep (image (⇑g : (a : ι') → ι) s) f

Tactic:
hs.image

Premises used: Finset.SupIndep.image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
⊢ SupIndep (image (⇑g : (a : ι') → ι) s) f

Tactic:
exact hs.image

Premises used: Finset.SupIndep.image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ (⇑g : (a : ι') → ι))
refine_2 refine_2₁ refine_2₂ : SupIndep (image (⇑g : (a : ι') → ι) s) f
⊢ (map g s).SupIndep f

Tactic:
classical
    rw [map_eq_image]
    exact hs.image

Premises used: Finset.map_eq_image
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
this : Disjoint (f i) (f j) → Disjoint (f j) ((erase {i, j} j).sup f)
⊢ SupIndep {i, j} f ↔ Disjoint (f i) (f j)

Tactic:
simpa [supIndep_iff_disjoint_erase, hij]

Premises used: Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
suffices : Disjoint (f i) (f j) → Disjoint (f j) ((erase {i, j} j).sup f)
⊢ SupIndep {i, j} f ↔ Disjoint (f i) (f j)

Tactic:
suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase {i, j} j).sup f) by
    simpa [supIndep_iff_disjoint_erase, hij]
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
rw : Disjoint (f i) (f j) → Disjoint (f j) ((erase {j, i} j).sup f)
⊢ Disjoint (f i) (f j) → Disjoint (f j) ((erase {i, j} j).sup f)

Tactic:
rw [pair_comm]

Premises used: Finset.pair_comm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
f : ι → α
inst_2 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) ((erase {j, i} j).sup f)

Tactic:
simp [hij.symm, disjoint_comm]

Premises used: disjoint_comm, Ne.symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
f : Bool → α
⊢ true ≠ false

Tactic:
simp only [Ne, not_false_iff, reduceCtorEq]

Premises used: reduceCtorEq, Ne, not_false_iff
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
f : Fin 2 → α
⊢ Ne (α := Fin 2) 0 1

Tactic:
simp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
⊢ (SupIndep.{u_1, u_3} (α := α) s.attach fun (a : ↥s) ↦ f (↑a : ι)) ↔ s.SupIndep f

Tactic:
simpa [Finset.attach_map_val] using (supIndep_map (s := s.attach) (g := .subtype _)).symm

Premises used: Finset.supIndep_map, Finset.attach_map_val, Iff.symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb : b ∈ s.biUnion g
hab : b ∉ a
obtain : ∀ (i' : ι') (hi' : i' ∈ s) (hb : b ∈ g i'), Disjoint (f b) (a.sup f)
⊢ Disjoint (f b) (a.sup f)

Tactic:
obtain ⟨i', hi', hb⟩ := mem_biUnion.mp hb

Premises used: Iff.mp, Finset.mem_biUnion
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ a.sup f ≤ (t.biUnion g ∪ u).sup f

Tactic:
grind
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ (t.biUnion g ∪ u).sup f ≤ (t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f

Tactic:
grind
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
apply : Disjoint (f b) ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f)
⊢ Disjoint (f b) (a.sup f)

Tactic:
apply Disjoint.mono_right <| calc
    a.sup f ≤ (t.biUnion g ∪ u).sup f := by grind
    _ ≤ (t.sup fun i => (g i).sup f) ⊔ (u.sup f) := by grind

Premises used: Finset.biUnion, Finset.sup, Union.union, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
symm : Disjoint ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f) (f b)
⊢ Disjoint (f b) ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f)

Tactic:
symm
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
h : Disjoint (u.sup f) (f b)
hsup : Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) (u.sup f ⊔ f b)
⊢ Disjoint ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f) (f b)

Tactic:
apply Disjoint.disjoint_sup_left_of_disjoint_sup_right

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (u.sup f) (f b)

Tactic:
(supIndep_iff_disjoint_erase.mp (hg i' hi') b hb).symm

Premises used: Disjoint.symm, Finset.supIndep_iff_disjoint_erase, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (u.sup f) (f b)

Tactic:
exact (supIndep_iff_disjoint_erase.mp (hg i' hi') b hb).symm

Premises used: Disjoint.symm, Finset.supIndep_iff_disjoint_erase, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ u ∪ {b} = g i'

Tactic:
grind
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
hsup : Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) ((g i').sup f)
⊢ Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) (u.sup f ⊔ f b)

Tactic:
rw [← sup_singleton (f := f) (b := b), ← sup_union, show u ∪ {b} = g i' by grind]

Premises used: Finset.sup_singleton, Finset.sup_union
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) ((g i').sup f)

Tactic:
(supIndep_iff_disjoint_erase.mp hs i' hi').symm

Premises used: Disjoint.symm, Finset.supIndep_iff_disjoint_erase, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb_1 : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := s.erase i'
u : Finset ι := (g i').erase b
⊢ Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) ((g i').sup f)

Tactic:
exact (supIndep_iff_disjoint_erase.mp hs i' hi').symm

Premises used: Disjoint.symm, Finset.supIndep_iff_disjoint_erase, Iff.mp
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
intro intro₁ intro₂ intro₃ intro₄ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a), Disjoint (f b) (a.sup f)
intro₅ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'), Disjoint (f b) (a.sup f)
intro₆ intro₇ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'), Disjoint (f b) (a.sup f)
intro₈ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'),
    let t := s.erase i';
    let u := (g i').erase b;
    Disjoint (f b) ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f)
intro₉ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'),
    let t := s.erase i';
    let u := (g i').erase b;
    Disjoint ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f) (f b)
h :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'),
    let u := (g i').erase b;
    Disjoint (u.sup f) (f b)
hsup hsup₁ :
  ∀ ⦃a : Finset ι⦄ (ha : a ⊆ s.biUnion g) ⦃b : ι⦄ (hb : b ∈ s.biUnion g) (hab : b ∉ a) (i' : ι') (hi' : i' ∈ s)
    (hb : b ∈ g i'),
    let t := s.erase i';
    let u := (g i').erase b;
    Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) (u.sup f ⊔ f b)
⊢ (s.biUnion g).SupIndep f

Tactic:
classical
  intro a ha b hb hab
  obtain ⟨i', hi', hb⟩ := mem_biUnion.mp hb
  let t := s.erase i'
  let u := (g i').erase b
  apply Disjoint.mono_right <| calc
    a.sup f ≤ (t.biUnion g ∪ u).sup f := by grind
    _ ≤ (t.sup fun i => (g i).sup f) ⊔ (u.sup f) := by grind
  symm
  apply Disjoint.disjoint_sup_left_of_disjoint_sup_right
  · exact (supIndep_iff_disjoint_erase.mp (hg i' hi') b hb).symm
  · rw [← sup_singleton (f := f) (b := b), ← sup_union, show u ∪ {b} = g i' by grind]
    exact (supIndep_iff_disjoint_erase.mp hs i' hi').symm

Premises used: Disjoint.disjoint_sup_left_of_disjoint_sup_right, Finset.sup_union, Disjoint.mono_right
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
rw : (s.biUnion g).SupIndep f
⊢ (s.sup g).SupIndep f

Tactic:
rw [sup_eq_biUnion]

Premises used: Finset.sup_eq_biUnion
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.biUnion g).SupIndep f

Tactic:
hs.biUnion hg

Premises used: Finset.SupIndep.biUnion
-- Module: Mathlib.Order.SupIndep
Goal:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : OrderBot α
inst_3 : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : SupIndep.{u_1, u_4} (α := α) s fun (i : ι') ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.biUnion g).SupIndep f

Tactic:
exact hs.biUnion hg

Premises used: Finset.SupIndep.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 β → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hg : ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
rw : SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
⊢ (s.sigma (α := β) g).SupIndep f

Tactic:
rw [Finset.sigma_eq_biUnion]

Premises used: Finset.sigma_eq_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 β → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hg : ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (map (Function.Embedding.sigmaMk (β := β) i) (g i)).sup f
hg₁ : ∀ i' ∈ s, (map (Function.Embedding.sigmaMk (β := β) i') (g i')).SupIndep f
⊢ SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f

Tactic:
apply Finset.SupIndep.biUnion

Premises used: Finset.SupIndep.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 β → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hg : ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
⊢ SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (map (Function.Embedding.sigmaMk (β := β) i) (g i)).sup f

Tactic:
simpa using hs
-- 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 β → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hg : ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
⊢ ∀ i' ∈ s, (map (Function.Embedding.sigmaMk (β := β) i') (g i')).SupIndep f

Tactic:
simpa [Finset.supIndep_map] using hg

Premises used: Finset.supIndep_map
-- 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 β → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (g i).sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
hg : ∀ i ∈ s, SupIndep.{u_1, u_5} (α := α) (g i) fun (b : β i) ↦ f (Sigma.mk (β := β) i b)
rw rw₁ rw₂ : SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (map (Function.Embedding.sigmaMk (β := β) i) (g i)).sup f
hg₁ hg₂ : ∀ i' ∈ s, (map (Function.Embedding.sigmaMk (β := β) i') (g i')).SupIndep f
⊢ (s.sigma (α := β) g).SupIndep f

Tactic:
classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using hs
  · simpa [Finset.supIndep_map] using hg

Premises used: Finset.supIndep_map, Finset.SupIndep.biUnion, Finset.sigma_eq_biUnion
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
rw : SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f
⊢ (s ×ˢ t).SupIndep f

Tactic:
rw [Finset.product_eq_biUnion]

Premises used: Finset.product_eq_biUnion
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ sup (image (fun (b : ι') ↦ (i, b)) t) f
hg : ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) f
⊢ SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f

Tactic:
apply Finset.SupIndep.biUnion

Premises used: Finset.SupIndep.biUnion
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
⊢ SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ sup (image (fun (b : ι') ↦ (i, b)) t) f

Tactic:
simpa using hs
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
⊢ ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) f

Tactic:
fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Premises used: Finset.SupIndep.mono, Finset.SupIndep.image, Finset.le_sup
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
⊢ ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) f

Tactic:
exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Premises used: Finset.SupIndep.mono, Finset.SupIndep.image, Finset.le_sup
-- 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 : ι × ι' → α
hs : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ t.sup fun (i' : ι') ↦ f (i, i')
ht : SupIndep.{u_1, u_4} (α := α) t fun (i' : ι') ↦ s.sup fun (i : ι) ↦ f (i, i')
rw rw₁ rw₂ : SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f
hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ sup (image (fun (b : ι') ↦ (i, b)) t) f
hg hg₁ : ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) f
⊢ (s ×ˢ t).SupIndep f

Tactic:
classical
  rw [Finset.product_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using hs
  · exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Premises used: Finset.product_eq_biUnion, Finset.SupIndep.biUnion
-- 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
v : Finset ι
hu : ∅ ⊆ s
hv : v ⊆ s
huv : Disjoint ∅ v
⊢ Disjoint (sup ∅ f) (v.sup f)

Tactic:
simp