awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
inst_11 : Flat R M
⊢ Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
        f))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥f.ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
          (a : ↥f.ker →ₗ[R] N) → M ⊗[R] ↥f.ker →ₗ[S] M ⊗[R] N)
        f.ker.subtype))
have rw : Function.Exact (M := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) (N := M ⊗[R] N) (P := M ⊗[R] P)
  (⇑(((AlgebraTensorModule.lTensor S M :
              (↥f.ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
            (a : ↥f.ker →ₗ[R] N) → M ⊗[R] ↥f.ker →ₗ[S] M ⊗[R] N)
          f.ker.subtype :
        TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
    (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
  (⇑(((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          f :
        M ⊗[R] N →ₗ[S] M ⊗[R] P) :
    (a : M ⊗[R] N) → M ⊗[R] P)
Tactic: rw [← LinearMap.exact_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Flat R M
⊢ Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          f :
        M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          g :
        M ⊗[R] N →ₗ[S] M ⊗[R] P))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(LinearMap.eqLocus f g)) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(LinearMap.eqLocus f g) →ₗ[R] N) →ₗ[R]
              TensorProduct.{u_1, u_3, u_4} R M ↥(LinearMap.eqLocus f g) →ₗ[S] M ⊗[R] N) :
          (a : ↥(LinearMap.eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(LinearMap.eqLocus f g) →ₗ[S] M ⊗[R] N)
        (Submodule.subtype (LinearMap.eqLocus f g))))
have rw : (HSub.hSub (α := M ⊗[R] N →ₗ[S] M ⊗[R] P) (β := M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          f :
        M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          g :
        M ⊗[R] N →ₗ[S] M ⊗[R] P)).ker =
  LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
    (((AlgebraTensorModule.lTensor S M :
          (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
        (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
      (f - g).ker.subtype)
Tactic: rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Flat R M
⊢ (HSub.hSub (α := M ⊗[R] N →ₗ[S] M ⊗[R] P) (β := M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            f :
          M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            g :
          M ⊗[R] N →ₗ[S] M ⊗[R] P)).ker =
    LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype)
have rw : Eq (α := Submodule S (M ⊗[R] N))
  (LinearMap.ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
    (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
        (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (f - g)))
  (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
    (((AlgebraTensorModule.lTensor S M :
          (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
        (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
      (f - g).ker.subtype))
Tactic: rw [← map_sub, ker_lTensor_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Flat R M
rw :
  Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (f - g)))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype))
⊢ (HSub.hSub (α := M ⊗[R] N →ₗ[S] M ⊗[R] P) (β := M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            f :
          M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            g :
          M ⊗[R] N →ₗ[S] M ⊗[R] P)).ker =
    LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype)
have rw₁ : Eq (α := Submodule S (M ⊗[R] N))
  (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
    (((AlgebraTensorModule.lTensor S M :
          (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
        (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
      (f - g).ker.subtype))
  (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
    (((AlgebraTensorModule.lTensor S M :
          (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
        (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
      (f - g).ker.subtype))
Tactic: rw [← map_sub, ker_lTensor_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorKer S M f :
              (a : M ⊗[R] ↥f.ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N)
have zero : Eq (α := M ⊗[R] N)
  (↑((tensorKer S M f :
          (a : M ⊗[R] ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
        0) :
    M ⊗[R] N)
  ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) 0)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
zero :
  Eq (α := M ⊗[R] N)
    (↑((tensorKer S M f :
            (a : M ⊗[R] ↥f.ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          0) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) 0)
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorKer S M f :
              (a : M ⊗[R] ↥f.ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N)
have tmul : ∀ (x : M) (y : ↥f.ker),
  Eq (α := M ⊗[R] N)
    ((↑((tensorKer S M f :
              (a : M ⊗[R] ↥f.ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            (x ⊗ₜ[R] y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
zero :
  Eq (α := M ⊗[R] N)
    (↑((tensorKer S M f :
            (a : M ⊗[R] ↥f.ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          0) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) 0)
tmul :
  ∀ (x : M) (y : ↥f.ker),
    Eq (α := M ⊗[R] N)
      ((↑((tensorKer S M f :
                (a : M ⊗[R] ↥f.ker) →
                  ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
              (x ⊗ₜ[R] y)) :
          M ⊗[R] N) :
        M ⊗[R] N)
      ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorKer S M f :
              (a : M ⊗[R] ↥f.ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N)
have add : ∀ (x y : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker),
  Eq (α := M ⊗[R] N)
      ((↑((tensorKer S M f :
                (a : M ⊗[R] ↥f.ker) →
                  ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
              x) :
          M ⊗[R] N) :
        M ⊗[R] N)
      ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N) →
    Eq (α := M ⊗[R] N)
        ((↑((tensorKer S M f :
                  (a : M ⊗[R] ↥f.ker) →
                    ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
                y) :
            M ⊗[R] N) :
          M ⊗[R] N)
        ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) y : M ⊗[R] N) →
      Eq (α := M ⊗[R] N)
        ((↑((tensorKer S M f :
                  (a : M ⊗[R] ↥f.ker) →
                    ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
                (x + y)) :
            M ⊗[R] N) :
          M ⊗[R] N)
        ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x + y) : M ⊗[R] N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorEqLocus S M f g :
              (a : M ⊗[R] ↥(eqLocus f g)) →
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) x : M ⊗[R] N)
have zero : Eq (α := M ⊗[R] N)
  (↑((tensorEqLocus S M f g :
          (a : M ⊗[R] ↥(eqLocus f g)) →
            ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
        0) :
    M ⊗[R] N)
  ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) 0)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
x : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)
zero :
  Eq (α := M ⊗[R] N)
    (↑((tensorEqLocus S M f g :
            (a : M ⊗[R] ↥(eqLocus f g)) →
              ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                  ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
          0) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) 0)
⊢ Eq (α := M ⊗[R] N)
    ((↑((tensorEqLocus S M f g :
              (a : M ⊗[R] ↥(eqLocus f g)) →
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
            x) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) x : M ⊗[R] N)
have tmul : ∀ (x : M) (y : ↥(eqLocus f g)),
  Eq (α := M ⊗[R] N)
    ((↑((tensorEqLocus S M f g :
              (a : M ⊗[R] ↥(eqLocus f g)) →
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
            (x ⊗ₜ[R] y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
inst_11 : Module.Flat R M
x :
  ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
        f))
⊢ (lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      ((tensorKerInv S M f :
          (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) → M ⊗[R] ↥f.ker)
        x) =
    (↑x : M ⊗[R] N)
have rw : ((((AlgebraTensorModule.lTensor S M : (↥f.ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
            (a : ↥f.ker →ₗ[R] N) → M ⊗[R] ↥f.ker →ₗ[S] M ⊗[R] N)
          f.ker.subtype :
        TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
      (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
    ((tensorKerInv S M f :
        (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) → M ⊗[R] ↥f.ker)
      x) =
  (↑x : M ⊗[R] N)
Tactic: rw [← AlgebraTensorModule.coe_lTensor (A := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
x :
  ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          f :
        M ⊗[R] N →ₗ[S] M ⊗[R] P)
      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          g :
        M ⊗[R] N →ₗ[S] M ⊗[R] P))
⊢ (lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      ((tensorEqLocusInv S M f g :
          (a :
              ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                  ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g))) →
            M ⊗[R] ↥(eqLocus f g))
        x) =
    (↑x : M ⊗[R] N)
have rw : ((((AlgebraTensorModule.lTensor S M :
              (↥(eqLocus f g) →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
            (a : ↥(eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(eqLocus f g) →ₗ[S] M ⊗[R] N)
          (Submodule.subtype (eqLocus f g)) :
        TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
      (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
    ((tensorEqLocusInv S M f g :
        (a :
            ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g))) →
          M ⊗[R] ↥(eqLocus f g))
      x) =
  (↑x : M ⊗[R] N)
Tactic: rw [← AlgebraTensorModule.coe_lTensor (A := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
⊢ Eq (α :=
    ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            f)) →ₗ[S]
      ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            f)))
    (tensorKer S M f ∘ₗ tensorKerInv S M f) id
have h : ∀
  (x :
    ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
          f))),
  Eq (α := M ⊗[R] N)
    (↑((tensorKer S M f ∘ₗ tensorKerInv S M f :
            (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          x) :
      M ⊗[R] N)
    (↑((id :
            (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          x) :
      M ⊗[R] N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (tensorKerInv S M f ∘ₗ tensorKer S M f :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (id : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
have a : ∀ (m : M) (x : ↥f.ker),
  Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (((((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f) :
                  M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (((((AlgebraTensorModule.curry id : M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
Tactic: ext m x