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

Goal state before:
pp: case refine_1
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g = ↑ULift.moduleEquiv.symm ∘ₗ LinearMap.id

Tactic:
refine (h (ULift.{max v₁ v₃} N) <| ULift.moduleEquiv.symm.toLinearMap.comp f).unique ?_ rfl

Goal state after:
case refine_1
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑R (↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ f
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : R'
⊢ (pushoutDesc S' f g H) ((algebraMap R' S') x) = g x

Tactic:
by
  simp [Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv

Tactic:
by
  rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]
  rfl

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

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
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f

Tactic:
exact α.naturality f

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
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)

Tactic:
exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
⊢ p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

Tactic:
refine ⟨fun h => ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Goal state after:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : q₁.length = q₂.length
h : p₁.comp q₁ = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁ = q₂
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
· simp only [comp_cons, cons.injEq] at h
      obtain rfl := h.1
      obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
      rw [h.2.2.eq]
      exact ⟨rfl, rfl⟩

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

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁷ : Quiver U
inst✝⁶ : Quiver V
inst✝⁵ : Quiver W
inst✝⁴ : HasReverse U
inst✝³ : HasReverse V
inst✝² : HasReverse W
φ : U ⥤q V
ψ : V ⥤q W
inst✝¹ : φ.MapReverse
inst✝ : ψ.MapReverse
u✝ v✝ : U
e : u✝ ⟶ v✝
⊢ (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e)

Tactic:
by
    simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']

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

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : X = Y
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯

Tactic:
induction p

Goal state after:
case h_map.refl
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ G.map { down := { down := ⋯ } } = eqToHom ⋯ ≫ F.map { down := { down := ⋯ } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
⊢ Function.LeftInverse (fun f ↦ { toFun := f }) fun f ↦ ⇑f

Tactic:
by intro; rfl

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

Goal state before:
pp: X Y : Type u
⊢ Function.RightInverse (fun f ↦ { toFun := f }) fun f ↦ ⇑f

Tactic:
by intro; rfl

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

Goal state before:
pp: X Y : Type u
f : X → Y
⊢ Mono (↾f) ↔ Function.Injective f

Tactic:
by
  constructor
  · intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono (ofHom f)).mp h
  · refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
    ext y
    exact ConcreteCategory.congr_hom h y

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
e : ↑X ≃* ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommMonCatIso.isIso_hom

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
t : Cone F
ht : ∀ (s : Cone F), ∃! l, ∀ (j : J), l ≫ t.π.app j = s.π.app j
⊢ IsLimit t

Tactic:
choose s hs hs' using ht
  exact ⟨s, hs, hs'⟩

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:
by
          intros
          simp [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]

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 ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
by rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
⊢ uliftYonedaEquiv (uliftYonedaEquiv.symm x ≫ f) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.app (op (unop X)))) x))

Tactic:
rw [uliftYonedaEquiv_comp]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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
a : C
⊢ Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ ⟦a⟧ ⟦a⟧

Tactic:
exact ⟨𝟙 _⟩

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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
⊢ (adj.homEquiv s.pt F).symm m = (adj.homEquiv s.pt F).symm ((adj.homEquiv s.pt F) s.π)

Tactic:
by ext j; simpa using! hm j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasProduct f
P : C
p : (b : β) → P ⟶ f b
b : β
⊢ lift p ≫ π f b = p b

Tactic:
simp only [limit.lift_π, Fan.mk_π_app]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryFan X Y
⊢ fst ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)) =
    (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)).pt).hom ≫ (map F s).fst

Tactic:
by simp [fst]

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✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Tactic:
prodComparison,

Goal state after:
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✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prodComparison F A B ≫ prod.map (F.map f) (F.map g)
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✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Tactic:
prodComparison,

Goal state after:
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✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map prod.fst) (F.map prod.snd) ≫ prod.map (F.map f) (F.map g)
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:
prodComparison,

Goal state after:
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) ≫ prod.lift (H.map prod.fst) (H.map prod.snd) = prodComparison F A B ≫ prod.map (α.app A) (α.app 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) ≫ prod.lift (H.map prod.fst) (H.map prod.snd) = prodComparison F A B ≫ prod.map (α.app A) (α.app B)

Tactic:
prodComparison,

Goal state after:
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) ≫ prod.lift (H.map prod.fst) (H.map prod.snd) =
    prod.lift (F.map prod.fst) (F.map prod.snd) ≫ prod.map (α.app A) (α.app B)
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
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)

Tactic:
eq_mk h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (fst f₁ f₂ ≫ i₁) ≫ g₁ = (snd f₁ f₂ ≫ i₂) ≫ g₂

Tactic:
simp only [Category.assoc, ← eq₁, ← eq₂, pullback.condition_assoc]

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
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Tactic:
eq_mk h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsIso (pullback.snd f g)

Tactic:
refine ⟨⟨pullback.lift (g ≫ inv f) (𝟙 _) (by simp), ?_, by simp⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback f g)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

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✝ : F.Faithful
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0

Tactic:
rintro rfl
    exact F.map_zero _ _

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

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ (coneOfIsSplitMono f).ι = s.ι

Tactic:
dsimp
      rw [Category.assoc, ← s.condition]
      apply Category.comp_id

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((limit.isLimit F).liftConeMorphism c)

Tactic:
suffices IsIso ((Cone.functoriality F G).map
      (IsLimit.liftConeMorphism (limit.isLimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cone.functoriality F G)

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cone.functoriality F G).map ((limit.isLimit F).liftConeMorphism c))
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')

pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
· rw [h]
        exact {Hom.id j}

Goal state after:
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : PreservesLimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)
  apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
  refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasZeroObject C
inst✝ : Epi f
x✝ : Cofork f 0
⊢ Cofork.π (zeroCokernelCofork f) ≫ 0 = x✝.π

Tactic:
by simp [zero_of_epi_comp f _]

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

Goal state before:
pp: case isTrue
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), Epi (p j)
j✝¹ j✝ : J
h✝ : j✝ = j✝¹
⊢ eqToHom ⋯ ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹

pp: case isFalse
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), Epi (p j)
j✝¹ j✝ : J
h✝ : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹

Tactic:
· subst_vars
      simp

Goal state after:
case isFalse
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), Epi (p j)
j✝¹ j✝ : J
h✝ : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun a ↦ count a ↑s) (↑s).dedup

Tactic:
simp only [map_map, Function.comp_apply]

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x ↦ count (e x) (map ⇑e ↑s)) (↑s).dedup = map (fun a ↦ count a ↑s) (↑s).dedup
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary

Tactic:
refine (Finset.orderEmbOfFin_unique' _ ?_).symm

Goal state after:
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)), c.boundary x ∈ c.boundaries
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hx
ι : 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
⊢ Function.update (⇑g) a n1 a = n1

Tactic:
rw [Function.update_self]

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

Goal state before:
pp: n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ False

Tactic:
apply lt_irrefl (x : ℕ)

Goal state after:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
d : ¬_root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
x : Fin n
hx₁ : x ∈ Set.range ⇑(c.embedding i₁)
hx₂ : x ∈ Set.range ⇑(c.embedding i₂)
A : (↑i₁).succ ≤ ↑i₂
⊢ ↑x < ↑x
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case right
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (mapRange ⇑e ⋯ g).support ⊆ s

Tactic:
exact subset_trans (support_mapRange) hsupp

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

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
⊢ a ∈ c.support → a ∈ s

Tactic:
ha

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ∈ c.support
⊢ a ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
⊢ a ∈ s → c a = g a

Tactic:
ha

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a