mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ Nat.find ⋯ = p.count a.factors

Tactic:
by
  apply le_antisymm
  · refine Nat.find_le ⟨1, ?_⟩
    rw [mul_one]
    symm
    exact eq_pow_count_factors_of_dvd_pow hp h
  · have hph := pow_ne_zero (@Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩) hp.ne_zero
    rcases subsingleton_or_nontrivial α with hα | hα
    · simp [eq_iff_true_of_subsingleton] at hph
    convert! count_le_count_of_le hph hp (@Nat.find_spec (fun n => a ∣ p ^ n) _ ⟨n, h⟩)
    rw [count_pow hp.ne_zero hp, count_self hp, mul_one]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ Transcendental R x ↔ RingHom.ker (aeval x) = ⊥

Tactic:
by
  rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ⊗ₜ[R] b ∈ ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ nilpotencyClass x = 0

Tactic:
by change sInf _ = 0; simp [s] at this; simp [this]

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intros

Goal state after:
case mp
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
i✝ : ι
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intros

Goal state after:
case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + t.dens = (s ∪ t).dens

Tactic:
rw [← dens_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
simp_rw [cons_eq_insert]
  rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b a : α
s : Finset α
ha : a ∉ s
⊢ Disjoint (map (Sym2.mkEmbedding a) (cons a s ha)) s.sym2

Tactic:
by
      simp [Finset.disjoint_left, ha]

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

Goal state before:
pp: case nil
α : Type u_1
xs : List α
⊢ List.sym 1 [] = map (fun x ↦ x ::ₛ Sym.nil) []

Tactic:
simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ ∀ a ∈ s.erase i, f a ≠ 0

Tactic:
intros

Goal state after:
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
a✝¹ : ι
a✝ : a✝¹ ∈ s.erase i
⊢ f a✝¹ ≠ 0
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ ⦃a b : α × α⦄, Rel α a b → (Vector.Perm.isSetoid α 2) ⟨[a.1, a.2], ⋯⟩ ⟨[b.1, b.2], ⋯⟩

Tactic:
rintro _ _ ⟨_⟩

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ (Vector.Perm.isSetoid α 2) ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩ ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩

case swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ (Vector.Perm.isSetoid α 2) ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩ ⟨[(y✝, x✝).1, (y✝, x✝).2], ⋯⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ (Vector.Perm.isSetoid α 2) ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩ ⟨[(y✝, x✝).1, (y✝, x✝).2], ⋯⟩

Tactic:
apply List.Perm.swap'

Goal state after:
case swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [].Perm []
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e
  simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
revert F₁ F₂
  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
    fun F₁ F₂ e => ⟨this e, this e.symm⟩
  intro F₁ F₂ e hf
  exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ α.symm.inv.app X✝ ≫ F'.map a₂✝ ≫ α.symm.hom.app Y✝ = F.map a₂✝

Tactic:
NatIso.naturality_1 α.symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₂✝ = F.map a₂✝
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : D
Y Z : C
hZ : P Z
e : Y ≅ Z
e' : F.obj Y ≅ X
⊢ P.map F X

Tactic:
exact ⟨Z, hZ, ⟨F.mapIso e.symm ≪≫ e'⟩⟩

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

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }

Tactic:
by
  rw [iff_iff_eq, discreteEquiv.forall_congr_left]
  simp only [discreteEquiv, Equiv.symm_mk, Equiv.coe_fn_mk]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map F

Tactic:
intro X Y f _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ ⊤.map F f
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x : X
⊢ ∀ ⦃a₂ : X⦄, f x = f a₂ → x = a₂

Tactic:
x'

Goal state after:
case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
⊢ f x = f x' → x = x'
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G : AddCommGrpCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k

Tactic:
by
  simpa using CategoryTheory.congr_fun w 1

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 Y : C⦄ (f : X ⟶ Y),
    (𝟭 C).map f ≫ (adj.homEquiv Y (F.obj Y)) (𝟙 (F.obj Y)) = (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X)) ≫ (F ⋙ G).map f

Tactic:
intros

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
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 C).map f✝ ≫ (adj.homEquiv Y✝ (F.obj Y✝)) (𝟙 (F.obj Y✝)) =
    (adj.homEquiv X✝ (F.obj X✝)) (𝟙 (F.obj X✝)) ≫ (F ⋙ G).map f✝
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 Y : D⦄ (f : X ⟶ Y),
    (G ⋙ F).map f ≫ (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y)) =
      (adj.homEquiv (G.obj X) ((𝟭 D).obj X)).invFun (𝟙 (G.obj X)) ≫ (𝟭 D).map f

Tactic:
intros

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
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ (G ⋙ F).map f✝ ≫ (adj.homEquiv (G.obj Y✝) ((𝟭 D).obj Y✝)).invFun (𝟙 (G.obj Y✝)) =
    (adj.homEquiv (G.obj X✝) ((𝟭 D).obj X✝)).invFun (𝟙 (G.obj X✝)) ≫ (𝟭 D).map f✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (e.homEquiv.trans (e'.app (op X)).toEquiv) (f ≫ g) =
    (ConcreteCategory.hom (F'.map f.op)) ((e.homEquiv.trans (e'.app (op X')).toEquiv) g)

Tactic:
dsimp
    rw [e.homEquiv_comp]
    apply e'.hom.naturality_apply

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (e.homEquiv.trans (e'.app Y').toEquiv) (f ≫ g) =
    (ConcreteCategory.hom (F'.map g)) ((e.homEquiv.trans (e'.app Y).toEquiv) f)

Tactic:
dsimp
    rw [e.homEquiv_comp]
    apply e'.hom.naturality_apply

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)

Tactic:
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: ⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
intros

Goal state after:
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
T : C
⊢ IsIso (↾fun x ↦ f ≫ x)

Tactic:
exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk)) = F

Tactic:
ext
    refine Functor.ext (by cat_disch) ?_
    intro x y f
    apply ULift.ext
    cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ (inv i ≫ f) ≫ p = g

Tactic:
simp only [sq.w, assoc, IsIso.inv_hom_id_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p

Tactic:
by
  constructor <;> intro
  exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongEpi f
inst✝ : StrongEpi g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Mono z], HasLiftingProperty (f ≫ g) z

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝² : StrongEpi f
inst✝¹ : StrongEpi g
X✝ Y✝ : C
z✝ : X✝ ⟶ Y✝
inst✝ : Mono z✝
⊢ HasLiftingProperty (f ≫ g) z✝
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f

Tactic:
rw [hI.hom_ext f (hI.to X)]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsTerminal X
⊢ ∀ (X_1 : C ⥤ D) (m : X_1 ⟶ (const C).obj X), m = { app := fun Z ↦ hX.from (X_1.obj Z), naturality := ⋯ }

Tactic:
intros

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsTerminal X
X✝ : C ⥤ D
m✝ : X✝ ⟶ (const C).obj X
⊢ m✝ = { app := fun Z ↦ hX.from (X✝.obj Z), naturality := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsInitial X
⊢ ∀ (Y : C ⥤ D) (m : (const C).obj X ⟶ Y), m = { app := fun Z ↦ hX.to (Y.obj Z), naturality := ⋯ }

Tactic:
intros

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsInitial X
Y✝ : C ⥤ D
m✝ : (const C).obj X ⟶ Y✝
⊢ m✝ = { app := fun Z ↦ hX.to (Y✝.obj Z), naturality := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
⊢ lift t ≫ s.π.app j = t.π.app j

Tactic:
by
    cases j
    · exact facbase t
    · exact facπ t _

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).inv ≫ π (f ∘ ⇑ε) b = π f (ε b)

Tactic:
by
  simp [Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: X Y : WalkingCospan
⊢ ∀ (a b : X ⟶ Y), a = b

Tactic:
intros

Goal state after:
X Y : WalkingCospan
a✝ b✝ : X ⟶ Y
⊢ a✝ = b✝
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 B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ α.app (A ⨯ B) ≫ prodComparison H A B = prodComparison F A B ≫ prod.map (α.app A) (α.app B)

Tactic:
by
  rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
φ : f ⟶ g
⊢ Hom.left φ ≫ g.hom = f.hom

Tactic:
by
  simpa using (CommaMorphism.w φ)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ f = t.snd ≫ g

Tactic:
← hxh,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ x ≫ h = t.snd ≫ g
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ Arrow.mk h.p ≅ Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)))

Tactic:
refine Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _) ?_

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ (F.objObjPreimageIso h.Z).symm.hom ≫ (Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)))).hom =
    (Arrow.mk h.p).hom ≫ (Iso.refl (Arrow.mk h.p).right).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ ⋯.to_ (G.obj Y) = ⋯.to_ (G.obj X) ≫ G.map f

Tactic:
intros

Goal state after:
case unique_to.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ ⋯.to_ (G.obj Y✝) = ⋯.to_ (G.obj X✝) ≫ G.map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), G.map f ≫ ⋯.from_ (G.obj Y) = ⋯.from_ (G.obj X) ≫ F.map f

Tactic:
intros

Goal state after:
case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ G.map f✝ ≫ ⋯.from_ (G.obj Y✝) = ⋯.from_ (G.obj X✝) ≫ F.map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (WalkingParallelPair.casesOn Y zero one).hom = (WalkingParallelPair.casesOn X zero one).hom ≫ G.map f

Tactic:
rintro _ _ ⟨_⟩

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.map WalkingParallelPairHom.left ≫ (WalkingParallelPair.casesOn WalkingParallelPair.one zero one).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero zero one).hom ≫ G.map WalkingParallelPairHom.left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.map WalkingParallelPairHom.right ≫ (WalkingParallelPair.casesOn WalkingParallelPair.one zero one).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero zero one).hom ≫ G.map WalkingParallelPairHom.right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ zero one).hom =
    (WalkingParallelPair.casesOn X✝ zero one).hom ≫ G.map (WalkingParallelPairHom.id X✝)