mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
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
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset
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
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #(G.edgeFinset ∩ s.sym2) = #(induce (↑s) G).edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #(G.edgeFinset ∩ s.sym2) = #(induce (↑s) G).edgeFinset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ ∅.sup id = ⊥

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ ∅.sup id = ⊥
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ id b ∈ P.parts

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ id b ∈ P.parts
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:
]

Goal state after:
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)
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition ⊥)
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
⊢ #(map f.sym2Map G.edgeFinset) = #G.edgeFinset

Tactic:
]

Goal state after:
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
⊢ #(map f.sym2Map G.edgeFinset) = #G.edgeFinset
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ∈ Q.parts

pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ∈ Q.parts

case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ d

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ d
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ∈ P.parts

pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ∈ P.parts

case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ b
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ d

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ d
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}) + #P.parts * (#s / #P.parts) = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) + #P.parts * (#s / #P.parts) = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
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

Tactic:
]

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

Tactic:
]

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 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
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b ((Q.parts.erase b).sup id)

Tactic:
]

Goal state after:
α : 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
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b ((Q.parts.erase b).sup id)
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}) + #P.parts * (#s / #P.parts) = #s
⊢ #s = #s

Tactic:
]

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
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts
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 ∈ P.parts | #p = #s / #P.parts})

Tactic:
]

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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint (↑(id i)) ((image Subtype.val t).sup id)

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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)

Tactic:
]

Goal state after:
α : 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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ Disjoint (↑(id i)) ((image Subtype.val t).sup id)

α : 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
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)
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 + 1

Tactic:
]

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
⊢ ∀ i ∈ image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts),
    Disjoint (id i) (((image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase i).sup id)

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ ∀ i ∈ image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts),
    Disjoint (id i) (((image (fun bc ↦ bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase i).sup id)
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
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ (i, i').1 ⊓ (i, i').2) = a

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ (i, i').1 ⊓ (i, i').2) = a
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
⊢ a = a

Tactic:
]

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
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ P.parts, c.1 ⊓ c.2 ≤ c_1

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ P.parts, c.1 ⊓ c.2 ≤ c_1
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
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_1

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
P Q : Finpartition a
c : α × α
hc : c.1 ∈ P.parts ∧ c.2 ∈ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_1
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
this : (P.parts.sup fun x ↦ x) = a
⊢ b = b

Tactic:
]

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 ∈ P.parts ∧ x ⊓ b = ⊥
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p = ∑ a ∈ parts.erase ⊥, f a

pp: case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∀ a ∈ {⊥}, a ∉ parts.erase ⊥ → f a = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ ({⊥} ∪ parts.erase ⊥).erase ⊥, f p = ∑ a ∈ parts.erase ⊥, f a

case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∀ a ∈ {⊥}, a ∉ parts.erase ⊥ → f a = 0
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ 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:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ 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
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ¬∃ a_1 ∈ I, ⊥ ∈ (P a_1).parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ¬∃ a_1 ∈ I, ⊥ ∈ (P a_1).parts
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.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)

Tactic:
]

Goal state after:
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.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ (P i).parts → a ∉ (P j).parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ (P i).parts → a ∉ (P j).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P✝ : Finpartition a
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ a = a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot
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 : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂

Tactic:
]

Goal state after:
case bot
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 : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts → a_1 ∉ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts → a_1 ∉ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : 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 : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts
hdc : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : 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 : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts
hdc : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
⊢ False
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint a (id b)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint a (id b)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top
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 : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁

Tactic:
]

Goal state after:
case top
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 : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁