mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ fromRel sym = Set.univ ↔ r = ⊤

Tactic:
refine ⟨fun h ↦ ?_, (· ▸ fromRel_top)⟩
  ext x y
  simpa [h] using fromRel_prop (sym := sym)

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b : α
⊢ ∀ (b_1 c d : α) (h : Rel α (b, b_1) (c, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then b_1 else b) ⋯ = fun x ↦ if a = c then d else c

Tactic:
c

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c : α
⊢ ∀ (c_1 d : α) (h : Rel α (b, c) (c_1, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = c_1 then d else c_1
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
⊢ (↑⋯.equiv).toFun (x * y) = (↑⋯.equiv).toFun x * (↑⋯.equiv).toFun y

Tactic:
dsimp
    induction x with
    | zero => simp
    | add x y _ _ => simp [*, add_mul]
    | tmul a b =>
      induction y with
      | zero => simp
      | add x y _ _ => simp [*, mul_add]
      | tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp ↦ dite q (b hp) (c hp)) = if hq : q then dite p a fun hp ↦ b hp hq else dite p a fun hp ↦ c hp hq

Tactic:
by
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp ↦ dite q (a hp) (b hp)) c = if hq : q then dite p (fun hp ↦ a hp hq) c else dite p (fun hp ↦ b hp hq) c

Tactic:
by
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp (Quiver.reverse a✝).toPath.reverse = a✝¹.cons a✝

Tactic:
Path.reverse_toPath,

Goal state after:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp (Quiver.reverse (Quiver.reverse a✝)).toPath = a✝¹.cons a✝
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
⊢ ∀ {X Y : D}, Function.Surjective F.map

Tactic:
by
  intro X₁ X₂ ψ
  obtain ⟨f, hf⟩ := h (F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫
    F.map (L.objObjPreimageIso X₂).inv)
  exact ⟨(L.objObjPreimageIso X₁).inv ≫ f ≫ (L.objObjPreimageIso X₂).hom, by simp [hf]⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)

Tactic:
aesop_cat

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)

Tactic:
aesop_cat

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
clear this

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
clear this

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
clear this

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]
  exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
by
  rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]
  exact (F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
by
  rw [← Equiv.eq_symm_apply]; simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ (e X Y') (g ≫ h) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map h

Tactic:
simp [← he, reassoc_of% (he'' e)]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Tactic:
← triangle,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (α_ f (𝟙 b) g).hom ≫ f ◁ (λ_ g).hom = f ◁ (λ_ g).hom
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ ↑F.sections

Tactic:
refine ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ ?_⟩
    simp [-const_obj_obj, ← comp_apply, -types_comp_apply, ← NatTrans.naturality]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.map f)

Tactic:
apply isSplitEpi_of_epi

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F

Tactic:
apply hasLimit_of_iso (e.invFunIdAssoc F)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case init.id
J : Type w
j✝ : J
⊢ Hom none (some j✝)

Tactic:
apply Hom.init _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
j : J
⊢ lift f fs w ≫ π arrows j = fs j

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_π_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ lift f fs w ≫ base arrows = f

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_π_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  ∀ (j : Discrete β),
    m ≫
        { pt := f default,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.π.app
          j =
      s.π.app j
⊢ m = s.π.app default

Tactic:
specialize w default
        simpa using w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂

Tactic:
simpa using congr_arg (fun f => coprod.inl ≫ f) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryCoproduct A B
inst✝² : HasBinaryCoproduct A' B'
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'

Tactic:
by
  rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : L' ⟶ G✝.obj L
β✝ : R ⋙ G✝ ⟶ F✝ ⋙ R'
F : C ≌ A
G : D ≌ B
α : L' ⟶ G.functor.obj L
α' : L ⟶ G.inverse.obj L'
β : R ⋙ G.functor ⟶ F.functor ⋙ R'
β' : R' ⋙ G.inverse ⟶ F.inverse ⋙ R
hαα' : α ≫ G.functor.map α' = G.counitIso.inv.app L'
hα'α : α' ≫ G.inverse.map α = G.unitIso.hom.app L
hββ' :
  R.rightUnitor.hom ≫ R.leftUnitor.inv ≫ Functor.whiskerRight F.unitIso.hom R ≫ (F.functor.associator F.inverse R).hom =
    R.whiskerLeft G.unitIso.hom ≫
      (R.associator G.functor G.inverse).inv ≫
        Functor.whiskerRight β G.inverse ≫ (F.functor.associator R' G.inverse).hom ≫ F.functor.whiskerLeft β'
hβ'β :
  Functor.whiskerRight β' G.functor ≫
      (F.inverse.associator R G.functor).hom ≫
        F.inverse.whiskerLeft β ≫ (F.inverse.associator F.functor R').inv ≫ Functor.whiskerRight F.counitIso.hom R' =
    (R'.associator G.inverse G.functor).hom ≫ R'.whiskerLeft G.counitIso.hom ≫ R'.rightUnitor.hom ≫ R'.leftUnitor.inv
X : C
⊢ ((R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ Functor.whiskerRight F.unitIso.hom R).app X =
    (R.whiskerLeft G.unitIso.hom ≫
          (R.associator G.functor G.inverse).inv ≫
            Functor.whiskerRight β G.inverse ≫
              (F.functor.associator R' G.inverse).hom ≫
                F.functor.whiskerLeft β' ≫ (F.functor.associator F.inverse R).inv).app
      X

Tactic:
simpa using congr($(hββ').app X)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : T ⥤ D
G : D ⥤ E
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ (post (F ⋙ G)).map f ≫ (Iso.refl ((post (F ⋙ G)).obj Y✝)).hom =
    (Iso.refl ((post (F ⋙ G)).obj X✝)).hom ≫ (post F ⋙ post G).map f

Tactic:
ext
    dsimp only [Iso.refl_hom, Under.comp_right, Under.id_right]
    simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
D : Type u'
F : D → C
X Y : InducedCategory C F
⊢ ∀ (x y : X ⟶ Y),
    InducedCategory.homEquiv.toFun (x + y) = InducedCategory.homEquiv.toFun x + InducedCategory.homEquiv.toFun y

Tactic:
aesop_cat

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ (↑a • e.hom) ≫ (↑a⁻¹ • e.inv) = 𝟙 X

Tactic:
by
        simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ⨆ a, (P a).isoClosure ≤ (⨆ a, P a).isoClosure

Tactic:
simp only [iSup_le_iff]
    intro a
    rw [isoClosure_le_iff]
    exact (le_iSup P a).trans (le_isoClosure _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : PreservesFiniteColimits X✝
⊢ PreservesFiniteColimits Y✝

Tactic:
exact preservesFiniteColimits_of_natIso e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBiproducts F
J : Type
x✝ : Finite J
⊢ PreservesBiproductsOfShape J F

Tactic:
let := preservesBiproducts_shrink.{0} F

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBiproducts F
J : Type
x✝ : Finite J
this : PreservesBiproducts F := preservesBiproducts_shrink F
⊢ PreservesBiproductsOfShape J F
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁸ : Category.{uC', uC} C✝
inst✝⁷ : HasZeroMorphisms C✝
D : Type uD
inst✝⁶ : Category.{uD', uD} D
inst✝⁵ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono (map p)

Tactic:
show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫
    (biproduct.isoProduct _).inv by aesop

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁸ : Category.{uC', uC} C✝
inst✝⁷ : HasZeroMorphisms C✝
D : Type uD
inst✝⁶ : Category.{uD', uD} D
inst✝⁵ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono ((isoProduct f).hom ≫ Pi.map p ≫ (isoProduct g).inv)
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
simp only [← NatIso.naturality_1 e (f + g), map_add, Preadditive.add_comp,
    NatTrans.naturality, Preadditive.comp_add, Iso.inv_hom_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ biproduct.fromSubtype f p ≫ biproduct.toSubtype f pᶜ = 0

Tactic:
classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
a b : Fin (n + 1)
hab : a < b
⊢ q.insertNth x f a < q.insertNth x f b

Tactic:
cases a using succAboveCases q <;> cases b using succAboveCases q

Goal state after:
case refine_4.x.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
hab : q < q
⊢ q.insertNth x f q < q.insertNth x f q

case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q < q.succAbove j✝
⊢ q.insertNth x f q < q.insertNth x f (q.succAbove j✝)

case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q.succAbove j✝ < q
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f q

case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_3
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ (Finsupp.erase a f).support ⊆ s

Tactic:
rwa [support_erase, ← subset_insert_iff]

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.sizeUpTo 0 = 0

Tactic:
simp [sizeUpTo]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ Function.update (⇑g) a n1 x = g x

Tactic:
update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g

Goal state after:
case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ g x = g x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ Int.negSucc n) x = x

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
ns : List ℕ
⊢ l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns

Tactic:
simp [splitWrtCompositionAux]

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

Goal state before:
pp: case nil
α : Type u_1
⊢ ∀ {l : List α}, [].sum ≤ l.length → map length (l.splitWrtCompositionAux []) = []

Tactic:
simp [splitWrtCompositionAux]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ # [].prod.support = (List.map (card ∘ support) []).sum

Tactic:
exact card_support_eq_zero.mpr rfl

Goal state after: