mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case bot.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
hab✝ : ⊥ ⟶ ⊥
hab : True
⊢ 𝟙 (𝟭 C) ≫ 0 = 0 ≫ Functor.whiskerRight (𝟙 0) (shiftFunctor C 1)

pp: case bot.coe
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✝ : ℤ
hab✝ : ⊥ ⟶ WithBotTop.coe a✝
hab : True
⊢ t.truncGEπ a✝ ≫ t.truncGEδLT a✝ = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)

pp: case bot.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
hab✝ : ⊥ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)

Tactic:
<;>

Goal state after:
case bot.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
hab✝ : ⊥ ⟶ ⊥
hab : True
⊢ 𝟙 (𝟭 C) ≫ 0 = 0 ≫ Functor.whiskerRight (𝟙 0) (shiftFunctor C 1)

case bot.coe
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✝ : ℤ
hab✝ : ⊥ ⟶ WithBotTop.coe a✝
hab : True
⊢ t.truncGEπ a✝ ≫ t.truncGEδLT a✝ = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)

case bot.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
hab✝ : ⊥ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = 0 ≫ Functor.whiskerRight 0 (shiftFunctor C 1)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊥
hab : WithBotTop.coe a✝ ≤ ⊥
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊥ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

pp: case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : WithBotTop.coe a✝¹ ≤ WithBotTop.coe a✝
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝¹) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

pp: case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : WithBotTop.coe a✝ ≤ ⊤
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
<;>

Goal state after:
case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊥
hab : WithBotTop.coe a✝ ≤ ⊥
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊥ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : WithBotTop.coe a✝¹ ≤ WithBotTop.coe a✝
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝¹) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : WithBotTop.coe a✝ ≤ ⊤
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case hi
α : 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
⊢ ∀ (a : α) (ha : a ∈ P.parts), ⟨a, ⋯⟩ ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts

pp: case i_inj
α : 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
⊢ ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts), ⟨a₁, ⋯⟩ = ⟨a₂, ⋯⟩ → a₁ = a₂

pp: case i_surj
α : 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
⊢ ∀ b ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts, ∃ a, ∃ (ha : a ∈ P.parts), ⟨a, ⋯⟩ = b

pp: case h
α : 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
⊢ ∀ (a : α) (ha : a ∈ P.parts), f a = f ↑⟨a, ⋯⟩

Tactic:
<;>

Goal state after:
case hi
α : 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
⊢ ∀ (a : α) (ha : a ∈ P.parts), ⟨a, ⋯⟩ ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts

case i_inj
α : 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
⊢ ∀ (a₁ : α) (ha₁ : a₁ ∈ P.parts) (a₂ : α) (ha₂ : a₂ ∈ P.parts), ⟨a₁, ⋯⟩ = ⟨a₂, ⋯⟩ → a₁ = a₂

case i_surj
α : 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
⊢ ∀ b ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts, ∃ a, ∃ (ha : a ∈ P.parts), ⟨a, ⋯⟩ = b

case h
α : 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
⊢ ∀ (a : α) (ha : a ∈ P.parts), f a = f ↑⟨a, ⋯⟩
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : #p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : ¬#p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : #p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : ¬#p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝¹) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

pp: case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
<;>

Goal state after:
case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝¹) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.natTransTruncGEOfLE a✝¹ a✝ ⋯ ≫ t.truncGEδLT a✝ =
    t.truncGEδLT a✝¹ ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a✝¹ a✝ ⋯) (shiftFunctor C 1)

pp: case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = t.truncGEδLT a✝ ≫ Functor.whiskerRight (t.truncLTι a✝) (shiftFunctor C 1)

Tactic:
<;>

Goal state after:
case coe.coe
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✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.natTransTruncGEOfLE a✝¹ a✝ ⋯ ≫ t.truncGEδLT a✝ =
    t.truncGEδLT a✝¹ ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a✝¹ a✝ ⋯) (shiftFunctor C 1)

case coe.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
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ 0 ≫ 0 = t.truncGEδLT a✝ ≫ Functor.whiskerRight (t.truncLTι a✝) (shiftFunctor C 1)
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
  simp only [← NatTrans.comp_app, ← Functor.map_comp]
  rfl

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
  simp only [← NatTrans.comp_app, ← Functor.map_comp]
  rfl

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 c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ ⊥ ∉ I.biUnion fun i ↦ (P i).parts

Tactic:
mem_biUnion

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.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
⊢ (b ∈ P.parts.attach.biUnion fun i ↦ (Q ↑i ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts

Tactic:
mem_biUnion

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.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ P.part a ∈ P.parts ↔ a ∈ s
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mpr.ht
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a ∈ P.parts

pp: case mpr.hu
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ t ∈ P.parts

pp: case mpr.hat
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ P.part a

pp: case mpr.hau
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ t

Tactic:
<;>

Goal state after:
case mpr.ht
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a ∈ P.parts

case mpr.hu
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ t ∈ P.parts

case mpr.hat
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ P.part a

case mpr.hau
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mp.refine_1
α : 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

pp: case mp.refine_2
α : 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:
<;>

Goal state after:
case mp.refine_1
α : 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

case mp.refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
⊢ b ∈ P.part b
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#(interedges r s t))

pp: case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)

Tactic:
<;>

Goal state after:
case ha
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#(interedges r s t))

case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ ↑(#(interedges r ∅ t)) / 0 = 0

Tactic:
div_zero

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ 0 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#s) * ε ≤ ↑(#s) * ε'

pp: case refine_2
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#t) * ε ≤ ↑(#t) * ε'

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#s) * ε ≤ ↑(#s) * ε'

case refine_2
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ ↑(#t) * ε ≤ ↑(#t) * ε'
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
⊢ ↑(#(interedges r s ∅)) / 0 = 0

Tactic:
div_zero

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
⊢ 0 = 0