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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⇑(OreLocalization.oreEqv S M) = r S M

Tactic:
ext a b

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
⊢ (OreLocalization.oreEqv S M) a b ↔ r S M a b
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
S : Submonoid R
⊢ Localization S = LocalizedModule S R

Tactic:
with_reducible rfl

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x : LocalizedModule S M
f : M × ↥S → α
wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'
⊢ ∀ (a b : M × ↥S), a ≈ b → f a = f b

Tactic:
by simpa +instances only [r.setoid, ← oreEqv_eq_r S M] using wd

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x y : LocalizedModule S M
f : M × ↥S → M × ↥S → α
wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
⊢ ∀ (a₁ b₁ a₂ b₂ : M × ↥S), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂

Tactic:
by simpa +instances only [r.setoid, ← oreEqv_eq_r S M] using wd

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ IsColimit (F.mapCocone (BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)))

Tactic:
apply isColimitOfPreserves _ (Nonempty.some ?_)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ Nonempty (IsColimit (BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s s' : ↥S
m : M
⊢ 1 • s • s' • m = 1 • (s * s') • m

Tactic:
by simp [mul_smul]

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
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 • f x₁ = ↑c • f x₂
⊢ f x₁ = f x₂

Tactic:
← Module.algebraMap_end_apply R R

Goal state after:
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 : ((algebraMap R (End R M')) ↑c) (f x₁) = ((algebraMap R (End R M')) ↑c) (f x₂)
⊢ f x₁ = f x₂
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)

Tactic:
rw [← map_id, ← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _,
    map_comp, T.map_unit_app X, ← T.unit_naturality]

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

Goal state before:
pp: case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext r

Goal state after:
case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: 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
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (F.map f)) (inv j) = inv k

Tactic:
← mul_one (F.map f (inv j)),

Goal state after:
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
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (F.map f)) (inv j) * 1 = inv k
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝¹ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
inst✝ : IsLocalRing ↑(F.obj j)
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsLocalRing ↑c.pt

Tactic:
by
  have := π_isLocalHom F hc j hj
  apply RingHom.domain_isLocalRing (c.π.app j).hom

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
⊢ IsLocalHom (Hom.hom (limit.π F (op one)))

Tactic:
by
  refine Limits.π_isLocalHom _ (limit.isLimit _) (op one) fun x hx i ↦ ?_
  rcases i with _ | _
  · refine ⟨op zero, 𝟙 _, op left, inferInstance, ?_⟩
    simp only [CategoryTheory.Functor.map_id, hom_id, limit.cone_x, limit.cone_π,
      RingHom.id_apply]
    exact (limit.w_apply F (op left) x).symm
  · exact ⟨op one, 𝟙 _, 𝟙 _, inferInstance, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
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.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
    G.map (F.map f) ◁ G.mapComp (F.map g) (F.map h) ≫
      G.mapComp (F.map f) (F.map g ≫ F.map h) ≫ G.map₂ (F.map f ◁ F.mapComp 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.map₂ (F.mapComp f (g ≫ h))

Tactic:
← map₂_associator_assoc

Goal state after:
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) ≫
    G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
      G.map₂ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)

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.map₂ (F.mapComp f (g ≫ h))
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∑ m_1 ∈ Finset.range (n + m + 1), J ^ m_1 * K ^ (n + m - m_1) * ↑((n + m).choose m_1) ≤ I

Tactic:
sum_eq_sup,

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ((Finset.range (n + m + 1)).sup fun m_1 ↦ J ^ m_1 * K ^ (n + m - m_1) * ↑((n + m).choose m_1)) ≤ I
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans h')

Goal state after:
case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J
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✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory
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
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le 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
F : C ⥤ D
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
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
inst✝ : EssentiallySmall.{w, v, u} C
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage

Tactic:
rw [← ObjectProperty.map_top]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber) ≫
      colimit.ι (Grothendieck.ι F x✝.base ⋙ G) ((F.map f.base).toFunctor.obj x✝¹.fiber)

Tactic:
← colimit.w (Grothendieck.ι F _ ⋙ G) f.fiber

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber) ≫
      (Grothendieck.ι F x✝.base ⋙ G).map f.fiber ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber
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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber

Tactic:
by
    rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]

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
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
X : Grothendieck F
⊢ (hom (𝟙 X).base).app X.fiber ≫ (fib X.base).map (𝟙 X).fiber = 𝟙 ((fib X.base).obj X.fiber)

Tactic:
simp [hom_id]

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
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).map f ≫
      (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).obj Y✝)).hom =
    (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c'} ↦ hom) hom_id hom_comp).obj X✝)).hom ≫ (fib c).map f

Tactic:
simp [hom_id]

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 : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X : StructuredArrow d G
⊢ (F.map X.hom).toFunctor.obj { base := d, fiber := f }.fiber ⟶
    ((pre F G).obj { base := X.right, fiber := (F.map X.hom).toFunctor.obj f }).fiber

Tactic:
by dsimp; exact 𝟙 _

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ (StructuredArrow.mk
          { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).right.base ⟶
    (StructuredArrow.right
        { left := { as := PUnit.unit }, right := { base := bi, fiber := fi },
          hom := { base := gbi, fiber := gfi } }).base

Tactic:
by dsimp; exact 𝟙 _

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ (StructuredArrow.mk
          { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).right.base ⟶
    (StructuredArrow.right
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).base

Tactic:
by dsimp; exact 𝟙 _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a ≫ 𝟙 X
⊢ Mono f

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ Mono f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q

Tactic:
exact le_trans (pushouts_monotone h) pushouts_le

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

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      (extendFan c₁ c₂).π.app { as := j } =
    s.π.app { as := j }

Tactic:
refine Fin.inductionOn j ?_ ?_

Goal state after:
case refine_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      (extendFan c₁ c₂).π.app { as := 0 } =
    s.π.app { as := 0 }

case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
              (t₁.lift
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x ↦
                      match x with
                      | { as := i } => s.π.app { as := i.succ } })) ≫
          (extendFan c₁ c₂).π.app { as := i.castSucc } =
        s.π.app { as := i.castSucc } →
      ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
              (t₁.lift
                { pt := s.pt,
                  π :=
                    Discrete.natTrans fun x ↦
                      match x with
                      | { as := i } => s.π.app { as := i.succ } })) ≫
          (extendFan c₁ c₂).π.app { as := i.succ } =
        s.π.app { as := i.succ }
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) g

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
⊢ (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)

Tactic:
ext r

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
r : R'
⊢ ((↑e.symm).comp (algebraMap R' S')) r = (algebraMap R' (R' ⊗[R] S)) r
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape J ≤ (P.strictLimitsOfShape J).isoClosure

Tactic:
intro X ⟨h⟩
    have := h.hasLimit
    exact ⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
      ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩

Goal state after: