awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
    (↑(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)
have 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))
Tactic: change RingHom.Flat (RingHom.comp (Algebra.TensorProduct.lTensor D
      (AlgHom.restrictScalars R f)).toRingHom _)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
have refine : ∀ (hf : (g.comp f).Flat), f.Flat
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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.Flat
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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)
⊢ f.Flat
have 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))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
have refine : ∀ (hf : (f.comp g).Flat), f.Flat
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ .comp (.of_bijective hg) hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
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.Flat
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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
⊢ f.Flat
have 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)
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
f : R →+* S
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S) ↔ f.Flat
have refine_1 : ∀ (hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)), f.Flat
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- 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
refine_1 : ∀ (hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)), f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S) ↔ f.Flat
have refine_2 : ∀ (hf : f.Flat), (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- 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 : (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)
⊢ f.Flat
have refine_1 : Flat.{u_1, u_2} (R := R) (S := S)
  (RingHom.comp (RingEquiv.toRingHom ULift.ringEquiv)
    ((ulift.{u₁, u₂, u_1, u_2} f).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv))))
Tactic: rwa [← comp_ulift_eq.{u₁, u₂} f, comp_iff_of_bijective_left (Equiv.bijective _),
      comp_iff_of_bijective_right (Equiv.bijective _)]
-- 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 : (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)
refine_1 :
  Flat.{u_1, u_2} (R := R) (S := S)
    (RingHom.comp (RingEquiv.toRingHom ULift.ringEquiv)
      ((ulift.{u₁, u₂, u_1, u_2} f).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv))))
⊢ f.Flat
have refine_1₁ : Flat (R := R) (S := ULift.{u₂, u_2} S)
  ((ulift.{u₁, u₂, u_1, u_2} f).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv)))
Tactic: rwa [← comp_ulift_eq.{u₁, u₂} f, comp_iff_of_bijective_left (Equiv.bijective _),
      comp_iff_of_bijective_right (Equiv.bijective _)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
hg : (Hom.hom g).Flat
⊢ Function.Injective (α := (↑T : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inr f g)) :
      (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))
have algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑T : Type u_1)
Tactic: algebraize [f.hom, g.hom]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
hg : (Hom.hom g).Flat
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u_1) (↑T : Type u_1) := (Hom.hom g).toAlgebra
algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑T : Type u_1)
⊢ Function.Injective (α := (↑T : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inr f g)) :
      (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))
have this : Eq.{u_1 + 1} (α := T ⟶ pushout f g)
  (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ Iso.hom (IsPushout.isoPushout sorry) :
    of (↑T : Type u_1) ⟶
      pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
        (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1))) (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1))))
  (pushout.inr f g)
Tactic: have : _ = pushout.inr f g := (CommRingCat.isPushout_tensorProduct R S T).inr_isoPushout_hom
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
hg : (Hom.hom g).Flat
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u_1) (↑T : Type u_1) := (Hom.hom g).toAlgebra
algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑T : Type u_1)
this :
  Eq.{u_1 + 1} (α := T ⟶ pushout f g)
    (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ Iso.hom (IsPushout.isoPushout ⋯) :
      of (↑T : Type u_1) ⟶
        pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
          (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1))) (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1))))
    (pushout.inr f g)
⊢ Function.Injective (α := (↑T : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inr f g)) :
      (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))
have rw : Function.Injective (α := (↑T : Type u_1)) (β := (↑(pushout f g) : Type u_1))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (X := T) (Y := pushout f g)
          (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ Iso.hom (IsPushout.isoPushout sorry) :
            of (↑T : Type u_1) ⟶
              pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
                (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1)))
                (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1)))) :
        (↑T : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
    (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑T : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          g) :
      (a : (↑R : Type u_1)) → (↑T : Type u_1))
⊢ Function.Injective (α := (↑S : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inl f g)) :
      (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))
have algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
Tactic: algebraize [f.hom, g.hom]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑T : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          g) :
      (a : (↑R : Type u_1)) → (↑T : Type u_1))
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u_1) (↑T : Type u_1) := (Hom.hom g).toAlgebra
algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
⊢ Function.Injective (α := (↑S : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inl f g)) :
      (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))
have this : Eq.{u_1 + 1} (α := S ⟶ pushout f g)
  (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ Iso.hom (IsPushout.isoPushout sorry) :
    of (↑S : Type u_1) ⟶
      pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
        (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1))) (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1))))
  (pushout.inl f g)
Tactic: have : _ = pushout.inl f g := (CommRingCat.isPushout_tensorProduct R S T).inl_isoPushout_hom
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑T : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          g) :
      (a : (↑R : Type u_1)) → (↑T : Type u_1))
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u_1) (↑T : Type u_1) := (Hom.hom g).toAlgebra
algebraizeInst : Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
this :
  Eq.{u_1 + 1} (α := S ⟶ pushout f g)
    (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ Iso.hom (IsPushout.isoPushout ⋯) :
      of (↑S : Type u_1) ⟶
        pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
          (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1))) (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1))))
    (pushout.inl f g)
⊢ Function.Injective (α := (↑S : Type u_1)) (β := (↑(pushout f g) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (Y := pushout f g) (pushout.inl f g)) :
      (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))
have rw : Function.Injective (α := (↑S : Type u_1)) (β := (↑(pushout f g) : Type u_1))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
          (X := S) (Y := pushout f g)
          (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ Iso.hom (IsPushout.isoPushout sorry) :
            of (↑S : Type u_1) ⟶
              pushout (X := of (↑R : Type u_1)) (Y := of (↑S : Type u_1)) (Z := of (↑T : Type u_1))
                (ofHom (algebraMap (↑R : Type u_1) (↑S : Type u_1)))
                (ofHom (algebraMap (↑R : Type u_1) (↑T : Type u_1)))) :
        (↑S : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
    (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
⊢ flat.IsStableUnderCobaseChange
have rw : RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.Flat
Tactic: rw [flat, RingHom.isStableUnderCobaseChange_toMorphismProperty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (hypothesis)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h : Flat.{u, u} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R))
⊢ Flat.{u, u} (R := T ⊗[R] A) (S := T ⊗[S] A) (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A))
have h₁ : CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
  (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
Tactic: rw [← CommRingCat.flat_ofHom_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ CommRingCat.flat.{u} (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
have apply : CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)
Tactic: apply MorphismProperty.of_isPushout _ h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
apply : CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)
⊢ CommRingCat.flat.{u} (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
have apply₁ : CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)
Tactic: apply MorphismProperty.of_isPushout _ h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
apply : CommRingCat.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)
apply₁ : CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)
⊢ CommRingCat.flat.{u} (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
have apply₂ : IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
  CommRingCat.of (T ⊗[S] A))
  (CommRingCat.ofHom
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
        S ⊗[R] S →ₐ[R] T ⊗[R] A)))
  (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
  (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
  (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
Tactic: apply MorphismProperty.of_isPushout _ h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
    CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
          S ⊗[R] S →ₐ[R] T ⊗[R] A)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
    (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
have refine_1 : pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
    (CommRingCat.ofHom (algebraMap R S)) ≅
  CommRingCat.of (S ⊗[R] S)
Tactic: refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_