awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
Goal:
R : Type u_1
C : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring C
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R C
inst_5 : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj :
  Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R C ↥D) (β := C ⊗[R] A)
    (⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
      (a : C ⊗[R] ↥D) → C ⊗[R] A)
z : TensorProduct.{u_1, u_2, u_3} R C ↥D
hx :
  Ne (α := C ⊗[R] A)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
      (0 : C ⊗[R] A) ∧
    IsNilpotent (R := C ⊗[R] A)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
hD :
  D.FG ∧
    Membership.mem (α := C ⊗[R] A) (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
⊢ False
have h_notReduced : ¬IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥D)
Tactic: have h_notReduced : ¬IsReduced (C ⊗[R] D) := by
    simp_rw [isReduced_iff, not_forall]
    exact ⟨z, (IsNilpotent.map_iff h_inj).mp hx.right, (by simpa [·] using hx.1)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
C : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring C
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R C
inst_5 : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj :
  Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R C ↥D) (β := C ⊗[R] A)
    (⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
      (a : C ⊗[R] ↥D) → C ⊗[R] A)
z : TensorProduct.{u_1, u_2, u_3} R C ↥D
hx :
  Ne (α := C ⊗[R] A)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
      (0 : C ⊗[R] A) ∧
    IsNilpotent (R := C ⊗[R] A)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
hD :
  D.FG ∧
    Membership.mem (α := C ⊗[R] A) (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A)
h_notReduced : ¬IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥D)
⊢ False
have tauto : Ne (α := C ⊗[R] A)
    ((AlgHom.toRingHom
            (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
          (a : C ⊗[R] ↥D) → C ⊗[R] A)
        z :
      C ⊗[R] A)
    (0 : C ⊗[R] A) →
  IsNilpotent (R := C ⊗[R] A)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id C C) D.val : TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
            (a : C ⊗[R] ↥D) → C ⊗[R] A)
          z :
        C ⊗[R] A) →
    D.FG →
      Membership.mem (α := C ⊗[R] A) (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D)
          ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id C C) D.val :
                    TensorProduct.{u_1, u_2, u_3} R C ↥D →ₐ[C] C ⊗[R] A) :
                (a : C ⊗[R] ↥D) → C ⊗[R] A)
              z :
            C ⊗[R] A) →
        False
Tactic: tauto
Cleared hypotheses: hx, hD
-- Lean 4 proof step from Mathlib.RingTheory.Flat.CategoryTheory (goal)
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ ShortComplex.Exact (C.map (tensorLeft M))
have rw : ∀
  (hC :
    Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) C.f) :
        (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) C.g) :
        (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))),
  Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorLeft M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorLeft M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorLeft M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorLeft M))) (ShortComplex.f (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₁ : Type u)) → (↑(C.map (tensorLeft M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorLeft M))) (ShortComplex.g (C.map (tensorLeft M)))) :
      (a : (↑(C.map (tensorLeft M)).X₂ : Type u)) → (↑(C.map (tensorLeft M)).X₃ : Type u))
Tactic: rw [moduleCat_exact_iff_function_exact] at hC ⊢
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.RingTheory.Flat.CategoryTheory (goal)
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ ShortComplex.Exact (C.map (tensorRight M))
have rw : ∀
  (hC :
    Function.Exact (M := (↑C.X₁ : Type u)) (N := (↑C.X₂ : Type u)) (P := (↑C.X₃ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) C.f) :
        (a : (↑C.X₁ : Type u)) → (↑C.X₂ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) C.g) :
        (a : (↑C.X₂ : Type u)) → (↑C.X₃ : Type u))),
  Function.Exact (M := (↑(ShortComplex.X₁ (C.map (tensorRight M))) : Type u)) (N :=
    (↑(ShortComplex.X₂ (C.map (tensorRight M))) : Type u)) (P := (↑(ShortComplex.X₃ (C.map (tensorRight M))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₁ (C.map (tensorRight M))) (ShortComplex.f (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₁ : Type u)) → (↑(C.map (tensorRight M)).X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ShortComplex.X₂ (C.map (tensorRight M))) (ShortComplex.g (C.map (tensorRight M)))) :
      (a : (↑(C.map (tensorRight M)).X₂ : Type u)) → (↑(C.map (tensorRight M)).X₃ : Type u))
Tactic: rw [moduleCat_exact_iff_function_exact] at hC ⊢
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.RingTheory.Flat.CategoryTheory (goal)
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
⊢ Flat R (↑M : Type u) ↔ PreservesFiniteLimits (tensorLeft M)
have rw : PreservesFiniteLimits (tensorLeft M) ∧ PreservesFiniteColimits (tensorLeft M) ↔ PreservesFiniteLimits (tensorLeft M)
Tactic: rw [Module.Flat.iff_lTensor_preserves_shortComplex_exact,
    ((Functor.exact_tfae <| tensorLeft M).out 1 3 :)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.CategoryTheory (goal)
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
h : PreservesFiniteLimits (tensorRight M)
⊢ Flat R (↑M : Type u)
have rw : PreservesFiniteLimits (tensorLeft M)
Tactic: rw [iff_preservesFiniteLimits_tensorLeft]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
⊢ Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)
have refine : Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
  (comp (β := M ⊗[R] N)
    (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
    (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
Tactic: refine .of_comp (f := TensorProduct.mk R K _ 1) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₁ : Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
  (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
    (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
Tactic: have H₁ := TensorProduct.map_injective_of_flat_flat (f.baseChange K) (g.baseChange K)
    (Module.Flat.lTensor_preserves_injective_linearMap f hf)
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₂ : Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
  (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
        K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
    (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
Tactic: have H₂ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₃ : Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
  (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
    (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
Tactic: have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₄ : Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
  (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
    (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
Tactic: have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₅ : Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
  (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
    (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
Tactic: have H₅ := (AlgebraTensorModule.assoc R R K K M N).injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₆ : Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
  (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))
Tactic: have H₆ := Module.Flat.rTensor_preserves_injective_linearMap (M := P ⊗[R] Q)
    (Algebra.linearMap R K) (FaithfulSMul.algebraMap_injective R K)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
H₆ :
  Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
    (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))
⊢ Injective (α := P ⊗[R] Q) (β := K ⊗[R] (M ⊗[R] N))
    (comp (β := M ⊗[R] N)
      (⇑((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1) : (a : M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
      (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N))
have H₇ : Injective (α := P ⊗[R] Q) (β := R ⊗[R] (P ⊗[R] Q))
  (⇑(LinearEquiv.symm (TensorProduct.lid R (P ⊗[R] Q))) : (a : P ⊗[R] Q) → R ⊗[R] (P ⊗[R] Q))
Tactic: have H₇ := (TensorProduct.lid R (P ⊗[R] Q)).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Injective (α := ι × κ →₀ R) (β := M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
have h : Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
  (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
  (Function.comp (β := (ι →₀ R) ⊗[R] (κ →₀ R))
    (⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) :
      (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → M ⊗[R] N)
    (⇑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)))
Tactic: convert!
    (TensorProduct.map_injective_of_flat_flat_of_isDomain _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Domain (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
    (⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
          (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) :
      (a : ι × κ →₀ R) → M ⊗[R] N)
have h : Eq (α := (ι × κ →₀ R) →ₗ[R] M ⊗[R] N) (Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2)
  (TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
    (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))
Tactic: congr!