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

Goal state before:
pp: case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
·

Goal state after:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
·

Goal state after:
case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
⊢ T.δ.app X ≫ i.hom.app (T.obj X) ≫ F.map (T.δ.app X) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))

Tactic:
← i.hom.naturality_assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
⊢ T.δ.app X ≫
      T.map (T.δ.app X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (i.hom.app (T.obj X)) ≫ F.map (F.map (i.hom.app X)) =
    T.δ.app X ≫
      T.δ.app (T.obj X) ≫ i.hom.app (T.obj (T.obj X)) ≫ F.map (T.map (i.hom.app X)) ≫ F.map (i.hom.app (F.obj X))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (↑(b * b') • a)) = g (b' • a)

pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')

Tactic:
·

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (↑(b * b') • a)) = g (b' • a)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')

Tactic:
·

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.e_6
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ ∃ u, u • s • m = u • 1 • ↑s • m

Tactic:
refine ⟨1, ?_⟩

Goal state after:
case h.e_6
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ 1 • s • m = 1 • 1 • ↑s • m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case W
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ CommRingCat

pp: case inl
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of A ⟶ ?W

pp: case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ ?W

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) ≫ ?inl = ofHom (algebraMap R B) ≫ ?inr

Tactic:
·

Goal state after:
case W
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ CommRingCat
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case inl
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of A ⟶ of (A ⊗[R] B)

pp: case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)

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) ≫ ?inl = ofHom (algebraMap R B) ≫ ?inr

Tactic:
·

Goal state after:
case inl
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of A ⟶ of (A ⊗[R] B)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)

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) ≫ ?inr

Tactic:
·

Goal state after:
case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)
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:
·

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
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom
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
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r = (algebraMap R (A ⊗[R] B)) r

pp: 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)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
·

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
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r = (algebraMap R (A ⊗[R] B)) r
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
r : ↑(of R)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
·

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
r : ↑(of R)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (↑(b * b') • a) = ↑b • f (b' • a)

pp: case e_a
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑(b * b') • f a' = ↑b' • f (b • a')

Tactic:
·

Goal state after:
case e_a
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (↑(b * b') • a) = ↑b • f (b' • a)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑(b * b') • f a' = ↑b' • f (b • a')

Tactic:
·

Goal state after:
case e_a
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑(b * b') • f a' = ↑b' • f (b • a')
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:
·

Goal state after:
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
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.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.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inr

pp: case property.right.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 := ⋯
⊢ ∀ {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:
·

Goal state after:
case property.right.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.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inr
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: case h₀
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.fst y.hom f = Hom.left v ≫ pullback.fst y.hom f

pp: case h₁
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.snd y.hom f = Hom.left v ≫ pullback.snd y.hom f

Tactic:
·

Goal state after:
case h₀
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.fst y.hom f = Hom.left v ≫ pullback.fst y.hom f
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
·

Goal state after:
case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: case h₁
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.snd y.hom f = Hom.left v ≫ pullback.snd y.hom f

Tactic:
·

Goal state after:
case h₁
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✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.snd y.hom f = Hom.left v ≫ pullback.snd y.hom f
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
·

Goal state after:
case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: case h₀
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 : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.inl x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inl x.hom f ≫ Hom.right u

pp: case h₁
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 : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.inr x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inr x.hom f ≫ Hom.right u

Tactic:
·

Goal state after:
case h₀
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 : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.inl x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inl x.hom f ≫ Hom.right u
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: case h₁
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 : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.inr x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inr x.hom f ≫ Hom.right u

Tactic:
·

Goal state after:
case h₁
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 : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.inr x.hom f ≫ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = pushout.inr x.hom f ≫ Hom.right u
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
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
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).left =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).left

pp: case h₂
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
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).right =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).right

Tactic:
·

Goal state after:
case h₁
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
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).left =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).left