mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.tmul.add
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 B
x✝ : A ⊗[R] B
hx✝ : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
a : A
b : B
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y
⊢ ∃ y_1,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case a.add
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 B
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x ∈ ↑(Submodule.restrictScalars R (map includeRight I))
hy :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈ ↑(Submodule.restrictScalars R (map includeRight I))
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y) ∈
    ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hx : ∃ k m n, x = ∑ j, m j ⊗ₜ[R] n j
hy : ∃ k m n, y = ∑ j, m j ⊗ₜ[R] n j
⊢ ∃ k m n, x + y = ∑ j, m j ⊗ₜ[R] n j

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ (s.disjUnion t h).dens = s.dens + t.dens

Tactic:
simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₁
inst✝ : Module.Flat R N₂
⊢ Function.Injective ⇑(hf.map hg i₁ i₂)

Tactic:
have h : hf.map hg i₁ i₂ = hg.equiv ∘ TensorProduct.map i₁ i₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using map_injective_of_flat_flat' i₁ i₂ h₁ h₂

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝ : DivisionSemiring K
s : Finset ι
f : ι → K
a : K
⊢ (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Tactic:
simp only [div_eq_mul_inv, sum_mul]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ((map₀RingHom f).comp (algebraMap R ((i : ι) → G i))) r * ⟦⟨i, x✝⟩⟧ =
    ⟦⟨i, x✝⟩⟧ * ((map₀RingHom f).comp (algebraMap R ((i : ι) → G i))) r

Tactic:
by
    dsimp [Pi.algebraMap_def, map₀RingHom]
    rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
by
  wlog hj : j < k + 1 generalizing j
  · grind [cast_val_eq_self]
  by_cases hj : j = k
  · simp [hj]
  · have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
    grind

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a

Tactic:
exact Int.emod_nonneg n (ne_of_gt ha)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ (s • 1) ⊗ₜ[R] x = s ⊗ₜ[R] x

Tactic:
congr 1

Goal state after:
case e_m
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 = s
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * g s' = g ((algebraMap S S') s) * g s'

Tactic:
congr 1

Goal state after:
case refine_3.e_a
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
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'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) = g ((algebraMap S S') s)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
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'
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
x y : S ⊗[R] M
hx : ↑(cancelBaseChangeAux R S A B M).symm (s • x) = s • ↑(cancelBaseChangeAux R S A B M).symm x
hy : ↑(cancelBaseChangeAux R S A B M).symm (s • y) = s • ↑(cancelBaseChangeAux R S A B M).symm y
⊢ ↑(cancelBaseChangeAux R S A B M).symm (s • (x + y)) = s • ↑(cancelBaseChangeAux R S A B M).symm (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj X Y → ∃ i, X i = Y

Tactic:
rintro ⟨i⟩

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ∃ i_1, X i_1 = X i
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F.unop ⟶ G.unop
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (α.app (unop Y)).op).unop = ((α.app (unop X)).op ≫ F.map f).unop

Tactic:
simpa only [Functor.unop_map] using! (α.naturality f.unop).symm

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ ((NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    ({ app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom).op

Tactic:
congr 1

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop =
    { app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op

Tactic:
congr 1

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (unop G).rightOpLeftOpIso.hom ≫ η.unop =
    NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ isomorphisms C = ⊤ → IsGroupoid C

Tactic:
intro h
    exact ⟨of_eq_top h⟩

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

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
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i

Tactic:
by simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ ofHoms f g → ∃ i, Arrow.mk g = Arrow.mk (f i)

Tactic:
rintro ⟨i⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X✝ Y✝ : ι → C
f : (i : ι) → X✝ i ⟶ Y✝ i
X Y : C
i : ι
⊢ ∃ i_1, Arrow.mk (f i) = Arrow.mk (f i_1)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.left (aux φ) = Hom.left (aux ψ)

Tactic:
congr 1

Goal state after:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ aux φ = aux ψ
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.isoClosure = P

Tactic:
by rwa [isoClosure_eq_iff]

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

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
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s

Tactic:
apply P.uniq_cone_morphism

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 h : b ⟶ c
η : g ≅ h
⊢ f ◁ 𝟙 g = 𝟙 (f ≫ g)

Tactic:
whiskerLeft_id

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ 𝟙 (f ≫ g) = 𝟙 (f ≫ g)
Module: Mathlib.CategoryTheory.Bicategory.Basic

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

Tactic:
whiskerLeft_id

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ 𝟙 (f ≫ h) = 𝟙 (f ≫ h)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
⊢ Function.RightInverse
    (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) fun η ↦
    (ConcreteCategory.hom (η.app (op X))) (𝟙 X)

Tactic:
intro ξ; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
⊢ Function.RightInverse (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
    fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)

Tactic:
intro ξ; simp

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
⊢ Small.{w, max u v} (Arrow C)

Tactic:
refine small_of_injective (f := φ) ?_

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
⊢ Function.Injective φ
Module: Mathlib.CategoryTheory.Limits.Cones

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
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
⊢ ∀ (j : K),
    (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app j =
      (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt).hom ≫
        ((𝟭 (Cone (e.functor ⋙ F))).obj s).π.app j

Tactic:
by
            intro k
            simpa [e.counit_app_functor] using s.w (e.unitInv.app k)

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

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ (productUniqueIso f).inv ≫ Pi.π f b = eqToHom ⋯

Tactic:
obtain rfl := Subsingleton.allEq b default

Goal state after:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
⊢ (productUniqueIso f).inv ≫ Pi.π f default = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom ⋯

Tactic:
obtain rfl := Subsingleton.allEq b default

Goal state after:
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
⊢ Sigma.ι f default ≫ (coproductUniqueIso f).hom = eqToHom ⋯
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
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
congr 1

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
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
      Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯ =
    Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
      Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯
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
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))

Tactic:
congr 1

Goal state after:
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
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : J
⊢ data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯) =
    data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)

Tactic:
congr 1

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ h ≫ x ≫ s.inl = f ≫ s.inl

Tactic:
by  -- Porting note: working around reassoc
      rw [← Category.assoc]; apply congrArg (· ≫ inl s) hhx

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ h ≫ y ≫ s.inr = g ≫ s.inr

Tactic:
rw [← Category.assoc]; apply congrArg (· ≫ inr s) hhy

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ 𝟙 Z = ((Image.monoFactorisation f).compMono g).m

Tactic:
← IsIso.inv_hom_id g,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g ≫ g = ((Image.monoFactorisation f).compMono g).m
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₁)
⊢ (Hom.hom (↟↑e ≫ ↟↑e.symm)) x✝ = (Hom.hom (𝟙 (of R X₁))) x✝

Tactic:
apply e.left_inv

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

Goal state before:
pp: case calc_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y)

Tactic:
rw [Adjunction.left_triangle_components]

Goal state after:
case calc_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ 𝟙 (F.obj Y)
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
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (lift f g)

Tactic:
by
  rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃ IsLimit (Fan.mk (G.obj P) fun j ↦ G.map (g j))

Tactic:
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
  · exact Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
  exact Cone.ext (Iso.refl _) fun j ↦ by dsimp; cases j; simp

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr

Tactic:
refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)

Goal state after:
case refine_1
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inl ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inl ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j