mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
x' : k
H : (algebraMap k D) x' = (algebraMap K D) x
⊢ (algebraMap K D) ((algebraMap k K) x') = (algebraMap K D) x

Tactic:
simp [← H, algebraMap_eq_smul_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
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
a : A
x✝ : IsAlgebraic R (f a)
p : R[X]
hp0 : p ≠ 0
hp : (aeval (f a)) p = 0
⊢ (f.comp (aeval a)) p = 0

Tactic:
← aeval_algHom

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
a : A
x✝ : IsAlgebraic R (f a)
p : R[X]
hp0 : p ≠ 0
hp : (aeval (f a)) p = 0
⊢ (aeval (f a)) p = 0
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ restrictSupport R s * restrictSupport R t ≤ restrictSupport R (s + t)

Tactic:
· rw [restrictSupport_eq_span, restrictSupport_eq_span, Submodule.span_mul_span,
      Submodule.span_le, Set.mul_subset_iff]
    simp +contextual [Set.add_mem_add]

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

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
x : M ⊗[R] N
⊢ ∃ S, x = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨Finsupp.single x y, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    use Sx + Sy
    rw [hx, hy]
    exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
x y : N ⊗[R] M
eq : (rTensor M f) x = (rTensor M f) y
⊢ x = y

Tactic:
by
  have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)
  obtain ⟨x, rfl⟩ := sub (.inl rfl)
  obtain ⟨y, rfl⟩ := sub (.inr rfl)
  simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl, rTensor_comp_apply] at eq
  have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
  simp_rw [← rTensor_comp_apply] at eq
  rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ ((↑(#s))⁻¹ • ∑ i ∈ s, f i) * a = (↑(#s))⁻¹ • ∑ i ∈ s, f i * a

Tactic:
smul_mul_assoc,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ (↑(#s))⁻¹ • ((∑ i ∈ s, f i) * a) = (↑(#s))⁻¹ • ∑ i ∈ s, f i * a
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
⊢ ⟨j - 1, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
by simp [le_iff_val_le_val]

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
z : Sym2 α
hz : z ∈ map (fun y ↦ s(x, y)) (x :: xs)
⊢ z ∈ xs.sym2 → False

Tactic:
hz'

Goal state after:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
z : Sym2 α
hz : z ∈ map (fun y ↦ s(x, y)) (x :: xs)
hz' : z ∈ xs.sym2
⊢ False
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2).dedup = s(x, x) :: map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2

Tactic:
cons_append,

Goal state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2).dedup = s(x, x) :: (map (fun y ↦ s(x, y)) xs.dedup ++ xs.sym2.dedup)

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : z ∈ map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))
⊢ z ∈ List.sym (n + 1) xs → False

Tactic:
hz'

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : z ∈ map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))
hz' : z ∈ List.sym (n + 1) xs
⊢ False
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
z : Sym2 α
⊢ ↑(map f z) = f '' ↑z

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ y✝ : α
⊢ ↑(map f s(x✝, y✝)) = f '' ↑s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mp
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)

Tactic:
cases z

Goal state after:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ x ∈ s(x✝, y✝) ∧ y ∈ s(x✝, y✝) → s(x✝, y✝) = s(x, y)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a ∈ z, f a = b

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
b : β
x✝ y✝ : α
⊢ b ∈ map f s(x✝, y✝) ↔ ∃ a ∈ s(x✝, y✝), f a = b
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
z : Sym2 α
h : ∀ a ∈ z, P a
⊢ pmap (fun a x ↦ f a) z h = map f z

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ pmap (fun a x ↦ f a) s(x✝, y✝) h = map f s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ b ∈ map f z, Q b
⊢ pmap g (map f z) h = pmap (fun a ha ↦ g (f a) ⋯) z ⋯

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ b ∈ map f s(x✝, y✝), Q b
⊢ pmap g (map f s(x✝, y✝)) h = pmap (fun a ha ↦ g (f a) ⋯) s(x✝, y✝) ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ map g (pmap f z h) = pmap (fun a ha ↦ g (f a ⋯)) z ⋯

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ map g (pmap f s(x✝, y✝) h) = pmap (fun a ha ↦ g (f a ⋯)) s(x✝, y✝) ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ pmap g (pmap f z h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) z ⋯

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
h' : ∀ b ∈ pmap f s(x✝, y✝) h, Q b
⊢ pmap g (pmap f s(x✝, y✝) h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) s(x✝, y✝) ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
z : Sym2 α
h : z.IsDiag
⊢ diag (z.diagElem h) = z

Tactic:
cases z

Goal state after:
case h
α : Type u_1
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ diag (s(x✝, y✝).diagElem h) = s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
sym : Std.Symm r
f : α → β
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ map f z ∈ fromRel sym

Tactic:
cases z

Goal state after:
case h
α : Type u_1
β : Type u_2
r : β → β → Prop
sym : Std.Symm r
f : α → β
x✝ y✝ : α
⊢ s(x✝, y✝) ∈ fromRel ⋯ ↔ map f s(x✝, y✝) ∈ fromRel sym
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁴ : CommSemiring R'
inst✝²³ : CommSemiring S'
inst✝²² : Algebra R R'
inst✝²¹ : Algebra S S'
inst✝²⁰ : Algebra R' S'
inst✝¹⁹ : Algebra R S'
inst✝¹⁸ : IsScalarTower R R' S'
inst✝¹⁷ : IsScalarTower R S S'
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
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C

Tactic:
refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)
  · simp [TensorProduct.one_def]
  · apply LinearMap.map_mul_of_map_mul_tmul
    simp

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
Y : D
⊢ (∃ X, P X ∧ F.obj X = Y) → P.strictMap F Y

Tactic:
rintro ⟨X, hX, rfl⟩

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
X : C
F : C ⥤ D
x✝ : D
⊢ (singleton X).strictMap F x✝ ↔ singleton (F.obj X) x✝

Tactic:
simp [strictMap_iff]

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

Goal state before:
pp: case mk.mk.mk
α : Type u₁
as✝² as✝¹ : α
g : ULift.{u₁, 0} (PLift ({ as := as✝² }.as = { as := as✝¹ }.as))
as✝ : α
f : ULift.{u₁, 0} (PLift ({ as := as✝¹ }.as = { as := as✝ }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as✝² }.as = { as := as✝ }.as))

Tactic:
rcases f with ⟨⟨⟨⟩⟩⟩

Goal state after:
case mk.mk.mk
α : Type u₁
as✝¹ as✝ : α
g : ULift.{u₁, 0} (PLift ({ as := as✝¹ }.as = { as := as✝ }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as✝¹ }.as = { as := as✝ }.as))
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget MonCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toMonCatIso.isIso_hom

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ coneOfHom h f = (limitCone h).extend f

Tactic:
by
  dsimp [coneOfHom, limitCone, Cone.extend]
  congr
  conv_lhs => rw [← Category.comp_id f]
  exact h.homEquiv_comp f (𝟙 X)

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
simp [homEquiv_comp]

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 Y' : C
y : F.obj Y
g : Y ⟶ Y'
⊢ e.homEquiv (e.homEquiv.symm y ≫ g) = e.homEquiv (e.homEquiv.symm ((ConcreteCategory.hom (F.map g)) y))

Tactic:
simp [homEquiv_comp]

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:
rw [← Category.id_comp f, e.homEquiv_comp]

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
| (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X))
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
simp [uliftYonedaEquiv, uliftYoneda, ← f.naturality_apply]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = hl.lift { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } } ≫ hi.hom

Tactic:
rw [← hl.uniq _ (f ≫ hi.inv) _]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = (f ≫ hi.inv) ≫ hi.hom

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j = { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.π.app j
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
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
  simp

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
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
simp only [HasLimit.isoOfEquivalence]
  simp

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

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)

Tactic:
exact hπ j

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

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

Tactic:
obtain rfl := Subsingleton.elim j default
        apply Category.id_comp

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

Goal state before:
pp: case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
← cancel_epi f

Goal state after:
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ f ≫ c.inl ≫ m = f ≫ c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

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

Tactic:
← cancel_epi f

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
this : l' = homMk m ⋯
⊢ l = m

Tactic:
apply congrArg CommaMorphism.right this

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 : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt
hm₁ : (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl
hm₂ : (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr
⊢ m = l

Tactic:
exact (PushoutCocone.IsColimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

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 f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f

Tactic:
rw [h]; simp only [image.fac]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = 0

Tactic:
by
  have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]
  simpa using h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ kernel.lift f g h ≫ 0 = 0

Tactic:
Limits.comp_zero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ Cofork.π c ≫ 0 = 0

Tactic:
Limits.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ 0 = 0
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 : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ g = inv f ≫ 0 ↔ g = 0

Tactic:
Limits.comp_zero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ g = 0 ↔ g = 0
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
W : C
g : W ⟶ X
h : W ⟶ Y
c : CokernelCofork h
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h
s : Cofork f 0
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ i.desc (CokernelCofork.ofπ s.π ⋯) = s.π

Tactic:
by simp only [CokernelCofork.π_ofπ, Cofork.IsColimit.π_desc]

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✝ : HasCokernel f
h : f = f
⊢ coequalizer.π f 0 ≫ (cokernelIsoOfEq h).hom = coequalizer.π f 0 ≫ (Iso.refl (cokernel f)).hom

Tactic:
simp [cokernelIsoOfEq]

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

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
P Q P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ BinaryFan.fst ((Cone.postcompose (mapPairIso eP eQ).hom).obj b.toCone) =
    (Iso.refl ((Cone.postcompose (mapPairIso eP eQ).hom).obj b.toCone).pt).hom ≫ BinaryFan.fst (b.ofIso eP eQ).toCone

Tactic:
by simp [BinaryFan.fst]

Goal state after:
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
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)

Tactic:
· rintro ⟨hA, hB⟩
    rw [IsZero.iff_id_eq_zero]
    apply biprod.hom_ext
    · apply hA.eq_of_tgt
    · apply hB.eq_of_tgt

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

Goal state before:
pp: n : ℕ
x : { x // x ≠ last n }
⊢ (finSuccAboveOrderIso (last n)).symm x = (↑x).castLT ⋯

Tactic:
by
  rw [← Option.some_inj]
  simp [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]

Goal state after: