awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b_1 c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ P.parts, b ≤ c
have obtain : ∀ (c : α × α) (hc : c ∈ P.parts ×ˢ Q.parts) (hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts), ∃ c_1 ∈ P.parts, c.1 ⊓ c.2 ≤ c_1
Tactic: obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ P.parts, c.1 ⊓ c.2 ≤ c_2
have hc₁ : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
Tactic: rw [mem_product] at hc
Cleared hypotheses: hc, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b_1 c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ Q.parts, b ≤ c
have obtain : ∀ (c : α × α) (hc : c ∈ P.parts ×ˢ Q.parts) (hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts), ∃ c_1 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_1
Tactic: obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_2
have hc₁ : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
Tactic: rw [mem_product] at hc
Cleared hypotheses: hc, hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b_1 c : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c
have obtain : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), ∃ c ∈ (Q ⊓ R).parts, b ≤ c
Tactic: obtain ⟨c, hc, hbc⟩ := hPQ hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b_1 c_1 : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c
have obtain : ∀ (d : α) (hd : d ∈ R.parts) (hbd : b ≤ d), ∃ c ∈ (Q ⊓ R).parts, b ≤ c
Tactic: obtain ⟨d, hd, hbd⟩ := hPR hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b_1 c_1 : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hbd : b ≤ d
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c
have h : b ≤ c ⊓ d
Tactic: have h := _root_.le_inf hbc hbd
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
x : α
hx : x ∈ (↑(erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) : Set α)
y : α
hy : y ∈ (↑(erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) : Set α)
hxy : x ≠ y
⊢ (Disjoint on id) x y
have hx₁ : (∃ x_1 ∈ (↑P.parts : Set α), x_1 ⊓ b = x) ∧ ¬x = ⊥
Tactic: simp only [coe_erase, coe_image, Set.mem_diff, Set.mem_image, Set.mem_singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
x : α
hx : x ∈ (↑(erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) : Set α)
y : α
hy : y ∈ (↑(erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) : Set α)
hxy : x ≠ y
hx₁ : (∃ x_1 ∈ (↑P.parts : Set α), x_1 ⊓ b = x) ∧ ¬x = ⊥
⊢ (Disjoint on id) x y
have hy₁ : (∃ x ∈ (↑P.parts : Set α), x ⊓ b = y) ∧ ¬y = ⊥
Tactic: simp only [coe_erase, coe_image, Set.mem_diff, Set.mem_image, Set.mem_singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
x y : α
hxy : x ≠ y
hx : (∃ x_1 ∈ (↑P.parts : Set α), x_1 ⊓ b = x) ∧ ¬x = ⊥
hy : (∃ x ∈ (↑P.parts : Set α), x ⊓ b = y) ∧ ¬y = ⊥
⊢ (Disjoint on id) x y
have obtain : ∀ (px : α) (hpx : px ∈ (↑P.parts : Set α)) (hxy : px ⊓ b ≠ y), ¬px ⊓ b = ⊥ → (Disjoint on id) (px ⊓ b) y
Tactic: obtain ⟨⟨px, hpx, rfl⟩, _⟩ := hx
Cleared hypotheses: x, hxy, hx
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
y : α
hy : (∃ x ∈ (↑P.parts : Set α), x ⊓ b = y) ∧ ¬y = ⊥
px : α
hpx : px ∈ (↑P.parts : Set α)
hxy : px ⊓ b ≠ y
right : ¬px ⊓ b = ⊥
⊢ (Disjoint on id) (px ⊓ b) y
have obtain : ∀ (py : α) (hpy : py ∈ (↑P.parts : Set α)) (hxy : px ⊓ b ≠ py ⊓ b), ¬py ⊓ b = ⊥ → (Disjoint on id) (px ⊓ b) (py ⊓ b)
Tactic: obtain ⟨⟨py, hpy, rfl⟩, _⟩ := hy
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ sup (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) id = b
have simp : (P.parts.sup fun (i : α) ↦ i) ⊓ b = b
Tactic: simp only [sup_erase_bot, sup_image, Function.id_comp, (sup_inf_distrib_right ..).symm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ (P.parts.sup fun (i : α) ↦ i) ⊓ b = b
have this : (P.parts.sup fun (x : α) ↦ x) = a
Tactic: have : P.parts.sup (fun x => x) = a := P.sup_parts
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
this : (P.parts.sup fun (x : α) ↦ x) = a
⊢ (P.parts.sup fun (i : α) ↦ i) ⊓ b = b
have rw : a ⊓ b = b
Tactic: rw [this, inf_eq_right.mpr hb]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
this : (P.parts.sup fun (x : α) ↦ x) = a
rw : a ⊓ b = b
⊢ (P.parts.sup fun (i : α) ↦ i) ⊓ b = b
have rw₁ : b = b
Tactic: rw [this, inf_eq_right.mpr hb]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x : α
hx : x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
y : α
hy : y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
hxy : x ⊓ b = y ⊓ b
⊢ x = y
have by_contra : ∀ (hne : ¬x = y), False
Tactic: by_contra hne
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x : α
hx : x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
y : α
hy : y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
hxy : x ⊓ b = y ⊓ b
hne : ¬x = y
⊢ False
have hx₁ : x ∈ P.parts ∧ x ⊓ b ≠ ⊥
Tactic: simp only [Finset.mem_filter] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x : α
hx : x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
y : α
hy : y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
hxy : x ⊓ b = y ⊓ b
hne : ¬x = y
hx₁ : x ∈ P.parts ∧ x ⊓ b ≠ ⊥
⊢ False
have hy₁ : y ∈ P.parts ∧ y ⊓ b ≠ ⊥
Tactic: simp only [Finset.mem_filter] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x y : α
hxy : x ⊓ b = y ⊓ b
hne : ¬x = y
hx : x ∈ P.parts ∧ x ⊓ b ≠ ⊥
hy : y ∈ P.parts ∧ y ⊓ b ≠ ⊥
⊢ False
have this : Disjoint (x ⊓ b) (y ⊓ b)
Tactic: have : Disjoint (x ⊓ b) (y ⊓ b) := (P.disjoint hx.1 hy.1 hne).mono inf_le_left inf_le_left
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
⊢ Eq.{u_2 + 1} (α := M) (∑ p ∈ (P.restrict hb).parts, f p) (∑ q ∈ P.parts, f (q ⊓ b))
have hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
Tactic: have hinj : ∀ x ∈ P.parts.filter (· ⊓ b ≠ ⊥), ∀ y ∈ P.parts.filter (· ⊓ b ≠ ⊥),
      x ⊓ b = y ⊓ b → x = y := fun x hx y hy hxy => by
    by_contra hne
    simp only [Finset.mem_filter] at hx hy
    have : Disjoint (x ⊓ b) (y ⊓ b) := (P.disjoint hx.1 hy.1 hne).mono inf_le_left inf_le_left
    grind
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
⊢ Eq.{u_2 + 1} (α := M) (∑ p ∈ (P.restrict hb).parts, f p) (∑ q ∈ P.parts, f (q ⊓ b))
have heq : Eq (α := Finset α) (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥)
  (image (fun (x : α) ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥}))
Tactic: have heq : (P.parts.image (· ⊓ b)).erase ⊥ = (P.parts.filter (· ⊓ b ≠ ⊥)).image (· ⊓ b) := by
    grind
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq :
  Eq (α := Finset α) (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥)
    (image (fun (x : α) ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥}))
x : α
hx : x ∈ {x ∈ P.parts | ¬x ⊓ b ≠ ⊥}
⊢ f (x ⊓ b) = 0
have hx₁ : x ∈ P.parts ∧ x ⊓ b = ⊥
Tactic: simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq :
  Eq (α := Finset α) (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥)
    (image (fun (x : α) ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥}))
x : α
hx : x ∈ P.parts ∧ x ⊓ b = ⊥
rw : f ⊥ = 0
⊢ f (x ⊓ b) = 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [hx.2, hf]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst_3 : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
heq :
  Eq (α := Finset α) (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥)
    (image (fun (x : α) ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥}))
⊢ Eq.{u_2 + 1} (α := M) (∑ p ∈ (P.restrict hb).parts, f p) (∑ q ∈ P.parts, f (q ⊓ b))
have hz : Eq.{u_2 + 1} (α := M) (∑ x ∈ P.parts with ¬x ⊓ b ≠ ⊥, f (x ⊓ b)) 0
Tactic: have hz : ∑ x ∈ P.parts.filter (¬ · ⊓ b ≠ ⊥), f (x ⊓ b) = 0 := Finset.sum_eq_zero fun x hx => by
    simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx
    rw [hx.2, hf]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
parts : Finset α
hdisjoint : (↑parts : Set α).PairwiseDisjoint id
X : Type u_2
inst_3 : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)
have pos : ∀ (hbot : ⊥ ∈ parts), Eq.{u_2 + 1} (α := X) (∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)
Tactic: by_cases hbot : ⊥ ∈ parts
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
parts : Finset α
hdisjoint : (↑parts : Set α).PairwiseDisjoint id
X : Type u_2
inst_3 : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
pos :
  ∀ (hbot : ⊥ ∈ parts), Eq.{u_2 + 1} (α := X) (∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)
have neg : ∀ (hbot : ⊥ ∉ parts), Eq.{u_2 + 1} (α := X) (∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)
Tactic: by_cases hbot : ⊥ ∈ parts
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
parts : Finset α
hdisjoint : (↑parts : Set α).PairwiseDisjoint id
X : Type u_2
inst_3 : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ parts.erase ⊥, f p) (∑ p ∈ parts, f p)
have pos : Eq.{u_2 + 1} (α := X) (∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p) (∑ a ∈ parts.erase ⊥, f a)
Tactic: rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
parts : Finset α
hdisjoint : (↑parts : Set α).PairwiseDisjoint id
X : Type u_2
inst_3 : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
pos : Eq.{u_2 + 1} (α := X) (∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p) (∑ a ∈ parts.erase ⊥, f a)
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ parts.erase ⊥, f p) (∑ p ∈ parts, f p)
have pos₁ : ∀ (a : α), Membership.mem (γ := Finset α) {⊥} a → a ∉ parts.erase ⊥ → f a = 0
Tactic: rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a_1 b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ sup (I.biUnion fun (i : ι) ↦ (P i).parts) id = I.sup a
have rw : (I.sup fun (x : ι) ↦ (P x).parts.sup id) = I.sup a
Tactic: rw [sup_biUnion]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a_1 b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ⊥ ∉ I.biUnion fun (i : ι) ↦ (P i).parts
have rw : ¬∃ a_2 ∈ I, ⊥ ∈ (P a_2).parts
Tactic: rw [mem_biUnion]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a_1 b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ¬∃ a_2 ∈ I, ⊥ ∈ (P a_2).parts
have push : ∀ (a_2 : ι) (_ : a_2 ∈ I), ⊥ ∉ (P a_2).parts
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst_4 : AddCommMonoid M
f : α → M
⊢ Eq.{u_3 + 1} (α := M) (∑ p ∈ I.biUnion fun (i : ι) ↦ (P i).parts, f p) (∑ i ∈ I, ∑ p ∈ (P i).parts, f p)
have refine : ∀ (i : ι) (hi : i ∈ (↑I : Set ι)) (j : ι) (hj : j ∈ (↑I : Set ι)) (hij : i ≠ j),
  onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset α) Disjoint (fun (i : ι) ↦ (P i).parts) i j
Tactic: refine Finset.sum_biUnion fun i hi j hj hij => ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst_4 : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ (↑I : Set ι)
j : ι
hj : j ∈ (↑I : Set ι)
hij : i ≠ j
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset α) Disjoint (fun (i : ι) ↦ (P i).parts) i j
have rw : ∀ ⦃a : α⦄, a ∈ (P i).parts → a ∉ (P j).parts
Tactic: rw [Function.onFun, Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst_4 : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ (↑I : Set ι)
j : ι
hj : j ∈ (↑I : Set ι)
hij : i ≠ j
p : α
hpi : p ∈ (P i).parts
hpj : p ∈ (P j).parts
⊢ False
have hp_disj : Disjoint p p
Tactic: have hp_disj : Disjoint p p := (ha.pairwiseDisjoint hi hj hij).mono ((P i).le hpi) ((P j).le hpj)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P_1 : Finpartition a
Q_1 : (i : α) → i ∈ P_1.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ P.parts.attach.sup (Subtype.val (p := fun (x : α) ↦ x ∈ P.parts)) = a
have rw : (P.parts.sup fun (x : α) ↦ x) = a
Tactic: rw [Finset.sup_attach (f := fun x => x), ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P_1 : Finpartition a
Q_1 : (i : α) → i ∈ P_1.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
rw : (P.parts.sup fun (x : α) ↦ x) = a
⊢ P.parts.attach.sup (Subtype.val (p := fun (x : α) ↦ x ∈ P.parts)) = a
have rw₁ : P.parts.sup id = a
Tactic: rw [Finset.sup_attach (f := fun x => x), ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P_1 : Finpartition a
Q_1 : (i : α) → i ∈ P_1.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
rw : (P.parts.sup fun (x : α) ↦ x) = a
rw₁ : P.parts.sup id = a
⊢ P.parts.attach.sup (Subtype.val (p := fun (x : α) ↦ x ∈ P.parts)) = a
have rw₂ : a = a
Tactic: rw [Finset.sup_attach (f := fun x => x), ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ b ∈ (P.bind Q).parts ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
have rw : (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) sorry).parts) ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
Tactic: rw [bind_parts, mem_biUnion]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts) ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
have mp : (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) sorry).parts) → ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
mp : (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts) → ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts) ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
have mpr : (∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q (↑a_2 : α) sorry).parts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q (↑A : α) ⋯).parts
have h : (↑P.parts.attach : Set ↥P.parts).PairwiseDisjoint (α := Finset α) fun (i : ↥P.parts) ↦
  parts (a := (↑i : α)) ((fun (i : ↥P.parts) ↦ Q (↑i : α) sorry) i)
Tactic: apply card_biUnion
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc
⊢ onFun (β := Finset α) Disjoint (fun (i : ↥P.parts) ↦ parts (a := (↑i : α)) ((fun (i : ↥P.parts) ↦ Q (↑i : α) ⋯) i))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc)
have h : ∀ ⦃a_1 : α⦄,
  Membership.mem (γ := Finset α)
      (parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb) : α))
        ((fun (i : ↥P.parts) ↦ Q (↑i : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb)))
      a_1 →
    a_1 ∉
      parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc) : α))
        ((fun (i : ↥P.parts) ↦ Q (↑i : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc))
Tactic: rw [Function.onFun, Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc
d : α
hdb :
  Membership.mem (γ := Finset α)
    (parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb) : α))
      ((fun (i : ↥P.parts) ↦ Q (↑i : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb)))
    d
hdc :
  Membership.mem (γ := Finset α)
    (parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc) : α))
      ((fun (i : ↥P.parts) ↦ Q (↑i : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc)))
    d
⊢ False
have h : ∀ (hbc : ¬b = c) ⦃d : α⦄
  (hdb :
    Membership.mem (γ := Finset α)
      (parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb) : α))
        ((fun (i : ↥P.parts) ↦ Q (↑i : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) b hb)))
      d)
  (hdc :
    Membership.mem (γ := Finset α)
      (parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc) : α))
        ((fun (i : ↥P.parts) ↦ Q (↑i : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) c hc)))
      d),
  False
Tactic: rw [Ne, Subtype.mk_eq_mk] at hbc
Cleared hypotheses: hbc, d, hdb, hdc
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ (insert b P.parts).SupIndep id
have refine : Disjoint (id b) (P.parts.sup id)
Tactic: refine P.supIndep.insert ?_