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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
by
  by_cases hp0 : p = 0; · simp only [hp0, rootMultiplicity_zero, Polynomial.map_zero]
  apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)
  rw [le_rootMultiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
    Polynomial.map_pow, Polynomial.map_sub, map_X, map_C]
  apply pow_rootMultiplicity_dvd

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ (Associates.mk a).factors

Tactic:
rw [factors_mk _ ha0]
  exact mem_factorSet_some.mpr (mem_factors'_of_dvd ha0 hp hd)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q ≠ 0
⊢ p ∣ q.primPart ↔ p ∣ q

Tactic:
refine ⟨fun h => h.trans (Dvd.intro_left _ q.eq_C_content_mul_primPart.symm), fun h => ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q ≠ 0
h : p ∣ q
⊢ p ∣ q.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
r : R[X]
hq : p * r ≠ 0
⊢ p ∣ (p * r).primPart

Tactic:
exact .trans (by simp [hp.primPart_eq]) (associated_primPart_mul hq).symm.dvd

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
p : R[X]
inst✝¹ : CommRing k
inst✝ : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ eval x (map f p) = 0 ↔ eval₂ f x p = 0

Tactic:
Polynomial.eval_map

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
p : R[X]
inst✝¹ : CommRing k
inst✝ : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ eval₂ f x p = 0 ↔ eval₂ f x p = 0
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (if a = 0 then ⊤ else ↑a.degree, a.leadingCoeff)
    (if a * c = 0 then ⊤ else ↑(a * c).degree, (a * c).leadingCoeff)

Tactic:
Polynomial.degree_mul,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (if a = 0 then ⊤ else ↑a.degree, a.leadingCoeff)
    (if a * c = 0 then ⊤ else ↑(a.degree + c.degree), (a * c).leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹).leadingCoeff * (p /ₘ (q * C q.leadingCoeff⁻¹)).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
leadingCoeff_C,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)).leadingCoeff = p.leadingCoeff / q.leadingCoeff
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), (conjAlgEquiv S g) a = (conjAlgEquiv S f) a) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
conjAlgEquiv_apply,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), ↑g ∘ₗ a ∘ₗ ↑g.symm = ↑f ∘ₗ a ∘ₗ ↑f.symm) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (g a)) (map (↑f) q) = 0
h' : q = 0
⊢ False

Tactic:
by simp [h'] at h1

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ ↑g ((aeval a) q) = 0

Tactic:
map_aeval_eq_aeval_map h,

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ (aeval (↑g a)) (map (↑f) q) = 0
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
g : G i
⊢ (linearEquiv G f) ((of R ι G f i) g) = ⟦⟨i, g⟩⟧

Tactic:
simp [linearEquiv]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : 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 ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
i✝ : ι
hj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by exact k.2.1

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Bijective ⇑(AlgHom.mulLeftRight R R)

Tactic:
rw [← coe_tensorEquivEnd]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Bijective ⇑↑(tensorEquivEnd R)
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✝¹
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f✝ : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y
h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y
⊢ ∀ (c : T) (m : M₁) (n : M₂), (f (c • m)) n = c • (f m) n

Tactic:
by simp [h₁]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ Nat.card ↑(f ⁻¹' ↑t) = ∑ b ∈ t, Nat.card ↑{a | f a = b}

Tactic:
rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]

Goal state after:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ ∑ b ∈ image f ht.toFinset, #({a ∈ ht.toFinset | f a = b}) = ∑ b ∈ t, Nat.card ↑{a | f a = b}
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
obtain ⟨z, hz, rfl⟩ | hz := hz

Goal state after:
case inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a ∈ x :: xs

case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
F : C ⥤ E
⊢ ((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
      (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F) =
    𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)

Tactic:
by
    ext X
    dsimp
    simp only [funInvIdAssoc_inv_app, id_obj, comp_obj, invFunIdAssoc_hom_app,
      Functor.comp_map, ← F.map_comp, unit_inverse_comp, map_id]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ iInf W f ↔ ∀ (i : ι), W i f

Tactic:
simp [← sInf_range]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P.inverseImage F f
⊢ P.inverseImage F (f ≫ e)

Tactic:
by
    simpa [MorphismProperty.inverseImage, cancel_right_of_respectsIso] using hf

Goal state after:
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)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).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.toMonCatIso.isIso_hom

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_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Tactic:
rw [Equiv.eq_symm_apply, he]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
a : Cᵒᵖ ⥤ Type u₁
b : ((yoneda.op ⋙ coyoneda).obj X).obj a
⊢ (ConcreteCategory.hom
          (((yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom).app a)).toFun
      b =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f).app a)).toFun
      b

Tactic:
simp [yonedaEquiv, ← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : Cᵒᵖ ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
intro Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y : Cᵒᵖ ⥤ Type v₁
⊢ ∀ {Y_1 : Cᵒᵖ ⥤ Type v₁} (f : Y ⟶ Y_1),
    ((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type v₁) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
intro Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : Cᵒᵖ
⊢ ∀ {Y_1 : Cᵒᵖ} (f : Y ⟶ Y_1),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
intro Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y : C ⥤ Type v₁
⊢ ∀ {Y_1 : C ⥤ Type v₁} (f : Y ⟶ Y_1),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
intro Y

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : C
⊢ ∀ {Y_1 : C} (f : Y ⟶ Y_1),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ Function.LeftInverse (fun u ↦ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ }) fun t X ↦
    {
      default :=
        t.lift { pt := X, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } },
      uniq := ⋯ }

Tactic:
dsimp [Function.LeftInverse]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ (x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }),
    { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ Function.LeftInverse (fun u ↦ { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ }) fun t X_1 ↦
    {
      default :=
        t.desc { pt := X_1, ι := { app := fun X_2 ↦ id (Discrete.casesOn X_2 fun as ↦ ⋯.elim), naturality := ⋯ } },
      uniq := ⋯ }

Tactic:
dsimp [Function.LeftInverse]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ ∀ (x : IsColimit { pt := X, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }),
    { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x
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₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl ↦ isLimitChangeEmptyCone C hl c₁ h.symm) fun hl ↦ isLimitChangeEmptyCone C hl c₂ h

Tactic:
dsimp [Function.LeftInverse]

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₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsLimit c₁), isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x c₂ h) c₁ h.symm = x
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₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl ↦ isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl ↦
    isColimitChangeEmptyCocone C hl c₂ h

Tactic:
dsimp [Function.LeftInverse]

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₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsColimit c₁), isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x c₂ h) c₁ h.symm = x
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''

Tactic:
reassoc_of% e₂,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''

Tactic:
reassoc_of% e₂,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ f₁ ≫ 𝟙 Z = 𝟙 X ≫ f₂

Tactic:
by simp [h₁]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁

Tactic:
by simp [h₁]

Goal state after: