awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≠ ⊥
this : Disjoint (x ⊓ b) (y ⊓ b)
⊢ False

Tactic:
grind
-- 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 ∈ {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
-- 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
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
⊢ Eq (α := Finset α) (erase (image (fun (x : α) ↦ x ⊓ b) P.parts) ⊥)
    (image (fun (x : α) ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥}))

Tactic:
grind
-- 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
hinj : ∀ x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, ∀ y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}, x ⊓ b = y ⊓ b → x = y
⊢ 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
-- 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
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 ≠ ⊥}
⊢ x ∈ P.parts ∧ x ⊓ b = ⊥

Tactic:
simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx

Premises used: ne_eq, Finset.mem_filter, Decidable.not_not
-- 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
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ f (x ⊓ b) = 0

Tactic:
rw [hx.2, hf]

Premises used: And.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
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) (∑ 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]
-- 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
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 ≠ ⊥}))
hz : Eq.{u_2 + 1} (α := M) (∑ x ∈ P.parts with ¬x ⊓ b ≠ ⊥, f (x ⊓ b)) 0
⊢ Eq.{u_2 + 1} (α := M) (∑ p ∈ (P.restrict hb).parts, f p) (∑ q ∈ P.parts, f (q ⊓ b))

Tactic:
simp only [restrict, heq, ← Finset.sum_filter_add_sum_filter_not P.parts (· ⊓ b ≠ ⊥), hz,
    Finset.sum_image hinj, add_zero]

Premises used: Ne, Bot.bot, Finpartition.parts, Finset.sum_filter_add_sum_filter_not, Finpartition.restrict, Finset.sum_image, add_zero, Min.min
-- Module: Mathlib.Order.Partition.Finpartition
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)
neg :
  ∀ (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)

Tactic:
by_cases hbot : ⊥ ∈ parts
-- Module: Mathlib.Order.Partition.Finpartition
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)
pos₁ : ∀ (a : α), Membership.mem (γ := Finset α) {⊥} a → a ∉ parts.erase ⊥ → f a = 0
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ parts.erase ⊥, f p) (∑ p ∈ parts, f p)

Tactic:
rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]

Premises used: Finset.union_comm, Bot.bot, Finset.erase_union_eq, Finset.sum_union_eq_right
-- Module: Mathlib.Order.Partition.Finpartition
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 ⊥).erase ⊥, f p) (∑ a ∈ parts.erase ⊥, f a)

Tactic:
simp
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ ∀ (a : α), Membership.mem (γ := Finset α) {⊥} a → a ∉ parts.erase ⊥ → f a = 0

Tactic:
grind
-- Module: Mathlib.Order.Partition.Finpartition
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 ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p) (∑ p ∈ parts, f p)

Tactic:
simp_all
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ SupIndep.{u_1, u_2} (α := α) I fun (i : ι) ↦ (P i).parts.sup id

Tactic:
simpa only [sup_parts]

Premises used: Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
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
rw : (I.sup fun (x : ι) ↦ (P x).parts.sup id) = I.sup a
⊢ sup (I.biUnion fun (i : ι) ↦ (P i).parts) id = I.sup a

Tactic:
rw [sup_biUnion]

Premises used: Finset.sup_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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.sup fun (x : ι) ↦ (P x).parts.sup id) = I.sup a

Tactic:
sup_congr rfl fun i _ => (P i).sup_parts

Premises used: Finset.sup_congr, Finpartition.sup_parts, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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.sup fun (x : ι) ↦ (P x).parts.sup id) = I.sup a

Tactic:
exact sup_congr rfl fun i _ => (P i).sup_parts

Premises used: Finset.sup_congr, Finpartition.sup_parts, rfl
-- Module: Mathlib.Order.Partition.Finpartition
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
rw : ¬∃ a_2 ∈ I, ⊥ ∈ (P a_2).parts
⊢ ⊥ ∉ I.biUnion fun (i : ι) ↦ (P i).parts

Tactic:
rw [mem_biUnion]

Premises used: Finset.mem_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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
push : ∀ (a_2 : ι) (_ : a_2 ∈ I), ⊥ ∉ (P a_2).parts
⊢ ¬∃ a_2 ∈ I, ⊥ ∈ (P a_2).parts

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Order.Partition.Finpartition
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 : ι) (_ : a_2 ∈ I), ⊥ ∉ (P a_2).parts

Tactic:
fun i _ => (P i).bot_notMem

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
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 : ι) (_ : a_2 ∈ I), ⊥ ∉ (P a_2).parts

Tactic:
exact fun i _ => (P i).bot_notMem

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
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)

Tactic:
Finset.sum_biUnion fun i hi j hj hij => ?_

Premises used: Finset.sum_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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
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
⊢ Eq.{u_3 + 1} (α := M) (∑ p ∈ I.biUnion fun (i : ι) ↦ (P i).parts, f p) (∑ i ∈ I, ∑ p ∈ (P i).parts, f p)

Tactic:
refine Finset.sum_biUnion fun i hi j hj hij => ?_

Premises used: Finset.sum_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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
rw : ∀ ⦃a : α⦄, a ∈ (P i).parts → a ∉ (P j).parts
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset α) Disjoint (fun (i : ι) ↦ (P i).parts) i j

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Premises used: Function.onFun, Finset.disjoint_left
-- Module: Mathlib.Order.Partition.Finpartition
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
⊢ Disjoint p p

Tactic:
have hp_disj : Disjoint p p := (ha.pairwiseDisjoint hi hj hij).mono ((P i).le hpi) ((P j).le hpj)
-- Module: Mathlib.Order.Partition.Finpartition
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
hp_disj : Disjoint p p
⊢ False

Tactic:
(P i).ne_bot hpi (disjoint_self.mp hp_disj)

Premises used: Finpartition.ne_bot, Iff.mp, disjoint_self
-- Module: Mathlib.Order.Partition.Finpartition
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
hp_disj : Disjoint p p
⊢ False

Tactic:
exact (P i).ne_bot hpi (disjoint_self.mp hp_disj)

Premises used: Finpartition.ne_bot, Iff.mp, disjoint_self
-- Module: Mathlib.Order.Partition.Finpartition
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
rw₂ rw₃ : a = a
⊢ P.parts.attach.sup (Subtype.val (p := fun (x : α) ↦ x ∈ P.parts)) = a

Tactic:
rw [Finset.sup_attach (f := fun x => x), ← Function.id_def, P.sup_parts]

Premises used: Function.id_def, Finset.sup_attach, Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
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
rw : (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts) ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts
⊢ b ∈ (P.bind Q).parts ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
rw [bind_parts, mem_biUnion]

Premises used: Finpartition.bind_parts, Finset.mem_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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
mpr : (∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q (↑a_2 : α) ⋯).parts
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts) ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
constructor
-- Module: Mathlib.Order.Partition.Finpartition
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 : α
hA : A ∈ P.parts
h :
  b ∈
    parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) A hA) : α))
      (Q (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) A hA) : α) ⋯)
⊢ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
⟨A, hA, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
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 : α
hA : A ∈ P.parts
h :
  b ∈
    parts (a := (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) A hA) : α))
      (Q (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ P.parts) A hA) : α) ⋯)
⊢ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
exact ⟨A, hA, h⟩
-- Module: Mathlib.Order.Partition.Finpartition
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 : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts

Tactic:
⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

Premises used: Finset.mem_attach, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
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 : α
hA : A ∈ P.parts
h : b ∈ (Q A hA).parts
⊢ ∃ a_1 ∈ P.parts.attach, b ∈ (Q (↑a_1 : α) ⋯).parts

Tactic:
exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩
-- Module: Mathlib.Order.Partition.Finpartition
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
h :
  (↑P.parts.attach : Set ↥P.parts).PairwiseDisjoint (α := Finset α) fun (i : ↥P.parts) ↦
    parts (a := (↑i : α)) ((fun (i : ↥P.parts) ↦ Q (↑i : α) ⋯) i)
⊢ #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q (↑A : α) ⋯).parts

Tactic:
apply card_biUnion

Premises used: Finset.card_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
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
h :
  ∀ ⦃a_1 : α⦄,
    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)))
        a_1 →
      a_1 ∉
        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))
⊢ 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)

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Premises used: Function.onFun, Finset.disjoint_left
-- Module: Mathlib.Order.Partition.Finpartition
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
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 : α) ⋯) (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
⊢ False

Tactic:
rw [Ne, Subtype.mk_eq_mk] at hbc

Premises used: Ne, Subtype.mk_eq_mk
-- Module: Mathlib.Order.Partition.Finpartition
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 : ¬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 : α) ⋯) (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

Tactic:
(Q b hb).ne_bot hdb
      (eq_bot_iff.2 <|
        (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)

Premises used: Iff.mpr, Disjoint.le_bot, Finpartition.disjoint, le_inf, Finpartition.ne_bot, Finpartition.le, LE.le.trans, eq_bot_iff
-- Module: Mathlib.Order.Partition.Finpartition
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 : ¬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 : α) ⋯) (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

Tactic:
exact
    (Q b hb).ne_bot hdb
      (eq_bot_iff.2 <|
        (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)

Premises used: Iff.mpr, Disjoint.le_bot, Finpartition.disjoint, le_inf, Finpartition.ne_bot, Finpartition.le, LE.le.trans, eq_bot_iff
-- Module: Mathlib.Order.Partition.Finpartition
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

Tactic:
P.supIndep.insert ?_

Premises used: Finset.SupIndep.insert, Finpartition.supIndep
-- Module: Mathlib.Order.Partition.Finpartition
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
refine : Disjoint (id b) (P.parts.sup id)
⊢ (insert b P.parts).SupIndep id

Tactic:
refine P.supIndep.insert ?_

Premises used: Finset.SupIndep.insert, Finpartition.supIndep
-- Module: Mathlib.Order.Partition.Finpartition
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
rwa : Disjoint (id b) a
rwa₁ rwa₂ rwa₃ rwa₄ : Disjoint a (id b)
⊢ Disjoint (id b) (P.parts.sup id)

Tactic:
rwa [sup_parts, disjoint_comm]

Premises used: disjoint_comm, Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
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
rwa : id b ⊔ P.parts.sup id = c
rwa₁ : id b ⊔ a = c
rwa₂ : b ⊔ a = c
rwa₃ rwa₄ rwa₅ rwa₆ : a ⊔ b = c
⊢ (insert b P.parts).sup id = c

Tactic:
rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]

Premises used: Finset.sup_insert, id, sup_comm, Finpartition.sup_parts