mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ▷ A ≫ (α_ A A A).hom ≫ A ◁ 𝒮 ▷ A ≫ (α_ A A A).inv ≫ μ ▷ A)

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ

Tactic:
← associator_naturality_middle_assoc,

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (α_ A A A).hom ≫ (α_ A A A).inv ≫ μ ▷ A)

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| limit.π F j ▷ limit G ▷ limit H ≫
    (α_ (F.obj j) (limit G) (limit H)).hom ≫ F.obj j ◁ limit.π G j ▷ limit H ≫ F.obj j ◁ G.obj j ◁ limit.π H j

Tactic:
← associator_naturality_middle_assoc,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| limit.π F j ▷ limit G ▷ limit H ≫
    (F.obj j ◁ limit.π G j) ▷ limit H ≫ (α_ (F.obj j) (G.obj j) (limit H)).hom ≫ F.obj j ◁ G.obj j ◁ limit.π H j
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ (regular S).X ≫ P.actRight = ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫ P.actRight

Tactic:
dsimp; rw [Category.assoc, right_assoc, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv

Tactic:
iterate 5 rw [← IsIso.comp_inv_eq]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ ((((((α_ X Y X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv) ≫ inv (Y ◁ (β_ X X).inv)) ≫ inv (α_ Y X X).hom) ≫
        inv ((β_ Y X).inv ▷ X)) ≫
      inv (α_ X Y X).inv =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : MonoidalCategory V
F G : C ⥤ V
inst✝¹⁴ : DayConvolution F G
inst✝¹³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝¹² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹¹ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
H K : C ⥤ V
inst✝¹⁰ : DayConvolution G H
inst✝⁹ : DayConvolution (F ⊛ G) H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution H K
inst✝⁶ : DayConvolution G (H ⊛ K)
inst✝⁵ : DayConvolution (G ⊛ H) K
inst✝⁴ : DayConvolution ((F ⊛ G) ⊛ H) K
inst✝³ : DayConvolution (F ⊛ G) (H ⊛ K)
inst✝² : DayConvolution (F ⊛ G ⊛ H) K
inst✝¹ : DayConvolution F (G ⊛ H ⊛ K)
inst✝ : DayConvolution F ((G ⊛ H) ⊛ K)
this :
  (((F ⊛ G) ⊠ H) ⊠ K).IsLeftKanExtension (extensionUnitLeft ((F ⊛ G) ⊠ H) (extensionUnitLeft (F ⊛ G) (unit F G) H) K)
l k i j : C
aux :
  ((unit F G).app (i, j) ⊗ₘ (unit H K).app (k, l)) ≫ (unit (F ⊛ G) (H ⊛ K)).app (i ⊗ j, k ⊗ l) =
    (α_ (F.obj i) (G.obj j) (H.obj k ⊗ K.obj l)).hom ≫
      F.obj i ◁ G.obj j ◁ (unit H K).app (k, l) ≫
        F.obj i ◁ (unit G (H ⊛ K)).app (j, k ⊗ l) ≫
          (unit F (G ⊛ H ⊛ K)).app (i, j ⊗ k ⊗ l) ≫
            (F ⊛ G ⊛ H ⊛ K).map (α_ i j (k ⊗ l)).inv ≫ (associator F G (H ⊛ K)).inv.app ((i ⊗ j) ⊗ k ⊗ l)
⊢ (α_ (F.obj i) (G.obj j) (H.obj k)).hom ▷ K.obj l ≫
      (α_ (F.obj i) (G.obj j ⊗ H.obj k) (K.obj l)).hom ≫
        F.obj i ◁
            ((α_ (G.obj j) (H.obj k) (K.obj l)).hom ≫
              G.obj j ◁ (unit H K).app (k, l) ≫ (unit G (H ⊛ K)).app (j, k ⊗ l) ≫ (G ⊛ H ⊛ K).map (α_ j k l).inv) ≫
          (unit F (G ⊛ H ⊛ K)).app (i, (j ⊗ k) ⊗ l) ≫
            (F ⊛ G ⊛ H ⊛ K).map (α_ i (j ⊗ k) l).inv ≫ (F ⊛ G ⊛ H ⊛ K).map ((α_ i j k).inv ▷ l) =
    (α_ (F.obj i ⊗ G.obj j) (H.obj k) (K.obj l)).hom ≫
      (α_ (F.obj i) (G.obj j) (H.obj k ⊗ K.obj l)).hom ≫
        F.obj i ◁ (G.obj j ◁ (unit H K).app (k, l) ≫ (unit G (H ⊛ K)).app (j, k ⊗ l)) ≫
          (unit F (G ⊛ H ⊛ K)).app (i, j ⊗ k ⊗ l) ≫
            (F ⊛ G ⊛ H ⊛ K).map (α_ i j (k ⊗ l)).inv ≫ (F ⊛ G ⊛ H ⊛ K).map (α_ (i ⊗ j) k l).inv

Tactic:
simp [← Functor.map_comp, pentagon_inv, pentagon_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f + β.f) ≫ G.a = F.a ≫ (α.f + β.f)

Tactic:
by simp only [Functor.map_add, add_comp, Monad.Algebra.Hom.h, comp_add]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
⊢ n • α.f ≫ G.a = (n • α.f) ≫ G.a

Tactic:
nsmul_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
⊢ n • α.f ≫ G.a = n • α.f ≫ G.a
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ n • α.f ≫ A₂.str = (n • α.f) ≫ A₂.str

Tactic:
nsmul_comp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ n • α.f ≫ A₂.str = n • α.f ≫ A₂.str
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:

Tactic:
m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
      { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }
    _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ (coherentTopology C) X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
constructor
  · intro h
    induction h with
    | of Y T hS =>
      obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
    | top Y =>
      exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
    | transitive Y R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩
  · exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
⊢ (ConcreteCategory.hom (f.app (op (∐ Z)))) ((ConcreteCategory.hom i'.hom) x) =
    (ConcreteCategory.hom (G.map (Sigma.desc π).op)) y

Tactic:
apply Concrete.isLimit_ext _ (isLimitOfPreserves G (coproductIsCoproduct Z).op)

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := ⋯
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
⊢ ∀ (j : (Discrete α)ᵒᵖ),
    (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j))
        ((ConcreteCategory.hom (f.app (op (∐ Z)))) ((ConcreteCategory.hom i'.hom) x)) =
      (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app j))
        ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
x : Unit → F.obj (op Y)
hx : Arrows.Compatible F (fun x ↦ f) x
y : (fun X ↦ X) (F.obj (op X))
h : (fun t ↦ ∀ (i : Unit), (ConcreteCategory.hom (F.map f.op)) t = x i) y
⊢ y = (ConcreteCategory.hom (F.map (Projective.factorThru (𝟙 X) f).op)) (x ())

Tactic:
· simp [← h (), ← comp_apply, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)

Tactic:
simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), m] using .of_hasPullback _ _

Goal state after:
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 * α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (β j * α j)

Tactic:
map_mul,

Goal state after:
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) * (ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (β j * α j)
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) * (ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (β j * α j)

Tactic:
map_mul,

Goal state after:
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) * (ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (β j) * (ConcreteCategory.hom (G.map b.op)) (α j))
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ x i ∈ G.obj (X i)

Tactic:
← ofSection_le_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : D
f : X ⟶ Y
⊢ (associator C D E).map ((inl_ (C ⊕ D) E).map ((inr_ C D).map f)) = (inr_ C (D ⊕ E)).map ((inl_ D E).map f)

Tactic:
simp [associator]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : D
f : X ⟶ Y
⊢ (associator C D E).map ((inl_ (C ⊕ D) E).map ((inr_ C D).map f)) = (inr_ C (D ⊕ E)).map ((inl_ D E).map f)

Tactic:
by
  simp [associator]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : E
f : X ⟶ Y
⊢ (associator C D E).map ((inr_ (C ⊕ D) E).map f) = (inr_ C (D ⊕ E)).map ((inr_ D E).map f)

Tactic:
simp [associator]

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : E
f : X ⟶ Y
⊢ (associator C D E).map ((inr_ (C ⊕ D) E).map f) = (inr_ C (D ⊕ E)).map ((inr_ D E).map f)

Tactic:
by
  simp [associator]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
this : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
exact h.uniq this

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ IsPullback (m.app X) (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X) ((χ m).app X)
    ((truth C).app X)

Tactic:
Types.isPullback_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ m.app X ≫ (χ m).app X = ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X ≫ (truth C).app X ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
        (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
            (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
              (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
        (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
              (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ (opOp C).mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
by
    refine isomorphic_distinguished _ (op_distinguished _ (op_distinguished _ hT)) _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
      (Quiver.Hom.unop_inj ?_))
    have := (shiftFunctorCompIsoId C (-1) 1 (neg_add_cancel 1)).inv.naturality T.mor₃
    dsimp at this ⊢
    simp only [shiftFunctor_op_map _ 1 (-1), Functor.op_obj,
      unop_id, shiftFunctor_op_map _ (-1) 1,
      commShiftIso_opOp_hom_app _ 1 (-1),
      opShiftFunctorEquivalence_counitIso_inv_app _ 1 (-1) (add_neg_cancel 1),
      unop_comp, Quiver.Hom.unop_op, Category.assoc, ← op_comp, Iso.inv_hom_id_app_assoc,
      shiftFunctorCompIsoId_op_hom_app, Iso.unop_hom_inv_id_app_assoc, ← Functor.map_comp]
    simp [Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app, ← reassoc_of% this]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
⊢ ThreeGPFree s ↔ ThreeGPFree t

Tactic:
rw [← threeGPFree_image hf subset_rfl, hf.bijOn.image_eq]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
⊢ ThreeGPFree (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ habc

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a = f b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f (a * c) = f (b * b)

Tactic:
map_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a * f c = f (b * b)
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: case e'_2.a
α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
B : α → Finset β
s : Finset α
x✝ : α
a✝ : x✝ ∈ s
⊢ B x✝ = bipartiteAbove (fun j x ↦ x ∈ B j) (s.biUnion B) x✝

pp: case e'_3.a
α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
B : α → Finset β
s : Finset α
x✝ : β
a✝ : x✝ ∈ s.biUnion B
⊢ {j | j ∈ s ∧ x✝ ∈ B j} = bipartiteBelow (fun j x ↦ x ∈ B j) s x✝

Tactic:
· grind [bipartiteAbove]

Goal state after:
case e'_3.a
α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
B : α → Finset β
s : Finset α
x✝ : β
a✝ : x✝ ∈ s.biUnion B
⊢ {j | j ∈ s ∧ x✝ ∈ B j} = bipartiteBelow (fun j x ↦ x ∈ B j) s x✝
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

Tactic:
mem_range,

Goal state after:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 < n * (d - 1) ^ 2 + 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
⊢ 2 ^ ↑6 ≤ ↑N

Tactic:
rw [rpow_natCast]

Goal state after:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N

Tactic:
by
  have : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N :=
    Nat.pow_le_pow_left (Nat.sub_le _ _) _
  apply this.trans
  suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N from mod_cast this
  suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (nValue N : ℝ)⁻¹ by
    rw [← rpow_natCast]
    apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
    rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
    rw [cast_ne_zero]
    apply (nValue_pos hN).ne'
  rw [← le_div_iff₀']
  · exact floor_le (by positivity)
  apply zero_lt_two

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 64 = 2 ^ ↑6

Tactic:
rw [rpow_natCast]

Goal state after:
⊢ 64 = 2 ^ 6
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ d ∉ {d.symm}

Tactic:
mem_singleton

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm