mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y * (algebraMap R Rₘ) ↑y)

Tactic:
IsLocalization.mk'_spec

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R (Localization M)) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk
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'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a : A
s : ↥S
⊢ 0 * Quot.mk ⇑(OreLocalization.oreEqv S A) (a, s) = 0

Tactic:
exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩

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

Goal state before:
pp: case property.left
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 := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl

pp: case property.right
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 := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
      s.inr ∧
    ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
      ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
        ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ m = s.inr →
          m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
· ext x
      exact Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x

Goal state after:
case property.right
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 := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
      s.inr ∧
    ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
      ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
        ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ m = s.inr →
          m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x x' : Under X
u : x ⟶ x'
⊢ x.hom ≫ Hom.right u ≫ pushout.inl x'.hom f = f ≫ pushout.inr x'.hom f

Tactic:
by simp [← pushout.condition]

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

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
⊢ Algebra.IsPushout R R' S S'

Tactic:
have h2 (r : R') : (CommRingCat.isPushout_tensorProduct R R' S).isoPushout.hom
      (r ⊗ₜ 1) = (pushout.inl (ofHom _) (ofHom _)) r :=
    congr($((CommRingCat.isPushout_tensorProduct R R' S).inl_isoPushout_hom).hom r)

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
⊢ Algebra.IsPushout R R' S S'
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
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤

Tactic:
algebraize [f.hom, g.hom]

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
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤
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
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤

Tactic:
let e := ((isPushout_tensorProduct R A B).isoIsPushout A B H).commRingCatIsoToRingEquiv

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.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv

Tactic:
← F.mapComp_naturality_right_assoc,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ F.mapComp f h ≫ (F'.mapCompIso f h).inv
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (span ↑s • Submodule.span R ↑t).FG

Tactic:
classical rw [Submodule.span_smul_span, ← s.coe_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (Submodule.span R ↑(s • t)).FG
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
inst✝¹ : IsPreconnected J
inst✝ : IsPreconnected K
a : Type (max u₁ u₂)
F : J × K ⥤ Discrete a
x✝¹ x✝ : J × K
j : J
k : K
j' : J
k' : K
⊢ F.obj (j, k) = F.obj (j', k')

Tactic:
exact (any_functor_const_on_obj (Prod.sectL J k ⋙ F) j j').trans
    (any_functor_const_on_obj (Prod.sectR j' K ⋙ F) k k')

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ : J
⊢ ∀ (j₂ : J), r j₁ j₂

Tactic:
j₂

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
⊢ r j₁ j₂
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ : J
⊢ ∀ (j₂ : J), Zigzag j₁ j₂

Tactic:
j₂

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
j₁ j₂ : J
⊢ Zigzag j₁ 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✝ : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
simpa only [← small_congr P.unop.subtypeOpEquiv]

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ : C
⊢ ∀ (X₂ : C) (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : j₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j

Tactic:
j₂

Goal state after:
case h₁
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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ colimit.ι F j ≫ colimMap c.ι =
    colimit.ι F j ≫
      ((colimit.isColimit F).coconePointUniqueUpToIso hc ≪≫
          (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom

Tactic:
simp only [ι_colimMap, colimit.cocone_x, Iso.trans_hom,
    colimit.comp_coconePointUniqueUpToIso_hom_assoc]

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ c.ι.app j ≫ colimit.ι ((Functor.const J).obj c.pt) j =
    c.ι.app j ≫
      ((isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom
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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ : C
⊢ ∀ (X₂ : C) (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : j₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j

Tactic:
j₂

Goal state after:
case h₂
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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ : CostructuredArrow F d
⊢ {j₂ : CostructuredArrow F d} → (j₁ ⟶ j₂) → Z j₁.left j₁.hom → Z j₂.left j₂.hom

Tactic:
j₂

Goal state after:
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
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
⊢ (j₁ ⟶ j₂) → Z j₁.left j₁.hom → Z j₂.left j₂.hom
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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ : CostructuredArrow F d
⊢ {j₂ : CostructuredArrow F d} → (j₁ ⟶ j₂) → Z j₂.left j₂.hom → Z j₁.left j₁.hom

Tactic:
j₂

Goal state after:
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
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
⊢ (j₁ ⟶ j₂) → Z j₂.left j₂.hom → Z j₁.left j₁.hom
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
s : Cone (F ⋙ G)
j j₁ : C
⊢ ∀ (X₂ : C) (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : j₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j

Tactic:
j₂

Goal state after:
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
s : Cone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₁ ≫ G.map k₁ = s.π.app j → s.π.app j₂ ≫ G.map k₂ = s.π.app j
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
s : Cone (F ⋙ G)
j j₁ : C
⊢ ∀ (X₂ : C) (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : j₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₂ ≫ G.map k₂ = s.π.app j → s.π.app j₁ ≫ G.map k₁ = s.π.app j

Tactic:
j₂

Goal state after:
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
s : Cone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₂ ≫ G.map k₂ = s.π.app j → s.π.app j₁ ≫ G.map k₁ = s.π.app j
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✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pushout.inl f.op f.op).unop ≫ f.op.unop = (pushout.inr f.op f.op).unop ≫ f.op.unop

Tactic:
← unop_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (f.op ≫ pushout.inl f.op f.op).unop = (pushout.inr f.op f.op).unop ≫ f.op.unop
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✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (f.op ≫ pushout.inl f.op f.op).unop = (pushout.inr f.op f.op).unop ≫ f.op.unop

Tactic:
← unop_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (f.op ≫ pushout.inl f.op f.op).unop = (f.op ≫ pushout.inr f.op f.op).unop
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✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pushout.inl f.op f.op).unop ≫ f.op.unop = (pushout.inr f.op f.op).unop ≫ f.op.unop

Tactic:
rw [← unop_comp, ← unop_comp, pushout.condition]

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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit G H
c : Cone (F ⋙ G)
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
by
    refine ⟨isLimitExtendConeEquiv F _ (isLimitOfReflects H ?_)⟩
    let hc' := (isLimitExtendConeEquiv (G := G ⋙ H) F _).symm hc
    exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_1
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inl f f =
    (pullback.fst f.op f.op).unop ≫ (pushoutIsoUnopPullback f f).inv.op.unop

Tactic:
← unop_comp,

Goal state after:
case refine_1
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inl f f =
    ((pushoutIsoUnopPullback f f).inv.op ≫ pullback.fst f.op f.op).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_2
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.op f.op).unop ≫ (pushoutIsoUnopPullback f f).inv.op.unop

Tactic:
← unop_comp,

Goal state after:
case refine_2
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f =
    ((pushoutIsoUnopPullback f f).inv.op ≫ pullback.snd f.op f.op).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
  rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pullbacks

Tactic:
by
  intro A B q hq
  exact P.pullbacks_mk IsPullback.of_id_fst hq

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso 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], P (algebraMap R T) → P (algebraMap S (S ⊗[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'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := ⋯.equiv
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
⊢ e x = f' x

Tactic:
suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso 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], P (algebraMap R T) → P (algebraMap S (S ⊗[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'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := ⋯.equiv
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
⊢ ↑R ↑e = f'.toLinearMap