mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ (ObjectProperty.ofObj ι).isoClosure J
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      (∑ j_1,
          (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
            if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
        0

pp: case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0

pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
· intro b _ hb
              apply Finset.sum_eq_zero
              intro x _
              rw [dif_neg hb.symm, zero_comp]

Goal state after:
case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0

C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) x' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) x'
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) x') ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) y') ↔
    (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'

Tactic:
have hy := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) x' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) x'
hy :
  (ConcreteCategory.hom (c.ι.app j ≫ hc.desc ((forget PartOrdEmb).mapCocone s))) y' =
    (ConcreteCategory.hom (((forget PartOrdEmb).mapCocone s).ι.app j)) y'
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) x') ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ }
        ((ConcreteCategory.hom (c.ι.app j)) y') ↔
    (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
x : X
⊢ (ConcreteCategory.hom (p.ι.app j')) (y' x) = (ConcreteCategory.hom (p.ι.app (j x))) (y x)

Tactic:
← p.w (IsCardinalFiltered.toMax j hX x)

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
x : X
⊢ (ConcreteCategory.hom (p.ι.app j')) (y' x) =
    (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x) ≫ p.ι.app (IsCardinalFiltered.max j hX))) (y x)
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
j : κ.ord.ToType
⊢ ¬IsMax j

Tactic:
by
      have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
      exact not_isMax j

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) (Order.succ j) A)) κ₂

Tactic:
have hκ₂ : κ₂.IsRegular := Fact.out
    rw [transfiniteIterate_succ _ _ _ hj, φ_eq _ _ _ hj']
    refine hasCardinalLT_iUnion _ (hY _ _)
      (fun ⟨C, hC⟩ ↦ hasCardinalLT_union hκ₂.aleph0_le ?_
        (hasCardinalLT_of_finite _ _ hκ₂.aleph0_le))
    refine (C.prop.of_le h₀.le).of_injective (fun ⟨c, hc⟩ ↦ ?_)
      (fun c₁ c₂ hc ↦ ?_)
    · simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at hc
      exact ⟨⟨c, hc.choose⟩, hc.choose_spec⟩
    · simpa only [Subtype.ext_iff] using hc

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
⊢ ∀ {i j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔ MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst) f → (D₁ D hι m).P i

Tactic:
simp only [D₁_W, D₁_P]

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
⊢ ∀ {i j : J} {f : i ⟶ j},
    (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
          MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
        f →
      (∃ a, (D a).P i) ∨ m = i
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
⊢ ∀ {i j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔ MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst) f → (D₁ D hι m).P j

Tactic:
simp only [D₁_W, D₁_P]

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
⊢ ∀ {i j : J} {f : i ⟶ j},
    (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
          MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
        f →
      (∃ a, (D a).P j) ∨ m = j
Module: Mathlib.CategoryTheory.Profunctor.Basic

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X : C
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ P.map (𝟙 X ≫ 𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g

Tactic:
simp only [P.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Profunctor.Basic

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
⊢ P.map (f ≫ f') (𝟙 Y ≫ 𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)

Tactic:
simp only [P.map_comp]

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
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    IsIso ((uliftYonedaEquiv.symm { down := x }).app (op Y))

Tactic:
isIso_iff_bijective,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective ⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y)))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.top
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), ⊤.arrows (π a)

Tactic:
refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
      have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
      exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι'
⊢ (F.map (p' i).op.toLoc).toFunctor.map (full_pullFunctor.hom w hf' φ (α i)) = φ.hom i

Tactic:
map_hom _ _ _ _ (𝟙 _) (by cat_disch),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι'
⊢ mor w φ (p' i) (𝟙 (X' i)) ⋯ = φ.hom i
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) ((β * α) i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) ((β * α) j)

Tactic:
by
  dsimp
  rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
    h₂₃ i j a b, mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW

Goal state before:
pp: C : Type u
inst✝¹⁴ : Category.{v, u} C
inst✝¹³ : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹² : Category.{v', u'} A
inst✝¹¹ : MonoidalCategory A
inst✝¹⁰ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁹ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁸ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁷ : ConcreteCategory A FC
inst✝⁶ : HasWeakSheafify J A
inst✝⁵ : (forget A).ReflectsIsomorphisms
inst✝⁴ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝³ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : J.HasEnoughPoints
⊢ J.W.IsMonoidal

Tactic:
obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J
  exact hP.isMonoidal_W A

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
R : Sieve U.left
hR : R ∈ J U.left
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu : (ConcreteCategory.hom (Φ.fiber.map f)) v ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
⊢ v ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj (Over.mk (f ≫ U.hom))

Tactic:
FunctorToTypes.mem_fromOverSubfunctor_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
R : Sieve U.left
hR : R ∈ J U.left
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu : (ConcreteCategory.hom (Φ.fiber.map U.hom)) ((ConcreteCategory.hom (Φ.fiber.map f)) v) = x
⊢ (ConcreteCategory.hom (Φ.fiber.map (Over.mk (f ≫ U.hom)).hom)) v = x
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ y ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      (Over.mk f)

Tactic:
FunctorToTypes.mem_fromOverSubfunctor_iff

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
⊢ K.Generates J ↔ K.toGrothendieck = J

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← Coverage.toGrothendieck_toPrecoverage]
    exact h.toGrothendieck_eq
  · rintro rfl
    exact Coverage.generates_toGrothendieck _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (J.overMapPullbackComp A f.unop (𝟙 b₀✝).unop).symm).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₀✝))).hom
            (J.overMapPullback A f.unop).toCatHom ≫
          (Bicategory.leftUnitor (J.overMapPullback A f.unop).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
simpa [overMapPullbackCongr_eq_eqToIso] using!
      J.overMapPullback_comp_id A f.unop

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
⊢ P.triangEnvelope.IsTriangulatedClosed₂

Tactic:
by
  apply IsTriangulatedClosed₂.mk'
  intro T hT h₁ h₂
  rw [prop_triangEnvelope_iff] at h₁ h₂ ⊢
  obtain ⟨n, hn⟩ := h₁
  obtain ⟨m, hm⟩ := h₂
  use n + (m + 1)
  rw [triangEnvelopeIter_add' P rfl]
  exact le_retractClosure _ _ ⟨_, _, _, _, _, hT, hn, hm⟩

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ IsColimit (CokernelCofork.ofπ f₂ ⋯)

Tactic:
by
  have hT' : Triangle.mk (0 : ((ι ⋙ shiftFunctor C (1 : ℤ)).obj 0) ⟶ _) (𝟙 (ι.obj X₃)) 0 ∈
      distTriang C := by
    refine isomorphic_distinguished _ (inv_rot_of_distTriang _
      (contractible_distinguished (ι.obj X₃))) _ ?_
    refine Triangle.isoMk _ _ (IsZero.iso ?_ ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
    · dsimp
      rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
    · dsimp
      rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]
    all_goals simp
  refine IsColimit.ofIsoColimit (AbelianSubcategory.isColimitCokernelCofork hι hT hT') ?_
  exact Cofork.ext (Iso.refl _) (ι.map_injective (by simp))

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ↑(∑ x ∈ s, #(bipartiteAbove r t x)) = ↑(∑ x ∈ t, #(bipartiteBelow r s x))

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

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

Goal state before:
pp: α : 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 : MapsTo f A B
⊢ (map g (map f s)).prod = (map g (map f t)).prod

Tactic:
apply hg.map_prod_eq_map_prod <;> simp_all [MapsTo]

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

Goal state before:
pp: n d k : ℕ
⊢ ThreeAPFree (⇑(map (2 * d - 1)) '' ↑(sphere n d k))

Tactic:
apply ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1))
    (map_injOn.mono _) threeAPFree_sphere

Goal state after:
n d k : ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 2 < rexp 1

Tactic:
exact exp_one_gt_d9.trans' (by norm_num)

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

Goal state before:
pp: ⊢ 0 < rexp 1

Tactic:
exact exp_one_gt_d9.trans' (by norm_num)

Goal state after: