-- Mathlib/AlgebraicGeometry/Pullbacks.lean
lemma diagonal_Spec_map :
    pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))) =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).toRingHom) ≫
        (pullbackSpecIso R S S).inv

Proof state:
case h₀.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)

Tactic:
simp

Result:
no goals

Proof state:
case h₁.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (1 ⊗ₜ[R] x)

Tactic:
simp

Result:
no goals

Proof state:
case h₀.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))) x

Tactic:
show x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1)

Result:
case h₀.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) =
    Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv

Tactic:
ext1 <;> simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
  AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]

Result:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))

case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Proof state:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Tactic:
congr 1

Result:
case h₁.e_f
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom ↑includeRight ≫ ofHom ↑(lmul' R)

Proof state:
case h₀.e_f
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R)

Tactic:
ext x

Result:
case h₀.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))) x

Proof state:
case h₁.e_f
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom ↑includeRight ≫ ofHom ↑(lmul' R)

Tactic:
ext x

Result:
case h₁.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))) x

Proof state:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))

Tactic:
congr 1

Result:
case h₀.e_f
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R)

Proof state:
case h₁.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ (Hom.hom (𝟙 (of S))) x = (Hom.hom (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))) x

Tactic:
show x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x)

Result:
case h₁.e_f.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (1 ⊗ₜ[R] x)