awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
r : Finset α
hrs : (↑r : Set α) ⊆ (↑s : Set α)
hr : Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
⊢ ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))

Tactic:
exact ⟨r, mod_cast hrs, hr⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
mp : a ∈ P.part b → ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
mpr : (∃ p ∈ P.parts, a ∈ p ∧ b ∈ p) → a ∈ P.part b
⊢ a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
constructor
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
⊢ b ∈ s

Tactic:
have : b ∈ s := P.part_nonempty.1 ⟨a, h⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
⊢ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
⟨_, ?_, h, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
mp : P.part b ∈ P.parts
mp₁ : b ∈ P.part b
⊢ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
refine ⟨_, ?_, h, ?_⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
⊢ P.part b ∈ P.parts

Tactic:
simp [this]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
⊢ b ∈ P.part b

Tactic:
simp [this]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
⊢ P.part b = p

Tactic:
P.part_eq_of_mem hp hbp

Premises used: Finpartition.part_eq_of_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
⊢ P.part b ∈ P.parts

Tactic:
obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp

Premises used: Finpartition.part_eq_of_mem, Finpartition.part, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
hp₁ : P.part b ∈ P.parts
⊢ a ∈ P.part b

Tactic:
obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp

Premises used: Finpartition.part_eq_of_mem, Finpartition.part, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
hp₁ : P.part b ∈ P.parts
hap₁ : a ∈ P.part b
⊢ b ∈ P.part b

Tactic:
obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp

Premises used: Finpartition.part_eq_of_mem, Finpartition.part, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
hp : P.part b ∈ P.parts
hap : a ∈ P.part b
hbp : b ∈ P.part b
⊢ a ∈ P.part b

Tactic:
hap
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
hp : P.part b ∈ P.parts
hap : a ∈ P.part b
hbp : b ∈ P.part b
⊢ a ∈ P.part b

Tactic:
exact hap
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : ↥s
⊢ (fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
      ((fun (x : ↥s) ↦
          (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
              (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
              (Subtype.mk (p := fun (x_1 : α) ↦
                x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α)) (↑x : α)
                ⋯) :
            (t : ↥P.parts) × ↥(↑t : Finset α)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥(↑t : Finset α)
e : α
a₁ :
  ∀ (p : Finset α) (mp : p ∈ P.parts) (f : α)
    (mf : f ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)),
    Membership.mem (γ := Finset α)
        (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
              ((fun (x : ↥s) ↦
                  (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                      (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                      (Subtype.mk (p := fun (x_1 : α) ↦
                        x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                        (↑x : α) ⋯) :
                    (t : ↥P.parts) × ↥(↑t : Finset α)))
                ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                    Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                  (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
                    (Subtype.mk (p := fun (x : α) ↦
                      x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))))) :
          Finset α)
        e ↔
      e ∈
        (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
              (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
                (Subtype.mk (p := fun (x : α) ↦
                  x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))) :
          Finset α)
⊢ Membership.mem (γ := Finset α)
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                      (↑x : α) ⋯) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                x))) :
        Finset α)
      e ↔
    e ∈ (↑(x.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : Finset α)

Tactic:
obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
p : Finset α
mp : p ∈ P.parts
f : α
mf : f ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)
a₁ : e ∈ P.part f ↔ e ∈ p
⊢ Membership.mem (γ := Finset α)
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                      (↑x : α) ⋯) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                  (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
                  (Subtype.mk (p := fun (x : α) ↦
                    x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))))) :
        Finset α)
      e ↔
    e ∈
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
              (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
              (Subtype.mk (p := fun (x : α) ↦
                x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))) :
        Finset α)

Tactic:
dsimp only at mf ⊢
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
p : Finset α
mp : p ∈ P.parts
f : α
mf : f ∈ p
a₁ a₂ : e ∈ p ↔ e ∈ p
⊢ e ∈ P.part f ↔ e ∈ p

Tactic:
rw [P.part_eq_of_mem mp mf]

Premises used: Finpartition.part_eq_of_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥(↑t : Finset α)
⊢ (↑(Sigma.snd (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                      (↑x : α) ⋯) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                x)) :
          ↥(↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
                  ((fun (x : ↥s) ↦
                      (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                          (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                          (Subtype.mk (p := fun (x_1 : α) ↦
                            x_1 ∈
                              (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                            (↑x : α) ⋯) :
                        (t : ↥P.parts) × ↥(↑t : Finset α)))
                    ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                        Subtype.mk (p := fun (x : α) ↦ x ∈ s)
                          (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                      x))) :
              Finset α)) :
      α) =
    (↑(x.snd (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : α)

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((P.equivSigmaParts.trans
                (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                  Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
              (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
            a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((P.equivSigmaParts.trans
                (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                  Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
              (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
            b))
⊢ ∃ (f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        Eq.{u_1 + 1} (α := ↥P.parts)
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))

Tactic:
use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))

Premises used: Equiv.sigmaCongr, Equiv.trans, Finpartition.equivSigmaParts, Equiv.refl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((P.equivSigmaParts.trans
                (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                  Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
              (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
            a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((P.equivSigmaParts.trans
                (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                  Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
              (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
            b))

Tactic:
simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

Premises used: Equiv.sigmaCongr, Equiv.sigmaCongrLeft, Finpartition.equivSigmaParts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #(P.parts.biUnion id) = #s

Tactic:
congr_arg Finset.card P.biUnion_parts

Premises used: Finpartition.biUnion_parts, congr_arg, Finset.card
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)
⊢ ∑ i ∈ P.parts, #i = #s

Tactic:
convert! congr_arg Finset.card P.biUnion_parts

Premises used: Finpartition.biUnion_parts, congr_arg, Finset.card
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : Eq (α := ℕ) (∑ i ∈ P.parts, #i) (∑ u ∈ P.parts, #(id u))
⊢ ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)

Tactic:
rw [card_biUnion P.supIndep.pairwiseDisjoint]

Premises used: Finset.card_biUnion, Finset.SupIndep.pairwiseDisjoint, Finpartition.supIndep
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ Eq (α := ℕ) (∑ i ∈ P.parts, #i) (∑ u ∈ P.parts, #(id u))

Tactic:
rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
rw :
  Set.PairwiseDisjoint (α := Finset α)
    ((⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) '' (↑s : Set α)) id
⊢ (↑(Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s) : Set (Finset α)).PairwiseDisjoint id

Tactic:
rw [Finset.coe_map]

Premises used: Finset.coe_map
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
⊢ Set.PairwiseDisjoint (α := Finset α)
    ((⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) '' (↑s : Set α)) id

Tactic:
Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)

Premises used: Finset.pairwiseDisjoint_range_singleton, Set.image_subset_range, Set.PairwiseDisjoint.subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
⊢ Set.PairwiseDisjoint (α := Finset α)
    ((⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) '' (↑s : Set α)) id

Tactic:
exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)

Premises used: Finset.pairwiseDisjoint_range_singleton, Set.image_subset_range, Set.PairwiseDisjoint.subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
rw : s.sup (id ∘ (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α)) = s
rw₁ : s.sup (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) = s
rw₂ : s.sup singleton = s
rw₃ rw₄ : s = s
⊢ (Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).sup id = s

Tactic:
rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]

Premises used: Finset.sup_singleton_eq_self, Finset.sup_map, Function.Embedding.coeFn_mk, Function.id_comp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
⊢ ⊥ ∉ Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ parts (a := s) ⊥ = Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ card.{u_1} (α := Finset α) (parts (a := s) ⊥) = #s

Tactic:
Finset.card_map _

Premises used: Finset.card_map, Finset.map
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) t ↔ ∃ a ∈ s, {a} = t

Tactic:
mem_map

Premises used: Set.Mem, setOf, Finset.mem_map
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) t
⊢ ∃ a ∈ s, {a} = t

Tactic:
rw [mem_bot_iff] at ht

Premises used: Finpartition.mem_bot_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : ∃ a ∈ s, {a} = t
obtain : ∀ (a : α) (ha : a ∈ s), ∃ c ∈ P.parts, {a} ≤ c
⊢ ∃ c ∈ P.parts, t ≤ c

Tactic:
obtain ⟨a, ha, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P_1 : Finpartition s_1
a_1 : α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
obtain : ∀ (t : Finset α) (ht : t ∈ P.parts) (hat : a ∈ t), ∃ c ∈ P.parts, {a} ≤ c
⊢ ∃ c ∈ P.parts, {a} ≤ c

Tactic:
obtain ⟨t, ht, hat⟩ := P.exists_mem ha

Premises used: Finpartition.exists_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a_1 : α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
hat : a ∈ t
⊢ ∃ c ∈ P.parts, {a} ≤ c

Tactic:
⟨t, ht, singleton_subset_iff.2 hat⟩

Premises used: Iff.mpr, Finset.singleton_subset_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a_1 : α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
hat : a ∈ t
⊢ ∃ c ∈ P.parts, {a} ≤ c

Tactic:
exact ⟨t, ht, singleton_subset_iff.2 hat⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
rw : #P.parts ≤ card.{u_1} (α := Finset α) (parts (a := s) ⊥)
⊢ #P.parts ≤ #s

Tactic:
rw [← card_bot s]

Premises used: Finpartition.card_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ card.{u_1} (α := Finset α) (parts (a := s) ⊥)

Tactic:
card_mono bot_le

Premises used: Finpartition.card_mono, bot_le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ card.{u_1} (α := Finset α) (parts (a := s) ⊥)

Tactic:
exact card_mono bot_le

Premises used: Finpartition.card_mono, bot_le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
inl : ∀ (h : #P.parts = 0), #s % #P.parts ≤ #P.parts
inr : ∀ (h : #P.parts > 0), #s % #P.parts ≤ #P.parts
⊢ #s % #P.parts ≤ #P.parts

Tactic:
obtain h | h := (#P.parts).eq_zero_or_pos

Premises used: Finpartition.parts, Finset.card, Nat.eq_zero_or_pos
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
inl : #s % 0 ≤ 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
rw [h]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s = 0

Tactic:
rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h

Premises used: Finset.bot_eq_empty, Finpartition.parts_eq_empty_iff, Finset.card_eq_zero
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
inl inl₁ : HMod.hMod (α := ℕ) 0 0 ≤ HMod.hMod (α := ℕ) 0 0
⊢ #s % 0 ≤ 0

Tactic:
rw [h]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
(Nat.mod_lt _ h).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
exact (Nat.mod_lt _ h).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
simp :
  ∀ a ∈ x,
    ∀ a_2 ∈ x,
      ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a x_3) (x : x_3 ∈ x)
        (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ SupIndep (α := Finset α) (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id

Tactic:
simp only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise, coe_image,
        Set.mem_image, mem_coe, ne_eq, onFun, id_eq, disjoint_iff_ne, forall_mem_not_eq,
        forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_filter, not_and, filter_inj',
        not_forall, @not_imp_comm (_ ↔ _), Decidable.not_not]

Premises used: Finset.forall_mem_not_eq, Function.onFun, and_imp, not_imp_comm, Set.PairwiseDisjoint, Set.mem_image, forall_exists_index, Finset.supIndep_iff_pairwiseDisjoint, Finset.coe_image, Finset.disjoint_iff_ne, Set.Pairwise, ne_eq, Finset.mem_filter, Decidable.not_not, Finset.filter_inj', not_and, Classical.not_forall, Finset.mem_coe, forall_apply_eq_imp_iff₂, id_eq
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
_ :
  a_1 ∈ x →
    ∀ a ∈ x,
      ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
        (h : (s : α → α → Prop) a x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a x_1
⊢ a_1 ∈ x →
    ∀ a ∈ x,
      ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
        (h : (s : α → α → Prop) a x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a x_1

Tactic:
_