awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact .comp (.of_bijective e.symm.bijective) hf
-- Module: Mathlib.RingTheory.RingHom.Flat
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

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.RingHom.Flat
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
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)
⊢ (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 ↦ ?_⟩
-- 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 : (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))))
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)))
refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)
⊢ f.Flat

Tactic:
rwa [← comp_ulift_eq.{u₁, u₂} f, comp_iff_of_bijective_left (Equiv.bijective _),
      comp_iff_of_bijective_right (Equiv.bijective _)]

Premises used: RingHom.Flat.comp_iff_of_bijective_right, RingHom.Flat.comp_iff_of_bijective_left
-- 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
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat (R := ULift.{u₁, u_1} R) (S := ULift.{u₂, u_2} S)

Tactic:
.comp (.comp (.of_bijective <| Equiv.bijective _) hf)
      (.of_bijective <| Equiv.bijective _)

Premises used: Equiv.bijective, RingHom.Flat.comp, RingHom.ulift, 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
f : R →+* S
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:
exact .comp (.comp (.of_bijective <| Equiv.bijective _) hf)
      (.of_bijective <| Equiv.bijective _)
-- Module: Mathlib.RingTheory.RingHom.Flat
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
⊢ Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑T : Type u_1)

Tactic:
algebraize [f.hom, g.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
⊢ 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)

Tactic:
have : _ = pushout.inr f g := (CommRingCat.isPushout_tensorProduct R S T).inr_isoPushout_hom
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
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 ⋯) :
              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))
⊢ 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))

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
            (X := T) (Y := 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)))) :
          (↑T : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
      (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))

Tactic:
(CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeRight_injective (B := T) hf)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.IsPushout.isoPushout, CommRingCat.carrier, RingEquiv.injective, CommRingCat.isPushout_tensorProduct, Algebra.TensorProduct.includeRight_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
            (X := T) (Y := 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)))) :
          (↑T : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
      (a : (↑T : Type u_1)) → (↑(pushout f g) : Type u_1))

Tactic:
exact (CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeRight_injective (B := T) hf)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.IsPushout.isoPushout, CommRingCat.carrier, RingEquiv.injective, CommRingCat.isPushout_tensorProduct, Algebra.TensorProduct.includeRight_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
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))
⊢ Module.Flat.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)

Tactic:
algebraize [f.hom, g.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
⊢ 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)

Tactic:
have : _ = pushout.inl f g := (CommRingCat.isPushout_tensorProduct R S T).inl_isoPushout_hom
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
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 ⋯) :
              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))
⊢ 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))

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
            (X := S) (Y := 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)))) :
          (↑S : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
      (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))

Tactic:
(CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeLeft_injective (S := R) (A := S) hg)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.IsPushout.isoPushout, CommRingCat.carrier, RingEquiv.injective, Algebra.TensorProduct.includeLeft_injective, CommRingCat.isPushout_tensorProduct, Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
            (X := S) (Y := 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)))) :
          (↑S : Type u_1) →+* (↑(pushout f g) : Type u_1)) :
      (a : (↑S : Type u_1)) → (↑(pushout f g) : Type u_1))

Tactic:
exact (CommRingCat.isPushout_tensorProduct R S T).isoPushout.commRingCatIsoToRingEquiv
    |>.injective.comp (Algebra.TensorProduct.includeLeft_injective (S := R) (A := S) hg)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.IsPushout.isoPushout, CommRingCat.carrier, RingEquiv.injective, Algebra.TensorProduct.includeLeft_injective, CommRingCat.isPushout_tensorProduct, Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ flat f ↔ (Hom.hom f).Flat

Tactic:
.rfl

Premises used: Iff.rfl, CommRingCat.flat, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ flat (ofHom f) ↔ f.Flat

Tactic:
.rfl

Premises used: Iff.rfl, CommRingCat.flat, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
rw : RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.Flat
⊢ flat.IsStableUnderCobaseChange

Tactic:
rw [flat, RingHom.isStableUnderCobaseChange_toMorphismProperty_iff]

Premises used: RingHom.isStableUnderCobaseChange_toMorphismProperty_iff, CommRingCat.flat
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
⊢ RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.Flat

Tactic:
RingHom.Flat.isStableUnderBaseChange

Premises used: RingHom.Flat.isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
⊢ RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.Flat

Tactic:
exact RingHom.Flat.isStableUnderBaseChange

Premises used: RingHom.Flat.isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.Flat
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))
⊢ 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 ⊢

Premises used: CommRingCat.flat_ofHom_iff
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
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)))
⊢ 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)))

Tactic:
apply MorphismProperty.of_isPushout _ h

Premises used: CategoryTheory.MorphismProperty.of_isPushout
-- Module: Mathlib.RingTheory.RingHom.Flat
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.of (S ⊗[R] S) ⟶ CommRingCat.of (T ⊗[R] A)

Tactic:
exact CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T)
      (IsScalarTower.toAlgHom R S A)).toRingHom

Premises used: Algebra.TensorProduct.map, IsScalarTower.toAlgHom, CommRingCat.ofHom, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.RingHom.Flat
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.of S ⟶ CommRingCat.of (T ⊗[S] A)

Tactic:
exact CommRingCat.ofHom
      (RingHom.comp (Algebra.TensorProduct.includeLeft (S := R)).toRingHom (algebraMap S T))

Premises used: Algebra.algebraMap, CommRingCat.ofHom, RingHom.comp