awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
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)
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)
⊢ 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

Premises used: disjoint_subtype_iff, Finset.sup_coe, Finset.image_subset_iff_subset_preimage, Finpartition.supIndep, Subtype.property
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ sup (P.parts.preimage (Subtype.val (p := Pr)) ⋯) id = Subtype.mk (p := Pr) s hs

Tactic:
simpa [Finset.sup_preimage_val_id Prsup Prbot hP] using P.sup_parts

Premises used: Finpartition.sup_parts, Finset.sup_preimage_val_id
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ⊥ ∉ P.parts.preimage (Subtype.val (p := Pr)) ⋯

Tactic:
simpa [mem_preimage, Subtype.coe_bot Prbot] using P.bot_notMem

Premises used: Subtype.coe_bot, Finset.mem_preimage, Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
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
p : Subtype Pr
⊢ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts ↔ (↑p : α) ∈ P.parts

Tactic:
simp [toSubtype]

Premises used: Finpartition.toSubtype
-- Module: Mathlib.Order.Partition.Finpartition
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
h : ∀ (a : α) (ha : a ∈ P.parts), f a = f (↑(Subtype.mk (p := Pr) a ⋯) : α)
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ P.parts, f p) (∑ p ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts, f (↑p : α))

Tactic:
apply Finset.sum_bij (fun p hpP => ⟨p, hP p hpP⟩)

Premises used: Finset.sum_bij
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ∀ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts),
    Subtype.mk (p := Pr) a₁ ⋯ = Subtype.mk (p := Pr) a₂ ⋯ → a₁ = a₂

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ∀ b ∈ (P.toSubtype (Pr := Pr) Prsup Prinf Prbot hs hP).parts,
    ∃ (a : α) (ha : a ∈ P.parts), Subtype.mk (p := Pr) a ⋯ = b

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ∀ (a : α) (ha : a ∈ P.parts), f a = f (↑(Subtype.mk (p := Pr) a ⋯) : α)

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P Q : Finpartition a
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)
⊢ SupIndep (α := α) (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) id

Tactic:
rw [supIndep_iff_disjoint_erase]

Premises used: Finset.supIndep_iff_disjoint_erase
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P Q : Finpartition a
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
⊢ ∀ (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:
simp only [mem_image, and_imp, forall_exists_index, id, Prod.exists,
          mem_product, Finset.disjoint_sup_right, mem_erase, Ne]

Premises used: Finset.mem_image, and_imp, forall_exists_index, id, Ne, Finset.mem_erase, Finset.disjoint_sup_right, Prod.exists, Finset.mem_product
-- Module: Mathlib.Order.Partition.Finpartition
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₂)
inr : ∀ (xdiff : x₁ ≠ x₂), Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)

Tactic:
rcases eq_or_ne x₁ x₂ with (rfl | xdiff)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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₂)

Tactic:
Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ hy₂ ?_)

Premises used: Finpartition.disjoint, inf_le_right, Disjoint.mono
-- Module: Mathlib.Order.Partition.Finpartition
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₁
inl : y₁ ≠ y₂
⊢ Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)

Tactic:
refine Disjoint.mono inf_le_right inf_le_right (Q.disjoint hy₁ hy₂ ?_)

Premises used: Finpartition.disjoint, inf_le_right, Disjoint.mono
-- Module: Mathlib.Order.Partition.Finpartition
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₁
t : y₁ = y₂
⊢ False

Tactic:
simp [t] at h
-- Module: Mathlib.Order.Partition.Finpartition
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₁
xdiff : x₁ ≠ x₂
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)

Tactic:
Disjoint.mono inf_le_left inf_le_left (P.disjoint hx₁ hx₂ xdiff)

Premises used: Finpartition.disjoint, Disjoint.mono, inf_le_left
-- Module: Mathlib.Order.Partition.Finpartition
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₁
xdiff : x₁ ≠ x₂
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)

Tactic:
exact Disjoint.mono inf_le_left inf_le_left (P.disjoint hx₁ hx₂ xdiff)

Premises used: Finpartition.disjoint, Disjoint.mono, inf_le_left
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P Q : Finpartition a
rw : (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = a
⊢ sup (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) id = a

Tactic:
rw [sup_image, id_comp, sup_product_left]

Premises used: Finset.sup_product_left, Finset.sup_image, Function.id_comp
-- Module: Mathlib.Order.Partition.Finpartition
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
trans₁ : P.parts.sup id ⊓ Q.parts.sup id = a
⊢ (P.parts.sup fun (i : α) ↦ Q.parts.sup fun (i' : α) ↦ (i, i').1 ⊓ (i, i').2) = a

Tactic:
trans P.parts.sup id ⊓ Q.parts.sup id

Premises used: id, Finpartition.parts, Finset.sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P Q : Finpartition a
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)
⊢ (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:
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left]

Premises used: Finset.sup_inf_distrib_left, Finset.sup_inf_distrib_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ 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:
rfl
-- Module: Mathlib.Order.Partition.Finpartition
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
rw₂ rw₃ : a = a
⊢ P.parts.sup id ⊓ Q.parts.sup id = a

Tactic:
rw [P.sup_parts, Q.sup_parts, inf_idem]

Premises used: Finpartition.sup_parts, inf_idem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a : α
P Q : Finpartition a
⊢ (P ⊓ Q).parts = erase (image (fun (bc : α × α) ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) ⊥

Tactic:
rfl

Premises used: Finset.erase, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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
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
⊢ ∃ c ∈ P.parts, b ≤ c

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)

Premises used: Finset.mem_image, Finset.mem_of_mem_erase, Iff.mp, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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.1 ∈ P.parts ∧ c.2 ∈ Q.parts

Tactic:
rw [mem_product] at hc

Premises used: Finset.mem_product
-- Module: Mathlib.Order.Partition.Finpartition
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
hc₁ : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
⊢ c.1 ⊓ c.2 ∈ (P ⊓ Q).parts

Tactic:
rw [mem_product] at hc

Premises used: Finset.mem_product
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ P.parts, c.1 ⊓ c.2 ≤ c_2

Tactic:
⟨c.1, hc.1, inf_le_left⟩

Premises used: Prod.fst, And.left, And.intro, Exists.intro, inf_le_left
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ P.parts, c.1 ⊓ c.2 ≤ c_2

Tactic:
exact ⟨c.1, hc.1, inf_le_left⟩
-- Module: Mathlib.Order.Partition.Finpartition
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
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
⊢ ∃ c ∈ Q.parts, b ≤ c

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)

Premises used: Finset.mem_image, Finset.mem_of_mem_erase, Iff.mp, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_2

Tactic:
⟨c.2, hc.2, inf_le_right⟩

Premises used: inf_le_right, And.right, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c_1 : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_2 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_2

Tactic:
exact ⟨c.2, hc.2, inf_le_right⟩
-- Module: Mathlib.Order.Partition.Finpartition
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
obtain : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), ∃ c ∈ (Q ⊓ R).parts, b ≤ c
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb
-- Module: Mathlib.Order.Partition.Finpartition
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
obtain : ∀ (d : α) (hd : d ∈ R.parts) (hbd : b ≤ d), ∃ c ∈ (Q ⊓ R).parts, b ≤ c
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
obtain ⟨d, hd, hbd⟩ := hPR hb
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ b ≤ c ⊓ d

Tactic:
have h := _root_.le_inf hbc hbd
-- Module: Mathlib.Order.Partition.Finpartition
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
h : b ≤ c ⊓ d
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
⟨c ⊓ d,
          mem_erase_of_ne_of_mem (ne_bot_of_le_ne_bot (P.ne_bot hb) h)
            (mem_image.2 ⟨(c, d), mem_product.2 ⟨hc, hd⟩, rfl⟩),
          h⟩

Premises used: Iff.mpr, ne_bot_of_le_ne_bot, Finset.mem_image, Finset.mem_erase_of_ne_of_mem, Prod.mk, And.intro, Finpartition.ne_bot, Exists.intro, Finset.mem_product, Min.min, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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
h : b ≤ c ⊓ d
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
refine
        ⟨c ⊓ d,
          mem_erase_of_ne_of_mem (ne_bot_of_le_ne_bot (P.ne_bot hb) h)
            (mem_image.2 ⟨(c, d), mem_product.2 ⟨hc, hd⟩, rfl⟩),
          h⟩
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ (∃ 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

Premises used: Finset.coe_erase, Set.mem_image, Finset.coe_image, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.Order.Partition.Finpartition
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 = ⊥
⊢ (∃ 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

Premises used: Finset.coe_erase, Set.mem_image, Finset.coe_image, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.Order.Partition.Finpartition
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 = ⊥
obtain : ∀ (px : α) (hpx : px ∈ (↑P.parts : Set α)) (hxy : px ⊓ b ≠ y), ¬px ⊓ b = ⊥ → (Disjoint on id) (px ⊓ b) y
⊢ (Disjoint on id) x y

Tactic:
obtain ⟨⟨px, hpx, rfl⟩, _⟩ := hx

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
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 = ⊥
obtain :
  ∀ (py : α) (hpy : py ∈ (↑P.parts : Set α)) (hxy : px ⊓ b ≠ py ⊓ b), ¬py ⊓ b = ⊥ → (Disjoint on id) (px ⊓ b) (py ⊓ b)
⊢ (Disjoint on id) (px ⊓ b) y

Tactic:
obtain ⟨⟨py, hpy, rfl⟩, _⟩ := hy

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
px : α
hpx : px ∈ (↑P.parts : Set α)
right : ¬px ⊓ b = ⊥
py : α
hpy : py ∈ (↑P.parts : Set α)
hxy : px ⊓ b ≠ py ⊓ b
right_1 : ¬py ⊓ b = ⊥
⊢ (Disjoint on id) (px ⊓ b) (py ⊓ b)

Tactic:
simpa [Function.onFun, id_eq]
      using (P.disjoint hpx hpy fun h => hxy (h ▸ rfl)).mono inf_le_left inf_le_left

Premises used: Finpartition.disjoint, Function.onFun, Eq.rec, Disjoint.mono, inf_le_left, rfl, id_eq
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderBot α
inst_2 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
simp : (P.parts.sup fun (i : α) ↦ i) ⊓ b = b
⊢ sup (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥) id = b

Tactic:
simp only [sup_erase_bot, sup_image, Function.id_comp, (sup_inf_distrib_right ..).symm]

Premises used: Finset.sup_erase_bot, Finset.sup_inf_distrib_right, Finset.sup_image, Eq.symm, Function.id_comp
-- Module: Mathlib.Order.Partition.Finpartition
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 (x : α) ↦ x) = a

Tactic:
have : P.parts.sup (fun x => x) = a := P.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
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
rw₁ rw₂ : b = b
⊢ (P.parts.sup fun (i : α) ↦ i) ⊓ b = b

Tactic:
rw [this, inf_eq_right.mpr hb]

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Order.Partition.Finpartition
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
by_contra : ∀ (hne : ¬x = y), False
⊢ x = y

Tactic:
by_contra hne
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ x ∈ P.parts ∧ x ⊓ b ≠ ⊥

Tactic:
simp only [Finset.mem_filter] at hx hy

Premises used: Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
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 ≠ ⊥
⊢ y ∈ P.parts ∧ y ⊓ b ≠ ⊥

Tactic:
simp only [Finset.mem_filter] at hx hy

Premises used: Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
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 ≠ ⊥
⊢ 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