awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
P : Ideal S
inst_2 : P.IsMaximal
algInst_1 : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat.{u_4, u_4} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)

Tactic:
replace h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) := h ..
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
P : Ideal S
inst_2 : P.IsMaximal
algInst_1 : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
h : Module.Flat.{u_4, u_4} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans, Ideal.comap
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
P : Ideal S
inst_2 : P.IsMaximal
algInst_1 : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
h : Module.Flat.{u_4, u_4} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
exact Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans, Ideal.comap
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
Q : Ideal R
inst_3 : Q.IsPrime
hQP : Q = Ideal.comap f P
subst :
  ∀ [inst_4 : Ideal.IsPrime (Ideal.comap f P)],
    Flat (R := Localization.AtPrime (Ideal.comap f P)) (S := Localization.AtPrime P)
      (Localization.localRingHom (Ideal.comap f P) P f ⋯)
⊢ Flat (R := Localization.AtPrime Q) (S := Localization.AtPrime P) (Localization.localRingHom Q P f hQP)

Tactic:
subst hQP
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f P)
⊢ Module.Flat R S

Tactic:
algebraize [f, Localization.localRingHom (Ideal.comap f P) P f rfl]

Premises used: Localization.localRingHom, Ideal.comap, rfl
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f P)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
algebraizeInst : Module.Flat R S
⊢ IsScalarTower.{u_1, u_1, u_2} R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)

Tactic:
have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f P)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
algebraizeInst : Module.Flat R S
this : IsScalarTower.{u_1, u_1, u_2} R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
rw : Module.Flat.{u_1, u_2} R (Localization.AtPrime P)
⊢ Flat (R := Localization.AtPrime (Ideal.comap f P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap f P) P f ⋯)

Tactic:
rw [RingHom.Flat, Module.flat_iff_of_isLocalization
    (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]

Premises used: RingHom.Flat, Localization.AtPrime, Ideal.comap, Ideal.primeCompl, Module.flat_iff_of_isLocalization
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f P)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
algebraizeInst : Module.Flat R S
this : IsScalarTower.{u_1, u_1, u_2} R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat.{u_1, u_2} R (Localization.AtPrime P)

Tactic:
Module.Flat.trans R S (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst_2 : P.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f P)
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
algebraizeInst : Module.Flat R S
this : IsScalarTower.{u_1, u_1, u_2} R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat.{u_1, u_2} R (Localization.AtPrime P)

Tactic:
exact Module.Flat.trans R S (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hR : IsField R
f : R →+* S
this_1 : Algebra R S := f.toAlgebra
this : Field R := hR.toField
rw : Module.Flat R S
⊢ f.Flat

Tactic:
rw [← f.algebraMap_toAlgebra, RingHom.flat_algebraMap_iff]

Premises used: RingHom.flat_algebraMap_iff, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
hR : IsField R
f : R →+* S
this_1 : Algebra R S := f.toAlgebra
this : Field R := hR.toField
⊢ Module.Flat R S

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing D
inst_10 : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
⊢ Module.Flat B D

Tactic:
algebraize [f.toRingHom, (Algebra.TensorProduct.lTensor (S := A) A f).toRingHom]

Premises used: AlgHom.toRingHom, Algebra.TensorProduct.lTensor
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing D
inst_10 : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
algInst : Algebra B D := f.toAlgebra
algInst_1 : Algebra (A ⊗[R] B) (A ⊗[R] D) :=
  toAlgebra (AlgHom.toRingHom (R := A) (Algebra.TensorProduct.lTensor A f : A ⊗[R] B →ₐ[A] A ⊗[R] D))
algebraizeInst : Module.Flat B D
e : A ⊗[R] D ≃ₐ[A ⊗[R] B] A ⊗[R] B ⊗[B] D :=
  let __spread.0 : A ⊗[R] D ≃ₐ[A] A ⊗[R] B ⊗[B] D :=
    AlgEquiv.symm (Algebra.IsPushout.cancelBaseChangeAlg R A B (A ⊗[R] B) D);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Flat (R := A ⊗[R] B) (S := A ⊗[R] D)
    (AlgHom.toRingHom (R := S) (Algebra.TensorProduct.lTensor A f : A ⊗[R] B →ₐ[S] A ⊗[R] D))

Tactic:
.of_linearEquiv e.toLinearEquiv

Premises used: RingHom.Flat, AlgEquiv.toLinearEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing D
inst_10 : Algebra R D
f : B →ₐ[R] D
hf : f.Flat
algInst : Algebra B D := f.toAlgebra
algInst_1 : Algebra (A ⊗[R] B) (A ⊗[R] D) :=
  toAlgebra (AlgHom.toRingHom (R := A) (Algebra.TensorProduct.lTensor A f : A ⊗[R] B →ₐ[A] A ⊗[R] D))
algebraizeInst : Module.Flat B D
e : A ⊗[R] D ≃ₐ[A ⊗[R] B] A ⊗[R] B ⊗[B] D :=
  let __spread.0 : A ⊗[R] D ≃ₐ[A] A ⊗[R] B ⊗[B] D :=
    AlgEquiv.symm (Algebra.IsPushout.cancelBaseChangeAlg R A B (A ⊗[R] B) D);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Flat (R := A ⊗[R] B) (S := A ⊗[R] D)
    (AlgHom.toRingHom (R := S) (Algebra.TensorProduct.lTensor A f : A ⊗[R] B →ₐ[S] A ⊗[R] D))

Tactic:
exact .of_linearEquiv e.toLinearEquiv
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
ha :
  ∀ (x : A),
    Eq (α := C ⊗[R] D)
      (((AlgHom.comp (B := A ⊗[R] B) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
                (Algebra.TensorProduct.includeLeft : A →ₐ[S] A ⊗[R] B) :
              A →ₐ[S] C ⊗[R] D) :
            (a : A) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      (((AlgHom.comp (B := A ⊗[R] B)
                (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
                    (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
                  A ⊗[R] B →ₐ[S] C ⊗[R] D)
                (Algebra.TensorProduct.includeLeft : A →ₐ[S] A ⊗[R] B) :
              A →ₐ[S] C ⊗[R] D) :
            (a : A) → C ⊗[R] D)
          x :
        C ⊗[R] D)
hb :
  ∀ (x : B),
    Eq (α := C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D))
              Algebra.TensorProduct.includeRight :
            (a : B) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
                    (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
                  A ⊗[R] B →ₐ[S] C ⊗[R] D))
              Algebra.TensorProduct.includeRight :
            (a : B) → C ⊗[R] D)
          x :
        C ⊗[R] D)
⊢ Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x : A
⊢ Eq (α := C ⊗[R] D)
    (((AlgHom.comp (B := A ⊗[R] B) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
              (Algebra.TensorProduct.includeLeft : A →ₐ[S] A ⊗[R] B) :
            A →ₐ[S] C ⊗[R] D) :
          (a : A) → C ⊗[R] D)
        x :
      C ⊗[R] D)
    (((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
                  (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
                A ⊗[R] B →ₐ[S] C ⊗[R] D)
              (Algebra.TensorProduct.includeLeft : A →ₐ[S] A ⊗[R] B) :
            A →ₐ[S] C ⊗[R] D) :
          (a : A) → C ⊗[R] D)
        x :
      C ⊗[R] D)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x : B
⊢ Eq (α := C ⊗[R] D)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D))
            Algebra.TensorProduct.includeRight :
          (a : B) → C ⊗[R] D)
        x :
      C ⊗[R] D)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
                  (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
                A ⊗[R] B →ₐ[S] C ⊗[R] D))
            Algebra.TensorProduct.includeRight :
          (a : B) → C ⊗[R] D)
        x :
      C ⊗[R] D)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
⊢ Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)

Tactic:
have heq : Algebra.TensorProduct.map f g =
      (Algebra.TensorProduct.map f (.id R D)).comp (Algebra.TensorProduct.map (.id _ _) g) := by
    ext <;> simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
rw :
  Flat (R := A ⊗[R] B) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
          (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
        A ⊗[R] B →ₐ[S] C ⊗[R] D))
⊢ Flat (R := A ⊗[R] B) (S := C ⊗[R] D) (AlgHom.toRingHom (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D))

Tactic:
rw [heq]
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
⊢ Flat (R := A ⊗[R] B) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
          (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
        A ⊗[R] B →ₐ[S] C ⊗[R] D))

Tactic:
RingHom.Flat.comp ?_ ?_

Premises used: RingHom.Flat.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
refine_1 : Flat (↑(Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) : A ⊗[R] B →+* A ⊗[R] D)
refine_2 :
  Flat (R := A ⊗[R] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D))
⊢ Flat (R := A ⊗[R] B) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
          (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
        A ⊗[R] B →ₐ[S] C ⊗[R] D))

Tactic:
refine RingHom.Flat.comp ?_ ?_

Premises used: RingHom.Flat.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
⊢ Flat (↑(Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) : A ⊗[R] B →+* A ⊗[R] D)

Tactic:
hg.lTensor _

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHom.Flat.lTensor, RingHomClass.toRingHom, TensorProduct
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
⊢ Flat (↑(Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) : A ⊗[R] B →+* A ⊗[R] D)

Tactic:
exact hg.lTensor _

Premises used: RingHom.Flat.lTensor
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : CommRing D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (AlgHom.comp (B := A ⊗[R] D) (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)
        (Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) :
      A ⊗[R] B →ₐ[S] C ⊗[R] D)
ha :
  ∀ (x : A),
    Eq (α := C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] D)
              (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D))
              Algebra.TensorProduct.includeLeft :
            (a : A) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      ((AlgHom.comp
              (AlgHom.comp (↑(Algebra.TensorProduct.comm R D C) : D ⊗[R] C →ₐ[R] C ⊗[R] D)
                (AlgHom.comp (Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f) : D ⊗[R] A →ₐ[R] D ⊗[R] C)
                  ((↑(Algebra.TensorProduct.comm R A D) : A ⊗[R] D →ₐ[R] D ⊗[R] A) : A ⊗[R] D →ₐ[R] D ⊗[R] A)))
              Algebra.TensorProduct.includeLeft :
            (a : A) → C ⊗[R] D)
          x :
        C ⊗[R] D)
hb :
  ∀ (x : D),
    Eq (α := C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] D)
              (AlgHom.restrictScalars R
                (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)))
              Algebra.TensorProduct.includeRight :
            (a : D) → C ⊗[R] D)
          x :
        C ⊗[R] D)
      ((AlgHom.comp (B := A ⊗[R] D)
              (AlgHom.restrictScalars R
                (AlgHom.comp (↑(Algebra.TensorProduct.comm R D C) : D ⊗[R] C →ₐ[R] C ⊗[R] D)
                  (AlgHom.comp (Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f) : D ⊗[R] A →ₐ[R] D ⊗[R] C)
                    ((↑(Algebra.TensorProduct.comm R A D) : A ⊗[R] D →ₐ[R] D ⊗[R] A) : A ⊗[R] D →ₐ[R] D ⊗[R] A))))
              Algebra.TensorProduct.includeRight :
            (a : D) → C ⊗[R] D)
          x :
        C ⊗[R] D)
⊢ Eq (α := A ⊗[R] D →ₐ[R] C ⊗[R] D)
    (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D))
    (AlgHom.comp (↑(Algebra.TensorProduct.comm R D C) : D ⊗[R] C →ₐ[R] C ⊗[R] D)
      (AlgHom.comp (Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f) : D ⊗[R] A →ₐ[R] D ⊗[R] C)
        ((↑(Algebra.TensorProduct.comm R A D) : A ⊗[R] D →ₐ[R] D ⊗[R] A) : A ⊗[R] D →ₐ[R] D ⊗[R] A)))

Tactic:
ext