mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : bicompr G F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x

Tactic:
intros

Goal state after:
case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ (∀ ⦃a₁ a₂ : M⦄ (x : ↥S), x • a₁ = x • a₂ → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂

Tactic:
forall_comm (α := S)

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
s : ↥S
p : LocalizedModule S M
⊢ ∀ (m : M) (s_1 : ↥S),
    ↑{ val := (algebraMap R (End R (LocalizedModule S M))) ↑s, inv := LocalizedModule.divBy s, val_inv := ⋯,
            inv_val := ⋯ }
        (LocalizedModule.mk m s_1) =
      ((algebraMap R (End R (LocalizedModule S M))) ↑s) (LocalizedModule.mk m s_1)

Tactic:
intros

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
s : ↥S
p : LocalizedModule S M
m✝ : M
s✝ : ↥S
⊢ ↑{ val := (algebraMap R (End R (LocalizedModule S M))) ↑s, inv := LocalizedModule.divBy s, val_inv := ⋯,
          inv_val := ⋯ }
      (LocalizedModule.mk m✝ s✝) =
    ((algebraMap R (End R (LocalizedModule S M))) ↑s) (LocalizedModule.mk m✝ s✝)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = mk' f (s₁ • m₁) s₁ • mk' f (s₂ • m₂) s₂

Tactic:
mk'_cancel,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = f m₁ • f m₂
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
X : T
G : A ⥤ T
F : J ⥤ StructuredArrow X G
i₁ : HasLimit (F ⋙ proj X G)
i₂ : PreservesLimit (F ⋙ proj X G) G
⊢ HasLimit F

Tactic:
by
  have : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) := i₁
  have : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) _ := i₂
  apply Comma.hasLimit

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

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
⊢ HasColimit F

Tactic:
have : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂

Goal state after:
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this✝ : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
this : PreservesColimit (F ⋙ Comma.fst G (fromPUnit X)) G
⊢ HasColimit F
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    (ConcreteCategory.hom (c.π.app j)) 1

Tactic:
RingHom.map_one

Goal state after:
case h
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) r *
      (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) =
    1
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    G.map₂ (F.map₂ (η ◁ η_1)) ≫ G.map₂ (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g') =
      (G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)

Tactic:
intros

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.map₂ (η ◁ η✝)) ≫ G.map₂ (F.mapComp η g'✝) ≫ G.mapComp (F.map η) (F.map g'✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp (𝟙 a✝) f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f)) ≫
      ((G.mapFunctor (F.obj a✝) (F.obj a✝)).map (F.mapId a✝) ≫ G.mapId (F.obj a✝)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        (λ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
dsimp
    simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_left_assoc,
      comp_whiskerRight, assoc]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
exact ⟨Q.unop, inferInstance, by rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1.inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
apply AddSubmonoid.mem_sup_left

Goal state after:
case refine_1.inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ (algebraMap R (MvPolynomial (Fin n) A)) r ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
apply AddSubmonoid.mem_sup_left

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ (algebraMap R (MvPolynomial (Fin n) A)) r ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b), NatTrans.toCatHom₂ (map₂ (𝟙 f).toNatTrans) = 𝟙 (map f.toFunctor).toCatHom

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans) = 𝟙 (map f✝.toFunctor).toCatHom
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
      NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
⊢ NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans) =
    NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    prelaxfunctor.map₂ (Bicategory.whiskerLeft f η) =
      (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
        Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
          (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝) =
    (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫
        (Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    prelaxfunctor.map₂ (Bicategory.whiskerRight η h) =
      (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
        Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
          (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝) =
    (Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).hom ≫
      Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫
        (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    prelaxfunctor.map₂ (Bicategory.associator f g h).hom =
      (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h.toFunctor)).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h) ≫
          (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom =
    (Cat.Hom.isoMk (mapComp (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom (prelaxfunctor.map h✝) ≫
        (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapComp f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom =
      (Cat.Hom.isoMk (mapComp (𝟙 a).toFunctor f.toFunctor)).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a)).hom (prelaxfunctor.map f) ≫
          (Bicategory.leftUnitor (prelaxfunctor.map f)).hom

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom =
    (Cat.Hom.isoMk (mapComp (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a✝)).hom (prelaxfunctor.map f✝) ≫
        (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom =
      (Cat.Hom.isoMk (mapComp f.toFunctor (𝟙 b).toFunctor)).hom ≫
        Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapId ↑b)).hom ≫
          (Bicategory.rightUnitor (prelaxfunctor.map f)).hom

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom =
    (Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
        (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h.some
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ some val✝ ∈ p

Tactic:
· rwa [t (WidePullbackShape.Hom.term _)]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
by
  constructor
  intro a b
  casesm* WithTerminal _, (_ : WithTerminal _) ⟶ (_ : WithTerminal _)
  · exact congr_arg (ULift.up ∘ PLift.up) rfl
  · rfl
  · rfl

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f

Tactic:
intro Z₁ Z₂ k₁ k₂ g a z
              rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w] at z
              rw [z, Category.assoc]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ (algebraMap R RXn) r ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
apply AddSubmonoid.mem_sup_left

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := ⋯
RXm : Type (max w₁ 0) := ⋯
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := ⋯
g' : Fin n → RXn := ⋯
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := ⋯
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ (algebraMap R RXn) r ∈ aeval_h.range.toAddSubmonoid
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ (pushout.inl f f).unop ≫ f.unop = (pushout.inr f f).unop ≫ f.unop

Tactic:
simp only [← unop_comp, pushout.condition]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
⊢ IsRegularEpi f

Tactic:
refine ⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩
  choose g hg using h s.condition
  refine ⟨g, hg, fun hm ↦ ?_⟩
  rwa [← cancel_epi f, hg]

Goal state after: