awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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]
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: 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]
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 α
β : ι → 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)
have 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))
Tactic: refine ⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩
-- 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 β → α
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))
⊢ (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)
have 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))
Tactic: refine ⟨fun h ↦ ⟨fun t _ i _ _ ↦ ?_, fun i _ t _ j _ _ ↦ ?_⟩, fun h ↦ h.1.sigma h.2⟩
-- 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 β → α
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_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))
have refine_1 : Disjoint (u.sup f) (v.sup f)
Tactic: suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]
-- 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 β → α
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.sup f) (v.sup f)
have refine_1 : u ⊆ s.sigma (α := β) g
Tactic: apply SupIndep.disjoint_sup_sup h
-- 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 β → α
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
⊢ Disjoint (u.sup f) (v.sup f)
have refine_1₁ : v ⊆ s.sigma (α := β) g
Tactic: apply SupIndep.disjoint_sup_sup h
-- 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 β → α
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
⊢ Disjoint (u.sup f) (v.sup f)
have refine_1₂ : Disjoint u v
Tactic: apply SupIndep.disjoint_sup_sup h
-- 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 β → α
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.{u_1} (α := α) ((fun (b : β i) ↦ f (Sigma.mk (β := β) i b)) j)
    (t.sup fun (b : β i) ↦ f (Sigma.mk (β := β) i b))
have refine_2 : Disjoint (f (Sigma.mk (β := β) i j)) (sup (image (fun (b : β i) ↦ Sigma.mk (β := β) i b) t) f)
Tactic: suffices Disjoint (f ⟨i, j⟩) ((t.image fun b ↦ ⟨i, b⟩).sup f) by simpa only [sup_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 α
β : ι → 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)
have 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))
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]
-- 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 β → α
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))
⊢ (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)
have 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))
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]
-- 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 : ι × ι' → α
⊢ (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')
have 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'))
Tactic: refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
-- 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 : ι × ι' → α
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'))
⊢ (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')
have 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'))
Tactic: refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
-- 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 : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
h_1 : u ⊆ s
i : ι
h_2 : i ∈ s
h_3 : 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'))
have refine_1 : Disjoint (sup (image (fun (x : ι') ↦ (i, x)) t) f) ((u ×ˢ t).sup f)
Tactic: suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
-- 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 : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
h_1 : u ⊆ t
i : ι'
h_2 : i ∈ t
h_3 : 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'))
have refine_2 : Disjoint (sup (image (fun (x : ι) ↦ (x, i)) s) f) ((s ×ˢ u).sup f)
Tactic: suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_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 α
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')
have 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'))
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]
-- 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 : ι × ι' → α
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'))
⊢ (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')
have 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'))
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]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
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).SupIndep f
have rw : SupIndep (Finset.biUnion {s, t} id) f
Tactic: rw [show s ∪ t = ({s, t} : Finset _).biUnion id by simp]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep (α := α) {a, b} ↔ Disjoint a b
have mp : sSupIndep (α := α) {a, b} → Disjoint a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
hab : a ≠ b
mp : sSupIndep (α := α) {a, b} → Disjoint a b
⊢ sSupIndep (α := α) {a, b} ↔ Disjoint a b
have mpr : Disjoint a b → sSupIndep (α := α) {a, b}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))
have h₁ : sSup ({c, b} \ {c}) = b
Tactic: convert! h using 1
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
have h₁ : sSup ({a, c} \ {c}) = a
Tactic: convert! h.symm using 1
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
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 y)
have this : Disjoint x (sSup (insert x y \ {x}))
Tactic: have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
⊢ sSupIndep s ↔ iSupIndep.{u_5 + 1, u_5} (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
have simp_rw : (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
  ∀ (x : α) (h : x ∈ s),
    Disjoint x (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h), (↑j : α))
Tactic: simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s),
      Disjoint x (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h), (↑j : α))
have refine : ∀ (a : α) (ha : a ∈ s),
  Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔
    Disjoint a (⨆ (j : { x : α // x ∈ s }), ⨆ (_ : j ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha), (↑j : α))
Tactic: refine forall₂_congr fun a ha => ?_
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))
have simp_rw : iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (a : ι), ⨆ (_ : Membership.mem (γ := Set ι) {j : ι | j ≠ i} a), t a)
Tactic: simp_rw [sSup_image]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})
have rw : (∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))) ↔
  ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})
Tactic: rw [iSupIndep_def']
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i : ι'
⊢ LE.le.{u_1} (α := α) (⨆ (j : ι'), ⨆ (_ : j ≠ i), (t ∘ f) j) (⨆ (j : ι), ⨆ (_ : j ≠ f i), t j)
have refine : ∀ (i_1 : ι'), LE.le.{u_1} (α := α) (⨆ (_ : i_1 ≠ i), (t ∘ f) i_1) (⨆ (_ : f i_1 ≠ f i), t (f i_1))
Tactic: refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
have obtain : ∀ (i' : ι'), Disjoint (t (f i')) (⨆ (j : ι), ⨆ (_ : j ≠ f i'), t j)
Tactic: obtain ⟨i', rfl⟩ := hf i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ (j : ι), ⨆ (_ : j ≠ f i'), t j)
have rw : Disjoint (t (f i')) (⨆ (x : ι'), ⨆ (_ : f x ≠ f i'), t (f x))
Tactic: rw [← hf.iSup_comp]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ sSupIndep (range t)
have rw : iSupIndep.{u_1 + 1, u_1} (ι := { x : α // x ∈ range t }) (Subtype.val (p := fun (x : α) ↦ x ∈ range t))
Tactic: rw [sSupIndep_iff]
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep.{u_1 + 1, u_1} (ι := { x : α // x ∈ range t }) (Subtype.val (p := fun (x : α) ↦ x ∈ range t))
have ht₁ : iSupIndep (Subtype.val (p := fun (x : α) ↦ x ∈ range t) ∘ rangeFactorization t)
Tactic: rw [← coe_comp_rangeFactorization t] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
⊢ (iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)) ↔ iSupIndep t
have refine : ∀ (h : iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)), iSupIndep t
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : iSupIndep.{u_3 + 1, u_1} (α := α) fun (i : { i : ι // t i ≠ ⊥ }) ↦ t (↑i : ι)
⊢ iSupIndep t
have h₁ : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
Tactic: simp only [iSupIndep_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
have hi : t i ≠ ⊥
Tactic: cases eq_or_ne (t i) ⊥ with
  | inl hi => simp [hi]
  | inr hi => ?_
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
⊢ Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
have h₁ : Eq.{u_1 + 1} (α := α) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
  (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))
Tactic: convert! h ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Order.SupIndep (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
    (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))
have this : ∀ (j : ι), Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥
Tactic: have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
h : ∀ (i : { i : ι // t i ≠ ⊥ }), Disjoint (t (↑i : ι)) (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ i), t (↑j : ι))
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), Eq.{u_1 + 1} (α := α) (⨆ (_ : t j = ⊥), t j) ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
    (⨆ (j : { i : ι // t i ≠ ⊥ }), ⨆ (_ : j ≠ Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi), t (↑j : ι))
have h₁ : Eq.{u_1 + 1} (α := α)
  ((⨆ (i_1 : ι), ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ (i_1 : ι), ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1)
  (⨆ (i_1 : ι),
    ⨆ (h : t i_1 ≠ ⊥),
      ⨆ (_ :
        Ne (α := { i : ι // t i ≠ ⊥ }) (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h)
          (Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i hi)),
        t (↑(Subtype.mk (p := fun (i : ι) ↦ t i ≠ ⊥) i_1 h) : ι))
Tactic: rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
⊢ i = j
have by_contra! : ∀ (contra : i ≠ j), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Order.SupIndep (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
h_1 : Membership.mem (γ := Set ι) {i : ι | t i ≠ ⊥} i
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ False
have apply : t j = ⊥
Tactic: apply hj