mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v ∩ s.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #s / #P.parts ≤ #t

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ (induce s G).degree v = G.degree ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ {p ∈ P.parts | ¬#p = #s / #P.parts + 1} = {p ∈ P.parts | #p = #s / #P.parts}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e).symm.toEmbedding u ⊆ P.parts
x✝¹ : β
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
hb : (↑e).symm x✝¹ ∈ P.parts
⊢ (↑e).symm x✝¹ ∉ Finset.map (↑e).symm.toEmbedding u

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ x ∈ P.parts with #x = #s / #P.parts + 1, #x + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ ∀ x ∈ {x ∈ P.parts | #x = #s / #P.parts + 1}, #x = #s / #P.parts + 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.minDegree ≤ (induce s G).minDegree

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : u ⊆ Finset.map (↑e).toEmbedding P.parts
x✝¹ : β
hb : x✝¹ ∈ Finset.map (↑e).toEmbedding P.parts
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
⊢ x✝ ≤ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
⊢ {e ∈ G.edgeFinset | e.toFinset ⊆ s} = G.edgeFinset ∩ s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ (Finset.map (↑e).toEmbedding P.parts).sup id = e a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ ⊥ ∉ Finset.map (↑e).toEmbedding P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts + 1) + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ ∀ x ∈ {p ∈ P.parts | #p = #s / #P.parts}, #x = #s / #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
⊢ (↑P.parts).PairwiseDisjoint f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts.Nonempty ↔ a ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
P : Finpartition ⊥
⊢ P = default

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ (SimpleGraph.map (⇑f) G).edgeFinset = map f.sym2Map G.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ Nonempty (Finpartition a)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ #(SimpleGraph.map (⇑f) G).edgeFinset = #G.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ P = indiscrete ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P x✝ Q R : Finpartition a
hPQ : x✝ ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x✝.parts
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
⊢ P = Q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
⊢ P ≤ if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
inst✝ : Decidable (a = ⊥)
⊢ ⊤.parts ⊆ {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ∈ s.powerset.powerset

Tactic:
mem_powerset

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ⊆ s.powerset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset

Tactic:
mem_powerset

Goal state after:
case refine_1
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ⊆ s
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P ∈
    image
      (fun ps ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
⊢ P.parts.sup id ≤ (Q.parts.erase b).sup id

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
x y z : EInt
f : x ⟶ y
g : y ⟶ z
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ z) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 z))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) z f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) z f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) z f)
      x (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) y f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) y f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) y f)
        x f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ z) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 z))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) z f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) z f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) z f)
        y g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
⊢ (t.eTruncGE.obj i).Additive

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
x✝ : Finset α
ha : x✝ ∈ P.parts
⊢ ¬#x✝ = #s / #P.parts + 1 ↔ #x✝ = #s / #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts }

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : 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✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
⊢ Disjoint (id i) (t.sup id)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : 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✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
⊢ (P.parts.preimage Subtype.val ⋯).sup id = ⟨s, hs⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : 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✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
⊢ ⊥ ∉ P.parts.preimage Subtype.val ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : 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 Prsup Prinf Prbot hs hP).parts ↔ ↑p ∈ P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : 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✝ : AddCommMonoid X
f : α → X
⊢ ∑ p ∈ P.parts, f p = ∑ p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts, f ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).SupIndep id

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).sup id = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ P.parts, b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ Q.parts, b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : EInt
hab : a ⟶ b
⊢ t.eTruncGE.map hab ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 a ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q R : Finpartition a
hPQ : P ≤ Q
hPR : P ≤ R
b : α
hb : b ∈ P.parts
⊢ ∃ c ∈ (Q ⊓ R).parts, b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ IsIso (t.eTruncLTι ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
x : α
hx : x ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
y : α
hy : y ∈ ↑((image (fun x ↦ x ⊓ b) P.parts).erase ⊥)
hxy : x ≠ y
⊢ (Disjoint on id) x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ ((image (fun x ↦ x ⊓ b) P.parts).erase ⊥).sup id = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.map f).app X ≫ (t.eTruncLTι j).app X = (t.eTruncLTι i).app X

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
x : α
hx : x ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
y : α
hy : y ∈ {x ∈ P.parts | x ⊓ b ≠ ⊥}
hxy : x ⊓ b = y ⊓ b
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : 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
⊢ (image (fun x ↦ x ⊓ b) P.parts).erase ⊥ = image (fun x ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥})

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i : EInt
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ IsIso (t.eTruncGEπ ⊥)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : 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 : (image (fun x ↦ x ⊓ b) P.parts).erase ⊥ = image (fun x ↦ x ⊓ b) ({x ∈ P.parts | x ⊓ b ≠ ⊥})
x : α
hx : x ∈ {x ∈ P.parts | ¬x ⊓ b ≠ ⊥}
⊢ f (x ⊓ b) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncGEπ i).app X ≫ (t.eTruncGE.map f).app X = (t.eTruncGEπ j).app X

Tactic:
by

Goal state after: