mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
p q : R[X]
hq : q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
simp [hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero]

Goal state after:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: k : Type y
inst✝ : Field k
p q : k[X]
hq : q = 0
⊢ q.natDegree = 0

Tactic:
simp [hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : q * C q.leadingCoeff⁻¹ = 1
⊢ (q * C q.leadingCoeff⁻¹).natDegree = 0

Tactic:
simp [hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
simp [hq]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case succ
σ : Type v
D : Type u
inst✝² : CommRing D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Finite σ
this : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)

Tactic:
| succ d hd =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
hp0 : p = 0
⊢ ¬p.degree = 1

Tactic:
simp [hp0]

Goal state after:
Module: Mathlib.Algebra.Azumaya.Defs

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (r • ab) • a = r • ab • a

Tactic:
by
      change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _
      simp

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ ((fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
        ⟨k, ⋯⟩)
      (f hk (e x).1) l =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨i⁺, hj⟩)
        x)
      l

Tactic:
piLTProj,

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ ((fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
        ⟨k, ⋯⟩)
      (f hk (e x).1) l =
    (piSplitLE
        (fun j ↦ equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨i⁺, hj⟩)
      x ⟨↑l, ⋯⟩
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = piLTProj h ((piLTLim hi).symm ((invLimEquiv nat) (equivLim t))) l

Tactic:
piLTProj,

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (equiv ⟨k, hk⟩) (f h t) l = (piLTLim hi).symm ((invLimEquiv nat) (equivLim t)) ⟨↑l, ⋯⟩
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : 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✝³ : (i : ι) → Star (G i)
inst✝² : Star C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), StarHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ (g i) (star x) = star ((g i) x)

Tactic:
map_star (g i)

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
⊢ Function.Even (f ∘ g)

Tactic:
by
  intro a
  simp only [comp_apply, hg a, hf _]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
⊢ Function.Odd (f ∘ g)

Tactic:
by
  intro a
  simp only [comp_apply, hg a, hf _]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive ((↑h.equiv).toFun (h.equiv.invFun m))

Tactic:
generalize h.equiv.invFun m = y

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
⊢ motive ((↑h.equiv).toFun y)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)

Tactic:
change hf.equiv.symm (s • _) = _
    dsimp
    rw [← map_smul]
    apply hf.equiv_symm_apply

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t ∈ s.powerset, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t

Tactic:
rw [powerset_card_disjiUnion, prod_disjiUnion]

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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]

Tactic:
by
  simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum,
    apply_ite Int.cast] at *
  exact Finset.sum_eq_ite _ hf

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

Goal state before:
pp: α : Type u_1
xs : List α
⊢ xs.sym2 = [] ↔ xs = []

Tactic:
cases xs <;> simp [List.sym2]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].sym2.dedup = [].dedup.sym2

Tactic:
simp only [List.sym2, dedup_nil]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

Tactic:
apply Finset.prod_congr rfl (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
⊢ ∀ (a : α × α) (b : β × β), f (Quot.mk (Rel α) a) (Quot.mk (Rel β) b)

Tactic:
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩

Goal state after:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ (p.comp q).comp (r.cons a✝) = p.comp (q.comp (r.cons a✝))

Tactic:
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ g.hom = Hom.left e.inv ≫ f.hom ≫ Hom.right e.hom

Tactic:
simp [← Arrow.comp_right]

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.map E.inverse ≤ P.inverseImage E.functor

Tactic:
rw [map_le_iff]
    intro X Y f hf
    exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((forget C).map f)

Tactic:
rwa [← @HasForget₂.forget_comp (C := C) (D := D)]

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 : CoreUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
have := adj.left_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.left_triangle] using this X

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
| e.homEquiv f

Tactic:
← Category.id_comp f,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
| e.homEquiv (𝟙 X ≫ f)
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x : X
⊢ IsIso (homOfLE ⋯)

Tactic:
change IsIso (𝟙 _)

Goal state after:
X : Type u
inst✝ : Preorder X
x : X
⊢ IsIso (𝟙 x)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
ext; apply this

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
⊢ e = e'

Tactic:
ext; apply this

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
simp [yonedaEquiv_comp]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ (∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)) → HasLiftingProperty i p

Tactic:
intro h
    exact ⟨fun {f g} sq ↦ ⟨h (Arrow.homMk f g sq.w)⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f ↔ StrongEpi g

Tactic:
by
  constructor <;> intro
  exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]

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
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : f ≫ (adj.homEquiv Y Z) g = f ≫ (adj.homEquiv Y Z) h
⊢ g = h

Tactic:
cancel_epi,

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 : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv Y Z) g = (adj.homEquiv Y Z) h
⊢ g = h
Module: Mathlib.CategoryTheory.Comma.Over.Basic

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

Tactic:
simpa using (CommaMorphism.w φ).symm

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

Goal state before:
pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro U V k

Goal state after:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)

Tactic:
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)
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)
this : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m
⊢ image.ι f = (Image.monoFactorisation f).m

Tactic:
image.as_ι

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)
this : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m
⊢ image.ι f = image.ι f
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
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ ∀ (j : WalkingParallelPair), k ≫ t.π.app j = s.π.app j

Tactic:
rintro ⟨_ | _⟩
    · exact w
    · simp only [Fork.app_one_eq_ι_comp_left, ← Category.assoc]
      congr

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ f = 0

Tactic:
← Category.id_comp f,

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
h : 𝟙 X = 0
⊢ 𝟙 X ≫ f = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ 𝟙 X = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ 𝟙 X = 0
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)
⊢ Nonempty (IsLimit c)

Tactic:
by
    suffices IsIso (IsLimit.lift (limit.isLimit F) c) from ⟨by
      apply IsLimit.ofPointIso (limit.isLimit F)⟩
    change IsIso ((Cone.forget _).map ((limit.isLimit F).liftConeMorphism c))
    suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by
      apply (Cone.forget F).map_isIso _
    suffices IsIso ((Cone.functoriality F G).map
      (IsLimit.liftConeMorphism (limit.isLimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cone.functoriality F G)
    exact t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _

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

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
⊢ IsIso (α.app c.pt)

Tactic:
let e := IsColimit.coconePointsIsoOfNatIso
    (isColimitOfPreserves L hc) (isColimitOfPreserves L' hc) (asIso (whiskerLeft K α))
  convert! (inferInstance : IsIso e.hom)
  apply (isColimitOfPreserves L hc).hom_ext fun j ↦ ?_
  simp only [Functor.comp_obj, Functor.mapCocone_pt, Functor.mapCocone_ι_app,
    NatTrans.naturality, IsColimit.coconePointsIsoOfNatIso_hom, asIso_hom, e]
  refine (((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm
  simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : f ≫ (-g) = f ≫ (-g')
⊢ g = g'

Tactic:
cancel_epi,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -g = -g'
⊢ g = g'
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
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ IsZero (F.obj x✝²)

Tactic:
rw [IsZero.iff_id_eq_zero]

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
inst✝¹ : Preadditive C
inst✝ : Preadditive D
F : C ⥤ D
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ 𝟙 (F.obj x✝²) = 0
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
j : Subtype p
k : Subtype pᶜ
⊢ (if h : p ↑k then biproduct.ι (Subtype.restrict p f) ⟨↑k, h⟩ else 0) ≫ biproduct.π (Subtype.restrict p f) j = 0

Tactic:
rw [dif_neg k.2]

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype p
k : Subtype pᶜ
⊢ 0 ≫ biproduct.π (Subtype.restrict p f) j = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ IsZero (A ⊞ B)

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) = 0