-- Mathlib/RingTheory/Flat/Equalizer.lean
@[simp]
private lemma AlgHom.coe_tensorEqualizerAux (x : T ⊗[R] AlgHom.equalizer f g) :
    (AlgHom.tensorEqualizerAux S T f g x : T ⊗[R] A) =
      Algebra.TensorProduct.map (AlgHom.id S T) (AlgHom.equalizer f g).val x

Proof state:
case add
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
hx : ↑((AlgHom.tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) x
hy : ↑((AlgHom.tensorEqualizerAux S T f g) y) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) y
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x + y)) =
    (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x + y)

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
case tmul
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x : T
y : ↥(equalizer f g)
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x ⊗ₜ[R] y)) =
    (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x ⊗ₜ[R] y)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) 0) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x : T ⊗[R] ↥(equalizer f g)
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) x

Tactic:
induction' x with x y x y hx hy

Result:
case zero
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) 0) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) 0

case tmul
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x : T
y : ↥(equalizer f g)
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x ⊗ₜ[R] y)) =
    (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x ⊗ₜ[R] y)

case add
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(equalizer f g)
hx : ↑((AlgHom.tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) x
hy : ↑((AlgHom.tensorEqualizerAux S T f g) y) = (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) y
⊢ ↑((AlgHom.tensorEqualizerAux S T f g) (x + y)) =
    (Algebra.TensorProduct.map (AlgHom.id S T) (equalizer f g).val) (x + y)