awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this_1 : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b a
have grw : Disjoint b ((Q.parts.erase b).sup id)
Tactic: grw [← P.sup_parts, this]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra : (¬∃ c ∈ P.parts, c ≤ b) → False
Tactic: classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra by_contra₁ by_contra₂ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra₃ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), Disjoint b a
Tactic: classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra by_contra₁ by_contra₂ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
by_contra₃ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), Disjoint b a
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra₄ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q), Disjoint b a
Tactic: classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra by_contra₁ by_contra₂ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
by_contra₃ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), Disjoint b a
by_contra₄ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q), Disjoint b a
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra₅ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q)
  (this : P.parts.sup id ≤ (Q.parts.erase b).sup id), Disjoint b a
Tactic: classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra by_contra₁ by_contra₂ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
by_contra₃ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), Disjoint b a
by_contra₄ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q), Disjoint b a
by_contra₅ :
  ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q)
    (this : P.parts.sup id ≤ (Q.parts.erase b).sup id), Disjoint b a
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra₆ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q)
  (this : P.parts.sup id ≤ (Q.parts.erase b).sup id), Disjoint b ((Q.parts.erase b).sup id)
Tactic: classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts
have this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
Tactic: have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
⊢ #Q.parts ≤ #P.parts
have choose : ∀ (f : (b : α) → b ∈ Q.parts → α) (hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts)
  (hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b), #Q.parts ≤ #P.parts
Tactic: choose f hP hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts ≤ #P.parts
have rw : #Q.parts.attach ≤ #P.parts
Tactic: rw [← card_attach]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts
have refine : ∀ b ∈ (↑Q.parts.attach : Set ↥Q.parts),
  ∀ c ∈ (↑Q.parts.attach : Set ↥Q.parts),
    ∀ (h : Eq.{u_1 + 1} (α := α) ((fun (b : ↥Q.parts) ↦ f (↑b : α) sorry) b) ((fun (b : ↥Q.parts) ↦ f (↑b : α) sorry) c)), b = c
Tactic: refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
⊢ Disjoint (id i) (t.sup id)
have this₁ : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
Tactic: have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ Disjoint (id i) (t.sup id)
have rw : Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
Tactic: rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
have a₁ : image (Subtype.val (p := Pr)) t ⊆ P.parts
Tactic: apply P.supIndep
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
a₁ : image (Subtype.val (p := Pr)) t ⊆ P.parts
⊢ Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
have a₂ : (↑(id i) : α) ∈ P.parts
Tactic: apply P.supIndep
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
a₁ : image (Subtype.val (p := Pr)) t ⊆ P.parts
a₂ : (↑(id i) : α) ∈ P.parts
⊢ Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
have a₃ : (↑(id i) : α) ∉ image (Subtype.val (p := Pr)) t
Tactic: apply P.supIndep
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
⊢ Disjoint (id i) (t.sup id)
have have : ∀ (this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))),
  Disjoint (id i) (t.sup id)
Tactic: classical
      have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
      rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
      · apply P.supIndep
        · simpa [image_subset_iff_subset_preimage] using ht
        · simpa using hi
        · simpa [i.property] using hi'
      exact Prsup
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
have have₁ have₂ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))),
    Disjoint (id i) (t.sup id)
⊢ Disjoint (id i) (t.sup id)
have have₃ : ∀ (this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))),
  Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
Tactic: classical
      have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
      rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
      · apply P.supIndep
        · simpa [image_subset_iff_subset_preimage] using ht
        · simpa using hi
        · simpa [i.property] using hi'
      exact Prsup
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
have have₁ have₂ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))),
    Disjoint (id i) (t.sup id)
have₃ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))),
    Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
⊢ Disjoint (id i) (t.sup id)
have have₄ : ∀ (this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr)))
  ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)
Tactic: classical
      have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
      rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
      · apply P.supIndep
        · simpa [image_subset_iff_subset_preimage] using ht
        · simpa using hi
        · simpa [i.property] using hi'
      exact Prsup
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
X : Type u_2
inst_2 : AddCommMonoid X
f : α → X
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ P.parts, f p) (∑ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, f (↑p : α))
have hi : ∀ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a sorry ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts
Tactic: apply Finset.sum_bij (fun p hpP => ⟨p, hP p hpP⟩)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
X : Type u_2
inst_2 : AddCommMonoid X
f : α → X
hi : ∀ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ P.parts, f p) (∑ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, f (↑p : α))
have i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts),
  Subtype.mk (p := Pr) a₁ sorry = Subtype.mk (p := Pr) a₂ sorry → a₁ = a₂
Tactic: apply Finset.sum_bij (fun p hpP => ⟨p, hP p hpP⟩)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
X : Type u_2
inst_2 : AddCommMonoid X
f : α → X
hi : ∀ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts
i_inj :
  ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts),
    Subtype.mk (p := Pr) a₁ ⋯ = Subtype.mk (p := Pr) a₂ ⋯ → a₁ = a₂
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ P.parts, f p) (∑ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, f (↑p : α))
have i_surj : ∀ b ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, ∃ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a sorry = b
Tactic: apply Finset.sum_bij (fun p hpP => ⟨p, hP p hpP⟩)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
X : Type u_2
inst_2 : AddCommMonoid X
f : α → X
hi : ∀ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts
i_inj :
  ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts),
    Subtype.mk (p := Pr) a₁ ⋯ = Subtype.mk (p := Pr) a₂ ⋯ → a₁ = a₂
i_surj :
  ∀ b ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts,
    ∃ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ = b
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ P.parts, f p) (∑ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, f (↑p : α))
have h : ∀ (a : α) (ha : a ∈ P.parts), f a = f (↑(Subtype.mk (p := Pr) a sorry) : α)
Tactic: apply Finset.sum_bij (fun p hpP => ⟨p, hP p hpP⟩)
-- 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 Q : Finpartition a
⊢ SupIndep (α := α) (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) id
have rw : ∀ (i : α),
  Membership.mem (γ := Finset α) (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) i →
    Disjoint (id i) ((erase (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) i).sup id)
Tactic: rw [supIndep_iff_disjoint_erase]
-- 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 Q : Finpartition a
⊢ ∀ (i : α),
    Membership.mem (γ := Finset α) (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) i →
      Disjoint (id i) ((erase (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) i).sup id)
have simp : ∀ (i x x_1 : α),
  x ∈ P.parts →
    x_1 ∈ Q.parts →
      x ⊓ x_1 = i → ∀ ⦃i_1 : α⦄, ¬i_1 = i → ∀ (x x_2 : α), x ∈ P.parts → x_2 ∈ Q.parts → x ⊓ x_2 = i_1 → Disjoint i i_1
Tactic: simp only [mem_image, and_imp, forall_exists_index, id, Prod.exists,
          mem_product, Finset.disjoint_sup_right, mem_erase, Ne]
-- 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 Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
have inl : ∀ (hx₂ : x₁ ∈ P.parts) (h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁), Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)
Tactic: rcases eq_or_ne x₁ x₂ with (rfl | xdiff)
Cleared hypotheses: x₂, hx₂, h
-- 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 Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
inl : ∀ (hx₂ : x₁ ∈ P.parts) (h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁), Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
have inr : ∀ (xdiff : x₁ ≠ x₂), Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
Tactic: rcases eq_or_ne x₁ x₂ with (rfl | xdiff)
-- 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 Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)
have inl : y₁ ≠ y₂
Tactic: refine Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ 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 Q : Finpartition a
⊢ sup (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) id = a
have rw : (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = a
Tactic: rw [sup_image, id_comp, sup_product_left]
-- 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 Q : Finpartition a
⊢ (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = a
have trans : (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = P.parts.sup id ⊓ Q.parts.sup id
Tactic: trans P.parts.sup id ⊓ Q.parts.sup id
-- 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 Q : Finpartition a
trans : (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = P.parts.sup id ⊓ Q.parts.sup id
⊢ (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = a
have trans₁ : P.parts.sup id ⊓ Q.parts.sup id = a
Tactic: trans P.parts.sup id ⊓ Q.parts.sup id
-- 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 Q : Finpartition a
⊢ (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = P.parts.sup id ⊓ Q.parts.sup id
have simp_rw : Eq (α := α) (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ i ⊓ i')
  (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i_1 : α) ↦ id i ⊓ id i_1)
Tactic: simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]
-- 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 Q : Finpartition a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a
have rw : a ⊓ Q.parts.sup id = a
Tactic: rw [P.sup_parts, Q.sup_parts, inf_idem]
-- 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 Q : Finpartition a
rw : a ⊓ Q.parts.sup id = a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a
have rw₁ : a ⊓ a = a
Tactic: rw [P.sup_parts, Q.sup_parts, inf_idem]
-- 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 Q : Finpartition a
rw : a ⊓ Q.parts.sup id = a
rw₁ : a ⊓ a = a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a
have rw₂ : a = a
Tactic: rw [P.sup_parts, Q.sup_parts, inf_idem]