awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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 R (Localization.AtPrime P)
have h₁ : 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 ..
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
⊢ Flat (R := Localization.AtPrime Q) (S := Localization.AtPrime P) (Localization.localRingHom Q P f hQP)
have 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 sorry)
Tactic: subst hQP
Cleared hypotheses: Q, inst_3, hQP
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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)
⊢ Flat (R := Localization.AtPrime (Ideal.comap f P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap f P) P f ⋯)
have algebraizeInst : Module.Flat R S
Tactic: algebraize [f, Localization.localRingHom (Ideal.comap f P) P f rfl]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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
⊢ Flat (R := Localization.AtPrime (Ideal.comap f P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap f P) P f ⋯)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
⊢ Flat (R := Localization.AtPrime (Ideal.comap f P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap f P) P f ⋯)
have rw : Module.Flat.{u_1, u_2} R (Localization.AtPrime P)
Tactic: rw [RingHom.Flat, Module.flat_iff_of_isLocalization
    (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
⊢ f.Flat
have rw : Module.Flat R S
Tactic: rw [← f.algebraMap_toAlgebra, RingHom.flat_algebraMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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
⊢ 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))
have algebraizeInst : Module.Flat B D
Tactic: algebraize [f.toRingHom, (Algebra.TensorProduct.lTensor (S := A) A f).toRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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
⊢ Flat (R := A ⊗[R] B) (S := C ⊗[R] D) (AlgHom.toRingHom (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D))
have 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)
Tactic: have heq : Algebra.TensorProduct.map f g =
      (Algebra.TensorProduct.map f (.id R D)).comp (Algebra.TensorProduct.map (.id _ _) g) := by
    ext <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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 (Algebra.TensorProduct.map f g : A ⊗[R] B →ₐ[S] C ⊗[R] D))
have 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))
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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))
have refine_1 : Flat (↑(Algebra.TensorProduct.map (AlgHom.id S A) g : A ⊗[R] B →ₐ[S] A ⊗[R] D) : A ⊗[R] B →+* A ⊗[R] D)
Tactic: refine RingHom.Flat.comp ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
⊢ 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))
have 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))
Tactic: refine RingHom.Flat.comp ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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] D) (S := C ⊗[R] D)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D))
have 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)))
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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D) : A ⊗[R] D →ₐ[S] C ⊗[R] D)))
have 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))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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))))
have 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)
Tactic: refine RingHom.Flat.comp ?_ (.of_bijective <| AlgEquiv.bijective _)