awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
rwa : ∀ (ha : K.subtype.range ≤ a.ker), K ≤ a.ker
⊢ K ≤ a.ker
have rwa₁ : ∀ (ha : K ≤ a.ker), K ≤ a.ker
Tactic: rwa [← range_le_ker_iff, Submodule.range_subtype] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
have h : h₁ =
  y ∘ₗ
    Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ := RingHom.id R)
        a sorry ∘ₗ
      (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)
Tactic: use k, (K.liftQ a (by rwa [← range_le_ker_iff, Submodule.range_subtype] at ha)) ∘ₗ ϕ, y
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ h₁ =
    y ∘ₗ
      Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
          RingHom.id R) a ⋯ ∘ₗ
        (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)
have h : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) =
  (y ∘ₗ
      Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
          RingHom.id R) a sorry ∘ₗ
        (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
    (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)
Tactic: apply (cancel_right ϕ.symm.surjective).mp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) =
    (y ∘ₗ
        Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
            RingHom.id R) a ⋯ ∘ₗ
          (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
      (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)
have h : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ K.mkQ =
  ((y ∘ₗ
        Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
            RingHom.id R) a sorry ∘ₗ
          (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
      (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ
    K.mkQ
Tactic: apply (cancel_right K.mkQ_surjective).mp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
⊢ FaithfullyFlat A B
have refine : ∀ (m : Ideal A) (hm : m.IsMaximal), HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
Tactic: refine ⟨fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
have obtain : ∀ (m' : PrimeSpectrum B)
  (hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := sorry : PrimeSpectrum A }),
  HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
Tactic: obtain ⟨m', hm'⟩ := h ⟨m, hm.isPrime⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
⊢ m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
have rw : m = PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A B) m')
Tactic: rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
rw : m = PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A B) m')
⊢ m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
have rw₁ : m = { asIdeal := m, isPrime := sorry }.asIdeal
Tactic: rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
have this : m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
Tactic: have : m = Ideal.comap (algebraMap A B) m'.asIdeal := by
    rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
this : m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
have rw : Ne.{u_2 + 1} (α := Submodule A B)
  (Submodule.restrictScalars A
    (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal)))
  ⊤
Tactic: rw [Ideal.smul_top_eq_map, this]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
⊢ FaithfullyFlat A B
have refine : ∀ (m : Ideal A) (hm : m.IsMaximal), HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
Tactic: refine ⟨fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
have rw : Ne.{u_2 + 1} (α := Submodule A B)
  (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤
Tactic: rw [Ideal.smul_top_eq_map, IsLocalRing.eq_maximalIdeal hm]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt :
  Eq.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤
⊢ False
have this : LE.le (α := Submodule A B)
  (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A)))
  (Submodule.restrictScalars A (IsLocalRing.maximalIdeal B))
Tactic: have : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
      Submodule.restrictScalars A (IsLocalRing.maximalIdeal B) :=
    ((IsLocalRing.local_hom_TFAE (algebraMap A B)).out 0 2).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt :
  Eq.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤
this :
  LE.le (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A)))
    (Submodule.restrictScalars A (IsLocalRing.maximalIdeal B))
⊢ False
have this₁ : Eq (α := Submodule B B) (IsLocalRing.maximalIdeal B) ⊤
Tactic: rw [eqt, top_le_iff, Submodule.restrictScalars_eq_top_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
inst_4 : Flat A B
inst_5 : Algebra.IsIntegral A B
inst_6 : FaithfulSMul A B
⊢ FaithfullyFlat A B
have refine : ∀ (P : PrimeSpectrum A), ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P
Tactic: refine Module.FaithfullyFlat.of_comap_surjective fun P ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
inst_4 : Flat A B
inst_5 : Algebra.IsIntegral A B
inst_6 : FaithfulSMul A B
P : PrimeSpectrum A
⊢ ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P
have obtain : ∀ (P_1 : Ideal B) (hP₁ : P_1.IsPrime) (hP₂ : Ideal.comap (F := A →+* B) (algebraMap A B) P_1 = P.asIdeal),
  ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P
Tactic: obtain ⟨P, hP₁, hP₂⟩ := Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain P.1 (S := B)
    (by simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective A B)])
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module A M
⊢ Function.Injective (α := M) (β := B ⊗[A] M)
    (⇑((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1) : (a : M) → B ⊗[A] M)
have rw : Function.Injective (α := B ⊗[A] M) (β := B ⊗[A] (B ⊗[A] M))
  (⇑(lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1)) : (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
Tactic: rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module A M
⊢ Eq (α := B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) (lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1))
    ((↑(LinearEquiv.symm (leftComm A B B M)) : B ⊗[A] (B ⊗[A] M) →ₗ[A] B ⊗[A] (B ⊗[A] M)) ∘ₗ
      (TensorProduct.mk A B (B ⊗[A] M) : (a : B) → B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) 1)
have H : ∀ (x : B) (y : M),
  Eq (α := B ⊗[A] (B ⊗[A] M))
    ((lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1) : (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
        (x ⊗ₜ[A] y) :
      B ⊗[A] (B ⊗[A] M))
    (((↑(LinearEquiv.symm (leftComm A B B M)) : B ⊗[A] (B ⊗[A] M) →ₗ[A] B ⊗[A] (B ⊗[A] M)) ∘ₗ
            (TensorProduct.mk A B (B ⊗[A] M) : (a : B) → B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) 1 :
          (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
        (x ⊗ₜ[A] y) :
      B ⊗[A] (B ⊗[A] M))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module A M
⊢ Function.Injective (α := B ⊗[A] M) (β := B ⊗[A] (B ⊗[A] M))
    (⇑(lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1)) : (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
have this : Eq (α := B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) (lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1))
  ((↑(LinearEquiv.symm (leftComm A B B M)) : B ⊗[A] (B ⊗[A] M) →ₗ[A] B ⊗[A] (B ⊗[A] M)) ∘ₗ
    (TensorProduct.mk A B (B ⊗[A] M) : (a : B) → B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) 1)
Tactic: have : (lTensor B <| TensorProduct.mk A B M 1) =
      (TensorProduct.leftComm A B B M).symm.comp (TensorProduct.mk A B (B ⊗[A] M) 1) := by
    apply TensorProduct.ext'
    intro x y
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module A M
this :
  Eq (α := B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) (lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1))
    ((↑(LinearEquiv.symm (leftComm A B B M)) : B ⊗[A] (B ⊗[A] M) →ₗ[A] B ⊗[A] (B ⊗[A] M)) ∘ₗ
      (TensorProduct.mk A B (B ⊗[A] M) : (a : B) → B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) 1)
⊢ Function.Injective (α := B ⊗[A] M) (β := B ⊗[A] (B ⊗[A] M))
    (⇑(lTensor B ((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1)) : (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
have rw : Function.Injective (α := B ⊗[A] M) (β := B ⊗[A] (B ⊗[A] M))
  (⇑((TensorProduct.mk A B (B ⊗[A] M) : (a : B) → B ⊗[A] M →ₗ[A] B ⊗[A] (B ⊗[A] M)) 1) :
    (a : B ⊗[A] M) → B ⊗[A] (B ⊗[A] M))
Tactic: rw [this, coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
⊢ FaithfulSMul A B
have eq_of_smul_eq_smul : ∀ {m₁ m₂ : A}, (∀ (a : B), m₁ • a = m₂ • a) → m₁ = m₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ a₁ = a₂
have eq_of_smul_eq_smul : Eq (α := B ⊗[A] A) (((TensorProduct.mk A B A : (a : B) → A →ₗ[A] B ⊗[A] A) 1 : (a : A) → B ⊗[A] A) a₁ : B ⊗[A] A)
  (((TensorProduct.mk A B A : (a : B) → A →ₗ[A] B ⊗[A] A) 1 : (a : A) → B ⊗[A] A) a₂ : B ⊗[A] A)
Tactic: apply Module.FaithfullyFlat.tensorProduct_mk_injective (A := A) (B := B) A
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : FaithfullyFlat A B
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ Eq (α := B ⊗[A] A) (1 ⊗ₜ[A] a₁) (1 ⊗ₜ[A] a₂)
have eq_of_smul_eq_smul : Eq (α := B ⊗[A] A) (1 ⊗ₜ[A] (a₁ * 1)) (1 ⊗ₜ[A] (a₂ * 1))
Tactic: rw [← mul_one a₁, ← mul_one a₂]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
I : Ideal A
⊢ comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I) = I
have refine : comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I) ≤ I
Tactic: refine le_antisymm ?_ le_comap_map
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
I : Ideal A
⊢ comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I) ≤ I
have inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
  HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
  (⇑((↑A :
            {S : Type u_2} →
              {M : Type (max u_1 u_2)} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_4 : Semiring S] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : AddCommMonoid M₂] →
                          [inst_7 : Module A M] →
                            [inst_8 : Module A M₂] →
                              [inst_9 : Module S M] →
                                [inst_10 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
        (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) :
    (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
Tactic: have inj : Function.Injective
      ((quotIdealMapEquivTensorQuot B I).symm.toLinearMap.restrictScalars _ ∘ₗ
        TensorProduct.mk A B (A ⧸ I) 1) := by
    rw [LinearMap.coe_comp, AlgEquiv.toLinearMap, ← LinearEquiv.restrictScalars_toLinearMap]
    exact (LinearEquiv.injective _).comp <|
      Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
I : Ideal A
inj :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (⇑((↑A :
              {S : Type u_2} →
                {M : Type (max u_1 u_2)} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_4 : Semiring S] →
                        [inst_5 : AddCommMonoid M] →
                          [inst_6 : AddCommMonoid M₂] →
                            [inst_7 : Module A M] →
                              [inst_8 : Module A M₂] →
                                [inst_9 : Module S M] →
                                  [inst_10 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
          (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) :
      (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
x : A
hx :
  Membership.mem (γ := Submodule A A) (comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I)) x
⊢ x ∈ I
have hx₁ : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (map (F := A →+* B) (algebraMap A B) I)
  ((algebraMap A B : (a : A) → B) x : B)
Tactic: rw [Ideal.mem_comap] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
I : Ideal A
inj :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (⇑((↑A :
              {S : Type u_2} →
                {M : Type (max u_1 u_2)} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_4 : Semiring S] →
                        [inst_5 : AddCommMonoid M] →
                          [inst_6 : AddCommMonoid M₂] →
                            [inst_7 : Module A M] →
                              [inst_8 : Module A M₂] →
                                [inst_9 : Module S M] →
                                  [inst_10 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (AlgEquiv.toLinearMap (AlgEquiv.symm (quotIdealMapEquivTensorQuot B I))) ∘ₗ
          (TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) :
      (a : A ⧸ I) → B ⧸ map (algebraMap A B) I)
x : A
hx :
  Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (map (F := A →+* B) (algebraMap A B) I)
    ((algebraMap A B : (a : A) → B) x : B)
⊢ x ∈ I
have rw : ∀
  (hx :
    Eq.{u_2 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
      ((Quotient.mk (map (F := A →+* B) (algebraMap A B) I) : (a : B) → B ⧸ map (algebraMap A B) I)
          ((algebraMap A B : (a : A) → B) x) :
        HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
      (0 : HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))),
  Eq (α := A ⧸ I) ((Quotient.mk I : (a : A) → A ⧸ I) x : A ⧸ I) (0 : A ⧸ I)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.FaithfullyFlat A B
p : Ideal A
inst_4 : p.IsPrime
⊢ ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
have obtain : ∀ (P : Ideal B),
  P.IsPrime → ∀ (hP : comap (F := A →+* B) (algebraMap A B) P = p), ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p
Tactic: obtain ⟨P, _, hP⟩ := (Ideal.comap_map_eq_self_iff_of_isPrime p).mp <|
    p.comap_map_eq_self_of_faithfullyFlat (B := B)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ FaithfullyFlat R M ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
have rw : (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) ↔
  Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
Tactic: rw [faithfullyFlat_iff]