awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)

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
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)
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)

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
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)
⊢ 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:
have : (Algebra.TensorProduct.map f (AlgHom.id R D)).restrictScalars R =
        (Algebra.TensorProduct.comm _ _ _).toAlgHom.comp
          ((Algebra.TensorProduct.lTensor _ (f.restrictScalars R)).comp
            (Algebra.TensorProduct.comm _ _ _).toAlgHom) := 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)
this :
  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)))
refine_2 :
  Flat (R := A ⊗[R] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (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))))
⊢ Flat (R := A ⊗[R] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)))

Tactic:
rw [this]
-- 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)
this :
  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)))
⊢ Flat (R := A ⊗[R] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (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:
RingHom.Flat.comp ?_ (.of_bijective <| AlgEquiv.bijective _)

Premises used: RingHom.Flat.comp, AlgEquiv.bijective, RingHom.Flat.of_bijective
-- 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)
this :
  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)))
refine_2 :
  Flat
    (↑(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) :
          A ⊗[R] D →ₐ[R] D ⊗[R] C) :
      A ⊗[R] D →+* D ⊗[R] C)
⊢ Flat (R := A ⊗[R] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom
      (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:
refine RingHom.Flat.comp ?_ (.of_bijective <| AlgEquiv.bijective _)

Premises used: RingHom.Flat.comp, RingHom.Flat.of_bijective
-- 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)
this :
  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)))
refine_2 :
  Flat (S := D ⊗[R] C)
    (RingHom.comp
      (AlgHom.toRingHom (R := R)
        (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 →+* D ⊗[R] A))
⊢ Flat
    (↑(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) :
          A ⊗[R] D →ₐ[R] D ⊗[R] C) :
      A ⊗[R] D →+* D ⊗[R] C)

Tactic:
change RingHom.Flat (RingHom.comp (Algebra.TensorProduct.lTensor D
      (AlgHom.restrictScalars R f)).toRingHom _)

Premises used: RingHom.Flat, RingHom.comp, AlgHom.restrictScalars, 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
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)
this :
  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)))
⊢ Flat (S := D ⊗[R] C)
    (RingHom.comp
      (AlgHom.toRingHom (R := R)
        (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 →+* D ⊗[R] A))

Tactic:
RingHom.Flat.comp (.of_bijective <| (TensorProduct.comm R A D).bijective) (lTensor D hf)

Premises used: TensorProduct.comm, LinearEquiv.bijective, RingHom.Flat.comp, RingHom.Flat.lTensor, RingHom.Flat.of_bijective
-- 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)
this :
  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)))
⊢ Flat (S := D ⊗[R] C)
    (RingHom.comp
      (AlgHom.toRingHom (R := R)
        (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 →+* D ⊗[R] A))

Tactic:
exact RingHom.Flat.comp (.of_bijective <| (TensorProduct.comm R A D).bijective) (lTensor D hf)
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
⊢ (g.comp f).Flat ↔ f.Flat

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩

Premises used: RingHom.Flat.comp, Iff.intro, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
refine : ∀ (hf : (g.comp f).Flat), f.Flat
⊢ (g.comp f).Flat ↔ f.Flat

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
a :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S)
      ((@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom
              (RingHom.comp e.toRingHom f) :
            (a : R) → S)
          x :
        S)
⊢ f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S)
    ((@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom
            (RingHom.comp e.toRingHom f) :
          (a : R) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
⊢ f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f)

Tactic:
have : f = e.symm.toRingHom.comp (e.toRingHom.comp f) := by ext; simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this :
  f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f)
rw :
  Flat.{u_1, u_2} (S := S)
    (@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f))
⊢ f.Flat

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this :
  f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f)
⊢ Flat.{u_1, u_2} (S := S)
    (@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f))

Tactic:
.comp hf (.of_bijective e.symm.bijective)

Premises used: RingHom.Flat.comp, RingEquiv.bijective, RingHom.Flat.of_bijective, RingEquiv.symm
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
this :
  f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f)
⊢ Flat.{u_1, u_2} (S := S)
    (@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ e.symm.toRingHom (RingHom.comp e.toRingHom f))

Tactic:
exact .comp hf (.of_bijective e.symm.bijective)
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
⊢ (f.comp g).Flat ↔ f.Flat

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ .comp (.of_bijective hg) hf⟩

Premises used: RingHom.Flat.comp, Iff.intro, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
refine : ∀ (hf : (f.comp g).Flat), f.Flat
⊢ (f.comp g).Flat ↔ f.Flat

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ .comp (.of_bijective hg) hf⟩
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
a :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S)
      ((@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom :
            (a : R) → S)
          x :
        S)
⊢ f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S)
    ((@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom :
          (a : R) → S)
        x :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
⊢ f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom

Tactic:
have : f = (f.comp e.toRingHom).comp e.symm.toRingHom := by ext; simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
this : f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom
rw :
  Flat.{u_1, u_2} (R := R)
    (@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom)
⊢ f.Flat

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective.{u_3 + 1, u_1 + 1} (α := T) (β := R) (⇑g : (a : T) → R)
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
this : f = @RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom
⊢ Flat.{u_1, u_2} (R := R)
    (@RingHom.comp.{u_1, u_3, u_2} _ T _ _ Semiring.toNonAssocSemiring _ (f.comp e.toRingHom) e.symm.toRingHom)

Tactic:
.comp (.of_bijective e.symm.bijective) hf

Premises used: RingHom.Flat.comp, RingEquiv.bijective, RingHom.Flat.of_bijective, RingEquiv.symm