-- Mathlib/RingTheory/Kaehler/TensorProduct.lean
lemma tensorKaehlerEquiv_left_inv [Algebra.IsPushout R S A B] :
    ((derivationTensorProduct R S A B).liftKaehlerDifferential.restrictScalars S).comp
    (((map R S A B).restrictScalars R).liftBaseChange S) = LinearMap.id

Proof state:
case H.intro.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x✝ • x ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))) =
    ↑R LinearMap.id

Tactic:
apply TensorProduct.ext'

Result:
case H
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ∀ (x : S) (y : Ω[A⁄R]),
    (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
        (x ⊗ₜ[R] y) =
      (↑R LinearMap.id) (x ⊗ₜ[R] y)

Proof state:
case H.intro.add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A ⊗[R] A
a✝¹ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo x✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo x✝)
a✝ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y✝)
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝))

Tactic:
simp only [map_add, TensorProduct.tmul_add, *]

Result:
no goals

Proof state:
case H.intro
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
y : A ⊗[R] A
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y)

Tactic:
induction y

Result:
case H.intro.zero
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo 0) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo 0)

case H.intro.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ ⊗ₜ[R] y✝))

case H.intro.add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A ⊗[R] A
a✝¹ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo x✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo x✝)
a✝ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y✝)
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝))

Proof state:
case H.intro.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x • x✝ • 1 ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)

Tactic:
rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Result:
case H.intro.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x✝ • x ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)

Proof state:
case H.intro.zero
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo 0) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo 0)

Tactic:
simp only [map_zero, TensorProduct.tmul_zero]

Result:
no goals