awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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 (f b) (a.sup f)
have apply : Disjoint (f b) ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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 (f b) ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f)
have symm : Disjoint ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f) (f b)
Tactic: symm
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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) ⊔ u.sup f) (f b)
have h : Disjoint (u.sup f) (f b)
Tactic: apply Disjoint.disjoint_sup_left_of_disjoint_sup_right
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ Disjoint ((t.sup fun (i : ι') ↦ (g i).sup f) ⊔ u.sup f) (f b)
have hsup : Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) (u.sup f ⊔ f b)
Tactic: apply Disjoint.disjoint_sup_left_of_disjoint_sup_right
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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) (u.sup f ⊔ f b)
have hsup : Disjoint (t.sup fun (i : ι') ↦ (g i).sup f) ((g i').sup f)
Tactic: rw [← sup_singleton (f := f) (b := b), ← sup_union, show u ∪ {b} = g i' by grind]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
have intro : ∀ ⦃a : Finset ι⦄, a ⊆ s.biUnion g → ∀ ⦃i : ι⦄, i ∈ s.biUnion g → i ∉ a → Disjoint (f i) (a.sup 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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.biUnion g).SupIndep f
have 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)
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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.biUnion g).SupIndep f
have 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)
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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.biUnion g).SupIndep f
have 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)
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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.biUnion g).SupIndep f
have 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)
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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.biUnion g).SupIndep f
have 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)
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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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.sup g).SupIndep f
have rw : (s.biUnion g).SupIndep f
Tactic: rw [sup_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.sigma (α := β) g).SupIndep f
have rw : SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
Tactic: rw [Finset.sigma_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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 (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
have hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (map (Function.Embedding.sigmaMk (β := β) i) (g i)).sup f
Tactic: apply Finset.SupIndep.biUnion
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
have hg₁ : ∀ i' ∈ s, (map (Function.Embedding.sigmaMk (β := β) i') (g i')).SupIndep f
Tactic: apply Finset.SupIndep.biUnion
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ (s.sigma (α := β) g).SupIndep f
have rw : SupIndep (s.biUnion fun (i : ι) ↦ map (Function.Embedding.sigmaMk (β := β) i) (g i)) f
Tactic: classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using hs
  · simpa [Finset.supIndep_map] using hg
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ (s.sigma (α := β) g).SupIndep f
have hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ (map (Function.Embedding.sigmaMk (β := β) i) (g i)).sup f
Tactic: classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using hs
  · simpa [Finset.supIndep_map] using hg
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ (s.sigma (α := β) g).SupIndep f
have hg₁ : ∀ i' ∈ s, (map (Function.Embedding.sigmaMk (β := β) i') (g i')).SupIndep f
Tactic: classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using hs
  · simpa [Finset.supIndep_map] using hg
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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')
⊢ (s ×ˢ t).SupIndep f
have rw : SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f
Tactic: rw [Finset.product_eq_biUnion]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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 (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f
have hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ sup (image (fun (b : ι') ↦ (i, b)) t) f
Tactic: apply Finset.SupIndep.biUnion
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) f
have hg : ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) f
Tactic: apply Finset.SupIndep.biUnion
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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')
⊢ (s ×ˢ t).SupIndep f
have rw : SupIndep (s.biUnion fun (a : ι) ↦ image (fun (b : ι') ↦ (a, b)) t) 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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ (s ×ˢ t).SupIndep f
have hs₁ : SupIndep.{u_1, u_3} (α := α) s fun (i : ι) ↦ sup (image (fun (b : ι') ↦ (i, b)) t) 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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ (s ×ˢ t).SupIndep f
have hg : ∀ i' ∈ s, SupIndep (image (fun (b : ι') ↦ (i', b)) t) 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
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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
⊢ Disjoint (u.sup f) (v.sup f)
have empty : ∀ {v : Finset ι} (hu : ∅ ⊆ s) (hv : v ⊆ s) (huv : Disjoint ∅ v), Disjoint (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]
Cleared hypotheses: u, v, hu, hv, huv
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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)
⊢ Disjoint (u.sup f) (v.sup f)
have 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 x u ⊆ s) (hv : v ⊆ s) (huv : Disjoint (insert x u) v), Disjoint ((insert x 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]
Cleared hypotheses: u, v, hu, hv, huv