awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
        (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
f : N' →ₗ[R] N''
hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')
x_5 : N' ⊗[R] M
hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_5 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)
x : N'
⊢ Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔
    Membership.mem (γ := Set N') (Set.range (ι := PUnit.{v' + 1}) (⇑0 : (a : PUnit.{v' + 1}) → N')) x
have simp_rw : Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x
Tactic: simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ Function.Injective (α := A) (β := A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
have h : Eq (α := A → A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
  (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
    (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R))
Tactic: convert!
    Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : CommSemiring S
inst_6 : Algebra S A
inst_7 : SMulCommClass R S A
inst_8 : Module.Flat R A
hb : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ Eq (α := A → A ⊗[R] B) (⇑includeLeft : (a : A) → A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R))
have h : ∀ (x : A),
  Eq (α := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
    (Function.comp (β := A ⊗[R] R) (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) : (a : A ⊗[R] R) → A ⊗[R] B)
        (⇑(LinearEquiv.symm (_root_.TensorProduct.rid R A)) : (a : A) → A ⊗[R] R) x :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Injective (α := B) (β := A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
have h : Eq (α := B → A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
  (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
    (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B))
Tactic: convert!
    Module.Flat.rTensor_preserves_injective_linearMap (M := B) (Algebra.linearMap R A) ha |>.comp
      (_root_.TensorProduct.lid R B).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Module.Flat R B
ha : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Eq (α := B → A ⊗[R] B) (⇑includeRight : (a : B) → A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
      (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B))
have h : ∀ (x : B),
  Eq (α := A ⊗[R] B) ((includeRight : (a : B) → A ⊗[R] B) x : A ⊗[R] B)
    (Function.comp (β := R ⊗[R] B) (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) : (a : R ⊗[R] B) → A ⊗[R] B)
        (⇑(LinearEquiv.symm (_root_.TensorProduct.lid R B)) : (a : B) → R ⊗[R] B) x :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R M
inst_10 : Module.Flat R Q
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)
have rw : Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
  (⇑(LinearMap.lTensor M g ∘ₗ LinearMap.rTensor Q f) : (a : P ⊗[R] Q) → M ⊗[R] N)
Tactic: rw [← LinearMap.lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_4
Q : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst_9 : Module.Flat R P
inst_10 : Module.Flat R N
hf : Function.Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Function.Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
⊢ Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N) (⇑(map f g) : (a : P ⊗[R] Q) → M ⊗[R] N)
have rw : Function.Injective (α := P ⊗[R] Q) (β := M ⊗[R] N)
  (⇑(LinearMap.rTensor N f ∘ₗ LinearMap.lTensor P g) : (a : P ⊗[R] Q) → M ⊗[R] N)
Tactic: rw [← LinearMap.rTensor_comp_lTensor]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Function.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))
    (⇑(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 _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
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)
    (⇑(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)
  (map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
    (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst_5 : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Eq (α := (ι × κ →₀ R) →ₗ[R] M ⊗[R] N) (Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2)
    (map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))
have h : ∀ (i : ι × κ),
  Eq (α := M ⊗[R] N)
    (((Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i : (a : R) → M ⊗[R] N) 1)
    (((map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
            (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) ∘ₗ
          Finsupp.lsingle i :
        (a : R) → M ⊗[R] N)
      1)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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_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 : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective.{u_6 + 1, u_8 + 1} (α := M₂) (β := N₂) (⇑i : (a : M₂) → N₂)
inst_11 : Module.Flat R M₁
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg LinearMap.id i) : (a : M) → N)
have h : Eq (α := (a : M) → N) (⇑(hf.map hg LinearMap.id i) : (a : M) → N)
  (Function.comp (β := M₁ ⊗[R] N₂) (⇑hg.equiv : (a : M₁ ⊗[R] N₂) → N)
    (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.lTensor M₁ i) : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] N₂)
      (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
Tactic: have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : AddCommMonoid N₁
inst_10 : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective.{u_5 + 1, u_7 + 1} (α := M₁) (β := N₁) (⇑i : (a : M₁) → N₁)
inst_11 : Module.Flat R M₂
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i LinearMap.id) : (a : M) → N)
have h : Eq (α := (a : M) → N) (⇑(hf.map hg i LinearMap.id) : (a : M) → N)
  (Function.comp (β := N₁ ⊗[R] M₂) (⇑hg.equiv : (a : N₁ ⊗[R] M₂) → N)
    (Function.comp (β := M₁ ⊗[R] M₂) (⇑(LinearMap.rTensor M₂ i) : (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] M₂)
      (⇑hf.equiv.symm : (a : M) → M₁ ⊗[R] M₂)))
Tactic: have h : hf.map hg i LinearMap.id = hg.equiv ∘ i.rTensor M₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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₁
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
have 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₂)))
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])
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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₂
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑(hf.map hg i₁ i₂) : (a : M) → N)
have 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₂)))
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])
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S)
have h : 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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
⊢ IsSMulRegular.{u_2, u_4} (R := S) N ((algebraMap R S : (a : R) → S) x : S)
have 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)
Tactic: rwa [hf.map_id_lsmul_eq_lsmul_algebraMap] at h
Cleared hypotheses: h
-- 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)
⊢ IsReduced (C ⊗[R] A)
have by_contra : ∀ (h_contra : ¬IsReduced (C ⊗[R] A)), False
Tactic: by_contra h_contra
-- 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)
⊢ False
have obtain : ∀ (x : C ⊗[R] A) (hx : x ≠ 0 ∧ IsNilpotent x), False
Tactic: obtain ⟨x, hx⟩ := exists_isNilpotent_of_not_isReduced h_contra
-- 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)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
⊢ False
have obtain : ∀ (D : Subalgebra R A) (hD : D.FG ∧ Membership.mem (γ := Subalgebra C (C ⊗[R] A)) (Subalgebra.baseChange C D) x), False
Tactic: obtain ⟨D, hD⟩ := exists_fg_and_mem_baseChange x
-- 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)
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
⊢ False
have 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)
Tactic: have h_inj : Function.Injective
      (Algebra.TensorProduct.map (AlgHom.id C C) D.val) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
-- 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)
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)
⊢ False
have 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
Tactic: obtain ⟨z, rfl⟩ := hD.2
Cleared hypotheses: x, hx, hD
-- 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)
⊢ ¬IsReduced (TensorProduct.{u_1, u_2, u_3} R C ↥D)
have simp_rw : ∃ (x : TensorProduct.{u_1, u_2, u_3} R C ↥D) (_ : IsNilpotent x), ¬x = 0
Tactic: simp_rw [isReduced_iff, not_forall]