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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ (comap e).comp (comap e.symm) = OrderHom.id

Tactic:
ext; simp [mem_comap]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
⊢ (comap f) ((comap g) I) = (comap (g.comp f)) I

Tactic:
ext; simp [mem_comap]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M

Tactic:
exact M.mul_mem_left _ hi

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsMaximal}) = sInf {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
⊢ x ∈ I → 1 ∈ I

Tactic:
H

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
H : x ∈ I
⊢ 1 ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b → selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b

Tactic:
· intro h
    have := congr_arg (fun s : B => s * selfZPow x B (-d)) h
    rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
h : Z₁ ⟶ Z₂
fg : X₂ ⊗ Y₂ ⟶ W
⊢ (α_ X₁ Y₁ Z₁).inv ≫ ((f ⊗ₘ g) ≫ fg ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv ≫ (fg ⊗ₘ 𝟙 Z₂)

Tactic:
by simp [tensorHom_def']

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X₁ : C
inst✝ : MonObj M
f : X₁ ⟶ M
⊢ (λ_ X₁).inv ≫ (η ⊗ₘ f) ≫ μ = f

Tactic:
by simp [tensorHom_def']

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X : C
inst✝ : MonObj M
f : X ⟶ M
⊢ (α_ M M X).inv ≫ (μ ⊗ₘ f) ≫ μ = (𝟙 M ⊗ₘ (𝟙 M ⊗ₘ f) ≫ μ) ≫ μ

Tactic:
by simp [tensorHom_def']

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ { l //
    l ≫ (PullbackCone.mk h k ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk h k ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
          m ≫ (PullbackCone.mk h k ⋯).fst = s.fst → m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = l }

Tactic:
use BinaryFan.IsLimit.lift H₂ s.fst s.snd

Goal state after:
case property
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
⊢ BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (PullbackCone.mk h k ⋯).fst = s.fst ∧
    BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (PullbackCone.mk h k ⋯).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
        m ≫ (PullbackCone.mk h k ⋯).fst = s.fst →
          m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ (BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ m =
    (BinaryCofan.mk f g).ι.app { as := WalkingPair.right } ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
exact h₂.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩).symm

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
      ((AlgebraTensorModule.lTensor A M) f) =
    (AlgebraTensorModule.lTensor A M') f

Tactic:
apply linearMap_ext S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)

Goal state after:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
        ((AlgebraTensorModule.lTensor A M) f) ∘ₗ
      (AlgebraTensorModule.rTensor R N) g =
    (AlgebraTensorModule.lTensor A M') f ∘ₗ (AlgebraTensorModule.rTensor R N) g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
I : C
hI : IsInitial I
s :
  PushoutCocone (hI.to ((pair X Y).obj { as := WalkingPair.right })) (hI.to ((pair X Y).obj { as := WalkingPair.left }))
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right } ⟶ s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ m = BinaryCofan.IsColimit.desc hc s.inr s.inl

Tactic:
apply BinaryCofan.IsColimit.hom_ext hc

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
I : C
hI : IsInitial I
s :
  PushoutCocone (hI.to ((pair X Y).obj { as := WalkingPair.right })) (hI.to ((pair X Y).obj { as := WalkingPair.left }))
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right } ⟶ s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ BinaryCofan.IsColimit.desc hc s.inr s.inl

case h₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
I : C
hI : IsInitial I
s :
  PushoutCocone (hI.to ((pair X Y).obj { as := WalkingPair.right })) (hI.to ((pair X Y).obj { as := WalkingPair.left }))
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right } ⟶ s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ c.inr ≫ m = c.inr ≫ BinaryCofan.IsColimit.desc hc s.inr s.inl
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ X.coeff 1 = (C w).coeff 1

Tactic:
H

Goal state after:
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
⊢ (C ↑w).coeff 1 = (C w).coeff 1
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
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : c • x₁ = c • x₂
⊢ f x₁ = f x₂

Tactic:
by
    apply_fun f at h
    simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h
    exact ((Module.End.isUnit_iff _).mp <| map_units f c).1 h

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Products

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryProducts C
A : (prodComonad X).Coalgebra
⊢ (((𝟭 (prodComonad X).Coalgebra).obj A).a ≫
        (prodComonad X).map (Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom) ≫
      prod.snd =
    ((Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom ≫ ((coalgebraToOver X ⋙ overToCoalgebra X).obj A).a) ≫
      prod.snd

Tactic:
simpa using A.counit

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }

Tactic:
let f' : A →ₐ[R] s.pt :=
      { s.inl.hom with
        commutes' := fun r => rfl }

Goal state after:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (⇑(Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) '' Set.range ⇑(ConcreteCategory.hom a) ∪
        ⇑(Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) '' Set.range ⇑(ConcreteCategory.hom b))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom a)) ∪
        Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom b)))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ f (x - y) = 0 → ∃ c, c • x = c • y

Tactic:
h₃

Goal state after:
case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ (∃ m, m • (x - y) = 0) → ∃ c, c • x = c • y
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom

Tactic:
← F.map₂_associator,

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ (α_ f g h).inv ≫ F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ ((α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h))

pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h)

pp: case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f ≫ F.map g) (F.map h)

Tactic:
← F.map₂_associator,

Goal state after:
case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom)

case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h)

case a.a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f ≫ F.map g) (F.map h)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
⊢ Classical.choice ⋯ ∈ p'

Tactic:
simp only [p']

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
⊢ Classical.choice ⋯ ∈ {j | { down := j } ∈ p}
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫
      ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom =
    ((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
      (prod.functor.obj X).map x✝

Tactic:
apply Limits.prod.hom_ext <;> simp <;> rfl

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

Goal state before:
pp: case refine_2
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
          (NatIso.ofComponents
              (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
              ⋯).hom ≫
          prod.functor.map x✝¹).app
      x✝

Tactic:
apply Limits.prod.hom_ext <;> simp <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
by
  rw [← small_op_iff, op_unop]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, hQ⟩ := exists_small_le' P
  let P' := Q ⊓ P.isoClosure
  have h (X' : Subtype P') : ∃ (X : Subtype P), Nonempty (X'.1 ≅ X.1) :=
    ⟨⟨X'.2.2.choose, X'.2.2.choose_spec.choose⟩, X'.2.2.choose_spec.choose_spec⟩
  choose φ hφ using h
  refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
  · exact small_of_surjective (f := fun X ↦ ⟨(φ X).1, by tauto⟩)
      (by rintro ⟨_, Z, rfl⟩; exact ⟨Z, rfl⟩)
  · intro X hX
    simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX
    obtain ⟨Y, hY, rfl⟩ := hX
    exact (φ ⟨Y, hY⟩).2
  · intro X hX
    obtain ⟨Y, hY, ⟨e⟩⟩ := hQ _ hX
    let Z : Subtype P' := ⟨Y, hY, ⟨X, hX, ⟨e.symm⟩⟩⟩
    exact ⟨_, ⟨Z, rfl⟩, ⟨e ≪≫ (hφ Z).some⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.Small

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
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
⊢ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
exact ⟨‹_›, .of_functor _ F (.of_le (Q := F.essImage)
    fun Y ↦ by simp [ObjectProperty.map, Functor.essImage]) (by simpa)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ : ↑(F.obj c)
a₁✝ a₂✝ : X✝ ⟶ Y✝
base_eq✝ : 𝟙 { base := c, fiber := X✝ }.base = 𝟙 { base := c, fiber := X✝ }.base
f : eqToHom ⋯ ≫ a₁✝ = eqToHom ⋯ ≫ a₂✝
⊢ a₁✝ = a₂✝

Tactic:
rwa [cancel_epi] at f

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
⊢ LiftableCocone (F ⋙ G) H c

Tactic:
refine ⟨(liftColimit ((isColimitExtendCoconeEquiv F (G := G ⋙ H) _).symm hc)).whisker F, ?_⟩

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
⊢ H.mapCocone (Cocone.whisker F (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc))) ≅ c
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (equalizer.ι g h) ⋯).pt
w : m ≫ (Fork.ofι (equalizer.ι g h) ⋯).ι = s.ι
⊢ m = limit.lift (parallelPair g h) s

Tactic:
apply equalizer.hom_ext
      simp [← w]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right

Tactic:
repeat (rw [← Category.assoc, ← eq_whisker sq.w])

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
f : FGAlgCatSkeleton R → Skeleton (FGAlgCat R) := toSkeleton ∘ (FGAlgCat.uliftFunctor R).obj ∘ FGAlgCatSkeleton.eval R
A : Skeleton (FGAlgCat R)
⊢ ∃ a, Nonempty ((FGAlgCat.uliftFunctor R).obj (FGAlgCatSkeleton.eval R a) ≅ (fromSkeleton (FGAlgCat R)).obj A)

Tactic:
obtain ⟨P, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R
      ((fromSkeleton (FGAlgCat R)).obj A).obj

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
f : FGAlgCatSkeleton R → Skeleton (FGAlgCat R) := toSkeleton ∘ (FGAlgCat.uliftFunctor R).obj ∘ FGAlgCatSkeleton.eval R
A : Skeleton (FGAlgCat R)
P : FGAlgCatSkeleton R
e : ↑((fromSkeleton (FGAlgCat R)).obj A).obj ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R P).obj
⊢ ∃ a, Nonempty ((FGAlgCat.uliftFunctor R).obj (FGAlgCatSkeleton.eval R a) ≅ (fromSkeleton (FGAlgCat R)).obj A)