mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1

case neg
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (if h : j = i then eqToHom ⋯ else 0) = (if h : j = i then eqToHom ⋯ else 0) PUnit.unit PUnit.unit

Tactic:
split_ifs with h

Goal state after:
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : j = i
⊢ eqToHom ⋯ = eqToHom ⋯ PUnit.unit PUnit.unit

case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : ¬j = i
⊢ 0 = 0 PUnit.unit PUnit.unit
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι D₁.obj₁ d ≫ D₁.l W Z ≫ toStep W Z = Sigma.ι D₁.obj₁ d ≫ D₁.t W Z ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)

Tactic:
pushout.condition

Goal state after:
case refine_2.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι D₁.obj₁ d ≫ D₁.l W Z ≫ toStep W Z = Sigma.ι D₁.obj₁ d ≫ D₁.l W Z ≫ pushout.inr (D₁.t W Z) (D₁.l W Z)
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
⊢ HasCardinalLT κ₁.ord.ToType κ₂

Tactic:
by simpa [hasCardinalLT_iff_cardinal_mk_lt]

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy ((ConcreteCategory.hom (F.map e.hom.op)) x) ↔ F.IsRepresentedBy x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.of_isoObj e⟩
  have : x = F.map e.inv.op (F.map e.hom.op x) := by
    simp [← comp_apply, ← map_comp, ← op_comp]
  exact this ▸ .of_isoObj h e.symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
hR : Presheaf.IsSheaf J R
⊢ Function.Bijective (⇑((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) ∘ fun g ↦ whiskerRight f G ≫ g)

Tactic:
convert!
      (((adj.whiskerRight Cᵒᵖ).homEquiv Q R).trans
          (hf.homEquiv (R ⋙ F) ((sheafCompose J F).obj ⟨R, hR⟩).property)).bijective

Goal state after:
case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
hR : Presheaf.IsSheaf J R
e_1✝ : (Q ⋙ G ⟶ R) = (((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R)
e_2✝ : (P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R) = (P ⟶ R ⋙ F)
⊢ (⇑((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) ∘ fun g ↦ whiskerRight f G ≫ g) =
    ⇑(((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv Q R).trans (ObjectProperty.isLocal.homEquiv hf (R ⋙ F) ⋯))
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
j : J
hj : D.P j
l₁ l₂ : j ⟶ m₁
hl₁ : (D₄ D φ).W l₁
hl₂ : (D₄ D φ).W l₂
⊢ l₁ = l₂

Tactic:
obtain rfl := h₂ hj hl₁
          obtain rfl := h₂ hj hl₂
          rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂

Tactic:
have := φ.comm (q ≫ f i) a₁ a₂ fac₁ fac₂
  dsimp at this
  rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    pullFunctorObjHom_eq _ _ _ _ _ (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) rfl,
    map_eq_pullHom _ _ _ _ (by exact rfl) rfl, map_eq_pullHom _ _ _ _ rfl rfl] at this
  dsimp at this
  simp only [Category.assoc, Cat.Hom.hom_inv_id_toNatTrans_app_assoc, cancel_epi] at this
  simp only [← Category.assoc, cancel_mono] at this
  rw [← cancel_mono (D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q), Category.assoc,
    D₂.hom_comp] at this
  rw [mor_eq _ _ _ _ _ _ _ rfl rfl, mor_eq _ _ _ _ _ _ _ rfl rfl, this]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ (x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)

Tactic:
H,

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ F.map (Over.Hom.left φ.unop).op ▷ M ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)) =
    uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
        (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))

Tactic:
← uncurry_pre_app,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)) ≫
        (pre (F.map (Over.Hom.left φ.unop).op)).app (G.obj (op (unop j').left))) =
    uncurry
      ((f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
        (ihom (F.obj (op (unop j).left))).map (G.map (Over.Hom.left φ.unop).op))
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)

Tactic:
isRegularEpi_iff_effectiveEpi

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ EffectiveEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
g : (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N
i₁ i₂ : ι
Z : Over S
f₁ : Z ⟶ (fun i ↦ Over.mk (f i)) i₁
f₂ : Z ⟶ (fun i ↦ Over.mk (f i)) i₂
h : f₁ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₁ = f₂ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₂
⊢ (ConcreteCategory.hom ((F.presheafHom M N).map f₁.op)) (g.hom i₁) =
    (ConcreteCategory.hom ((F.presheafHom M N).map f₂.op)) (g.hom i₂)

Tactic:
by
        simpa [map_eq_pullHom (g.hom i₁) f₁.left Z.hom Z.hom (Over.w f₁) (Over.w f₁),
          map_eq_pullHom (g.hom i₂) f₂.left Z.hom Z.hom (Over.w f₂) (Over.w f₂),
          cancel_epi, cancel_mono] using g.comm Z.hom f₁.left f₂.left (Over.w f₁) (Over.w f₂)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData fun f ↦ f.obj.hom).map ↔
    Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
rw [bijective_toDescentData_map_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
⊢ Presieve.IsSheafFor (F.presheafHom M N)
      (Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯) ↔
    Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

Tactic:
isPrestackFor_iff_isSheafFor

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ (∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows) ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsPrestackFor (Sieve.generate (Presieve.ofArrows X f)).arrows

Tactic:
isPrestackFor_iff_isSheafFor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ ∀ (M N : ↑(F.obj { as := op S })),
    Presieve.IsSheafFor (F.presheafHom M N)
      ((Sieve.overEquiv (Over.mk (𝟙 S))).symm (Sieve.generate (Presieve.ofArrows X f))).arrows
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ F.op.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

Tactic:
rw [mem_distTriang_op_iff]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.IsTriangulated
T : Triangle Cᵒᵖ
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ unop ((triangleOpEquivalence D).inverse.obj (F.op.mapTriangle.obj T)) ∈ Pretriangulated.distinguishedTriangles
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : a * c = b * b
⊢ b = c

Tactic:
obtain rfl := hs ha hb hc habc

Goal state after:
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
c : α
hc : c ∈ s
hb : a ∈ s
habc : a * c = a * a
⊢ a = c
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
simp_rw [mem_bipartiteBelow]

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case g2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x

Tactic:
case g2 => exact h.1 (htA hx)

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanHom n B C g
hf : IsMulFreimanHom n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (g ∘ f) s).prod = (map (g ∘ f) t).prod

Tactic:
by
    rw [← map_map, ← map_map]
    refine hg.map_prod_eq_map_prod ?_ ?_ (by rwa [card_map]) (by rwa [card_map])
      (hf.map_prod_eq_map_prod hsA htA hs ht h)
    · simpa using fun a h ↦ hf.mapsTo (hsA h)
    · simpa using fun a h ↦ hf.mapsTo (htA h)

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ ↑12 * log 2 < 16

Tactic:
cast_ofNat

Goal state after:
⊢ 12 * log 2 < 16
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B) = A.convolution B⁻¹ x

Tactic:
by
  simpa using card_smul_inter_smul _ _ 1 x

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
have hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)} := by
    rw [hg]
    apply Nat.succ_pos

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #{w | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)}
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)
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:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
⊢ P ≤ (Finpartition.empty α).copy ⋯

case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h
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:
ne_eq

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
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)
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃
      Fin (#P.parts - #s % #P.parts) := (Equiv.Set.sep ..).symm.trans (sneg.trans es)

Goal state after:
α : 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, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mp
α : 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:
rintro ⟨⟨A, hA⟩, -, h⟩
    exact ⟨A, hA, h⟩

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥↑t
e : α
⊢ e ∈ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) x)).fst ↔ e ∈ ↑x.fst

Tactic:
obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
      dsimp only at mf ⊢
      rw [P.part_eq_of_mem mp mf]

Goal state after: