awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₁
inst_14 : Module.Flat R N₂
x : M
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) 0 : N)
    (Function.comp (α := M) (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        0 :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₁
inst_14 : Module.Flat R N₂
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq.{u_3 + 1} (α := N)
      ((hf.map hg i₁ i₂ : (a : M) → N) ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) : N)
      (Function.comp (α := M) (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
          (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
              (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂) :
            M → N₁ ⊗[R] N₂)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₁
inst_14 : Module.Flat R N₂
x x_1 x_2 : M
hx :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) x_1 : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_1 :
      N)
hy :
  Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) x_2 : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        x_2 :
      N)
⊢ Eq.{u_3 + 1} (α := N) ((hf.map hg i₁ i₂ : (a : M) → N) (x_1 + x_2) : N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
        (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂))
        (x_1 + x_2) :
      N)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₁
inst_14 : Module.Flat R N₂
⊢ Eq (α := (a : M) → N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))

Tactic:
have h : hf.map hg i₁ i₂ = hg.equiv ∘ TensorProduct.map i₁ i₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : Module R N₁
inst_12 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i₁ : (a : M₁) → N₁)
h₂ : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i₂ : (a : M₂) → N₂)
inst_13 : Module.Flat R M₁
inst_14 : Module.Flat R N₂
h :
  Eq (α := (a : M) → N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
    (Function.comp (β := N₁ ⊗[R] N₂) (⇑hg.equiv : (a : N₁ ⊗[R] N₂) → N)
      (Function.comp (β := M₁ ⊗[R] M₂) (⇑(TensorProduct.map i₁ i₂) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)

Tactic:
simpa [h] using map_injective_of_flat_flat' i₁ i₂ h₁ h₂

Premises used: TensorProduct.map_injective_of_flat_flat'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
reg : IsSMulRegular M x
⊢ Function.Injective (α := N) (β := N)
    (⇑(IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x)) : (a : N) → N)

Tactic:
have h := hf.map_id_injective_of_flat_left hf (LinearMap.lsmul R M x) reg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
reg : IsSMulRegular M x
h :
  Function.Injective (α := N) (β := N)
    (⇑(IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) x)) : (a : N) → N)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Function.Injective.{u_4 + 1, u_4 + 1} (α := N) (β := N)
        (⇑((↑R :
                {S : Type u_2} →
                  {M M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_10 : Semiring S] →
                        [inst_11 : AddCommMonoid M] →
                          [inst_12 : AddCommMonoid M₂] →
                            [inst_13 : Module R M] →
                              [inst_14 : Module R M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S) ((LinearMap.lsmul S N : (a : S) → N →ₗ[S] N) ((algebraMap R S : (a : R) → S) x))) :
          (a : N) → N)),
    IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S)
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S)

Tactic:
rwa [hf.map_id_lsmul_eq_lsmul_algebraMap] at h

Premises used: IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
x : R
reg : IsSMulRegular R x
⊢ IsSMulRegular (R := S) S ((algebraMap R S : (a : R) → S) x : S)

Tactic:
reg.of_flat_of_isBaseChange (IsBaseChange.linearMap R S)

Premises used: IsSMulRegular.of_flat_of_isBaseChange, IsBaseChange.linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
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)
by_contra : ∀ (h_contra : ¬IsReduced (C ⊗[R] A)), False
⊢ IsReduced (C ⊗[R] A)

Tactic:
by_contra h_contra
-- Module: Mathlib.RingTheory.Flat.Basic
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)
obtain : ∀ (x : C ⊗[R] A) (hx : x ≠ 0 ∧ IsNilpotent x), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_isNilpotent_of_not_isReduced h_contra

Premises used: exists_isNilpotent_of_not_isReduced
-- Module: Mathlib.RingTheory.Flat.Basic
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)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
obtain :
  ∀ (D : Subalgebra R A) (hD : D.FG ∧ Membership.mem (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D) x),
    False
⊢ False

Tactic:
obtain ⟨D, hD⟩ := exists_fg_and_mem_baseChange x

Premises used: exists_fg_and_mem_baseChange
-- Module: Mathlib.RingTheory.Flat.Basic
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)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ Membership.mem (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D) x
⊢ 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)

Tactic:
have h_inj : Function.Injective
      (Algebra.TensorProduct.map (AlgHom.id C C) D.val) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Basic
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)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ Membership.mem (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D) x
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)
obtain :
  ∀ (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
⊢ False

Tactic:
obtain ⟨z, rfl⟩ := hD.2

Premises used: And.right, rfl
-- Module: Mathlib.RingTheory.Flat.Basic
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)
simp_rw : ∃ (x : TensorProduct.{u_1, u_2, u_3} R C ↥D) (_ : IsNilpotent x), ¬x = 0
⊢ ¬IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥D)

Tactic:
simp_rw [isReduced_iff, not_forall]

Premises used: isReduced_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.Flat.Basic
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)
⊢ ∃ (x : TensorProduct.{u_1, u_2, u_3} R C ↥D) (_ : IsNilpotent x), ¬x = 0

Tactic:
exact ⟨z, (IsNilpotent.map_iff h_inj).mp hx.right, (by simpa [·] using hx.1)⟩
-- Module: Mathlib.RingTheory.Flat.Basic
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)
⊢ ¬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)⟩
-- Module: Mathlib.RingTheory.Flat.Basic
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)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ 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
⊢ False

Tactic:
tauto
-- Module: Mathlib.RingTheory.Flat.CategoryTheory
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
inst_1 : Flat R (↑M : Type u)
C : ShortComplex (ModuleCat R)
hC : C.Exact
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))
⊢ ShortComplex.Exact (C.map (tensorLeft M))

Tactic:
rw [moduleCat_exact_iff_function_exact] at hC ⊢

Premises used: CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact