awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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))
⊢ Eq (α := Submodule B B) (IsLocalRing.maximalIdeal B) ⊤

Tactic:
rw [eqt, top_le_iff, Submodule.restrictScalars_eq_top_iff] at this

Premises used: top_le_iff, Submodule.restrictScalars_eq_top_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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 : Eq (α := Submodule B B) (IsLocalRing.maximalIdeal B) ⊤
⊢ False

Tactic:
Ideal.IsPrime.ne_top' this

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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 : Eq (α := Submodule B B) (IsLocalRing.maximalIdeal B) ⊤
⊢ False

Tactic:
exact Ideal.IsPrime.ne_top' this

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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

Tactic:
Module.FaithfullyFlat.of_comap_surjective fun P ↦ ?_

Premises used: Module.FaithfullyFlat.of_comap_surjective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
refine : ∀ (P : PrimeSpectrum A), ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P
⊢ FaithfullyFlat A B

Tactic:
refine Module.FaithfullyFlat.of_comap_surjective fun P ↦ ?_

Premises used: Module.FaithfullyFlat.of_comap_surjective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ RingHom.ker (F := A →+* B) (algebraMap A B) ≤ P.asIdeal

Tactic:
simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective A B)]

Premises used: RingHom.injective_iff_ker_eq_bot, FaithfulSMul.algebraMap_injective, Iff.mp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
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
⊢ ∃ (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)])

Premises used: Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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_1 : PrimeSpectrum A
P : Ideal B
hP₁ : P.IsPrime
hP₂ : Ideal.comap (F := A →+* B) (algebraMap A B) P = P_1.asIdeal
⊢ ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P_1

Tactic:
⟨⟨P, hP₁⟩, PrimeSpectrum.ext_iff.mpr hP₂⟩

Premises used: Iff.mpr, PrimeSpectrum.mk, PrimeSpectrum.ext_iff, Exists.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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_1 : PrimeSpectrum A
P : Ideal B
hP₁ : P.IsPrime
hP₂ : Ideal.comap (F := A →+* B) (algebraMap A B) P = P_1.asIdeal
⊢ ∃ (a : PrimeSpectrum B), PrimeSpectrum.comap (algebraMap A B) a = P_1

Tactic:
exact ⟨⟨P, hP₁⟩, PrimeSpectrum.ext_iff.mpr hP₂⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
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))
⊢ Function.Injective (α := M) (β := B ⊗[A] M)
    (⇑((TensorProduct.mk A B M : (a : B) → M →ₗ[A] B ⊗[A] M) 1) : (a : M) → B ⊗[A] M)

Tactic:
rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]

Premises used: Module.FaithfullyFlat.lTensor_injective_iff_injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
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))
⊢ 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:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
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:
simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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)

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
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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)
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))
⊢ 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 [this, coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective]

Premises used: EmbeddingLike.comp_injective, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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))
    (⇑((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:
Algebra.TensorProduct.mk_one_injective_of_isScalarTower _

Premises used: Algebra.TensorProduct.mk_one_injective_of_isScalarTower
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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))
    (⇑((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:
exact Algebra.TensorProduct.mk_one_injective_of_isScalarTower _

Premises used: Algebra.TensorProduct.mk_one_injective_of_isScalarTower
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
eq_of_smul_eq_smul : ∀ {m₁ m₂ : A}, (∀ (a : B), m₁ • a = m₂ • a) → m₁ = m₂
⊢ FaithfulSMul A B

Tactic:
constructor
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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_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)
⊢ a₁ = a₂

Tactic:
apply Module.FaithfullyFlat.tensorProduct_mk_injective (A := A) (B := B) A

Premises used: Module.FaithfullyFlat.tensorProduct_mk_injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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_of_smul_eq_smul : Eq (α := B ⊗[A] A) (1 ⊗ₜ[A] (a₁ * 1)) (1 ⊗ₜ[A] (a₂ * 1))
⊢ Eq (α := B ⊗[A] A) (1 ⊗ₜ[A] a₁) (1 ⊗ₜ[A] a₂)

Tactic:
rw [← mul_one a₁, ← mul_one a₂]

Premises used: mul_one
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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)) (1 ⊗ₜ[A] (a₂ * 1))

Tactic:
simp only [← smul_eq_mul, ← TensorProduct.smul_tmul, ha (1 : B)]

Premises used: TensorProduct.smul_tmul, smul_eq_mul, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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

Tactic:
le_antisymm ?_ le_comap_map

Premises used: le_antisymm, Ideal.le_comap_map
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
refine : comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I) ≤ I
⊢ comap (F := A →+* B) (algebraMap A B) (map (F := A →+* B) (algebraMap A B) I) = I

Tactic:
refine le_antisymm ?_ le_comap_map

Premises used: le_antisymm, Ideal.le_comap_map
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (Function.comp (β := B ⊗[A] (A ⧸ I))
      (⇑(↑(LinearEquiv.restrictScalars A
                (↑(AlgEquiv.symm (quotIdealMapEquivTensorQuot B I)) :
                  B ⊗[A] (A ⧸ I) ≃ₗ[B] B ⧸ map (algebraMap A B) I)) :
            B ⊗[A] (A ⧸ I) →ₗ[A] B ⧸ map (algebraMap A B) I) :
        (a : B ⊗[A] (A ⧸ I)) → B ⧸ map (algebraMap A B) I)
      (⇑((TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) : (a : A ⧸ I) → B ⊗[A] (A ⧸ I)))

Tactic:
(LinearEquiv.injective _).comp <|
      Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)

Premises used: HasQuotient.Quotient, Function.Injective.comp, Module.FaithfullyFlat.tensorProduct_mk_injective, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A ⧸ I) (β :=
    HasQuotient.Quotient B (B := Ideal B) (map (F := A →+* B) (algebraMap A B) I))
    (Function.comp (β := B ⊗[A] (A ⧸ I))
      (⇑(↑(LinearEquiv.restrictScalars A
                (↑(AlgEquiv.symm (quotIdealMapEquivTensorQuot B I)) :
                  B ⊗[A] (A ⧸ I) ≃ₗ[B] B ⧸ map (algebraMap A B) I)) :
            B ⊗[A] (A ⧸ I) →ₗ[A] B ⧸ map (algebraMap A B) I) :
        (a : B ⊗[A] (A ⧸ I)) → B ⧸ map (algebraMap A B) I)
      (⇑((TensorProduct.mk A B (A ⧸ I) : (a : B) → A ⧸ I →ₗ[A] B ⊗[A] (A ⧸ I)) 1) : (a : A ⧸ I) → B ⊗[A] (A ⧸ I)))

Tactic:
exact (LinearEquiv.injective _).comp <|
      Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)

Premises used: HasQuotient.Quotient, Function.Injective.comp, Module.FaithfullyFlat.tensorProduct_mk_injective, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ 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)
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ 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

Premises used: Ideal.mem_comap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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)
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)
⊢ x ∈ I

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem] at hx ⊢

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ Function.Surjective (α := Ideal B) (β := Ideal A) (comap (F := A →+* B) (algebraMap A B))

Tactic:
fun I ↦ ⟨I.map (algebraMap A B), comap_map_eq_self_of_faithfullyFlat I⟩

Premises used: Ideal.comap_map_eq_self_of_faithfullyFlat, Algebra.algebraMap, Ideal.map, Exists.intro, Function.Surjective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
x x_1 : Ideal A
h : Eq.{u_2 + 1} (α := Ideal B) (map (F := A →+* B) (algebraMap A B) x) (map (F := A →+* B) (algebraMap A B) x_1)
⊢ x = x_1

Tactic:
simpa [comap_map_eq_self_of_faithfullyFlat]
    using congr_arg (Ideal.comap (algebraMap A B) ·) h

Premises used: Ideal.comap_map_eq_self_of_faithfullyFlat, Algebra.algebraMap, congr_arg, Ideal.comap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
obtain :
  ∀ (P : Ideal B),
    P.IsPrime → ∀ (hP : comap (F := A →+* B) (algebraMap A B) P = p), ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver 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)

Premises used: Ideal.comap_map_eq_self_of_faithfullyFlat, Ideal.comap_map_eq_self_iff_of_isPrime, Iff.mp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
left : P.IsPrime
hP : comap (F := A →+* B) (algebraMap A B) P = p
⊢ ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p

Tactic:
⟨P, inferInstance, ⟨hP.symm⟩⟩

Premises used: inferInstance, Ideal.LiesOver.mk, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
left : P.IsPrime
hP : comap (F := A →+* B) (algebraMap A B) P = p
⊢ ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p

Tactic:
exact ⟨P, inferInstance, ⟨hP.symm⟩⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
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
⊢ Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (comap (algebraMap A B))

Tactic:
fun I ↦
  (PrimeSpectrum.mem_range_comap_iff (algebraMap A B)).mpr
    I.asIdeal.comap_map_eq_self_of_faithfullyFlat

Premises used: Iff.mpr, Ideal.comap_map_eq_self_of_faithfullyFlat, Algebra.algebraMap, Set.Mem, setOf, PrimeSpectrum.mem_range_comap_iff, Set.range, PrimeSpectrum.asIdeal, Function.Surjective