awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x : ULift.{max u₁ u₂ u₃, u₃} T
⊢ Eq.{u₃ + 1} (α := T)
    (ULift.down
      ((AlgHom.comp
            (AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R) (S := ULift.{max (max u₁ u₂) u₃, u₁} R)
              (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)))
            TensorProduct.includeRight :
          (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
        x))
    (ULift.down
      ((AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T)
            (AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R) (S := ULift.{max (max u₁ u₂) u₃, u₁} R)
              (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
                (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
                  ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
                      ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                    ULift.{max u₁ u₂ u₃, u₃} T)
                (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                    (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
                  ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
                      ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
                    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)))
            TensorProduct.includeRight :
          (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
        x))

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))

Tactic:
have heq : TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T) (ULift R) =
        AlgHom.comp ((TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T)
          (ULift.{max u₁ u₂ u₃} S)).restrictScalars (ULift.{max u₁ u₂ u₃} R))
          (TensorProduct.mapOfCompatibleSMul ..) := by
      ext <;> simp
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
rw :
  RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T)
    (AlgHom.toRingHom (R := ULift.{max u₁ u₂ u₃, u₁} R)
      (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
        (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T)
        (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
            (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)))
⊢ RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T) (AlgHom.toRingHom (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₁} R)))

Tactic:
rw [heq]
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T)
    (AlgHom.toRingHom (R := ULift.{max u₁ u₂ u₃, u₁} R)
      (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
        (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T)
        (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
            (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)))

Tactic:
.comp ?_ ?_

Premises used: RingHom.Flat.comp
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat
    (↑(TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
            (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T) :
      ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T →+*
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)

Tactic:
(flat_lmul' (ULift R) (ULift S)).mapOfCompatibleSMul
        (ULift.{max u₁ u₂ u₃} T) (ULift.{max u₁ u₂ u₃} T)

Premises used: RingHom.Flat.mapOfCompatibleSMul, Quotient.liftOn', AddCon.liftOn, ULift, MonoidHomClass.toMonoidHom, Algebra.WeaklyEtale.flat_lmul', RingHomClass.toRingHom, TensorProduct
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat
    (↑(TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
            (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
              ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T) :
      ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T →+*
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)

Tactic:
exact (flat_lmul' (ULift R) (ULift S)).mapOfCompatibleSMul
        (ULift.{max u₁ u₂ u₃} T) (ULift.{max u₁ u₂ u₃} T)
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T)
    (AlgHom.toRingHom (R := ULift.{max u₁ u₂ u₃, u₁} R)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))))

Tactic:
WeaklyEtale.flat_lmul' (ULift S) (ULift T)

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Quotient.liftOn', AddCon.liftOn, AlgHom.ofLinearMap, ULift, Algebra.TensorProduct.lmul', MonoidHomClass.toMonoidHom, Algebra.WeaklyEtale.flat_lmul', AlgHom.restrictScalars, Algebra.TensorProduct.lmul'', RingHomClass.toRingHom, TensorProduct
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T)
    (AlgHom.toRingHom (R := ULift.{max u₁ u₂ u₃, u₁} R)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))))

Tactic:
exact WeaklyEtale.flat_lmul' (ULift S) (ULift T)

Premises used: ULift, Algebra.WeaklyEtale.flat_lmul'
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
mp : IsIdempotentElem I → ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
mpr : (∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e) → IsIdempotentElem I
⊢ IsIdempotentElem I ↔ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
rw : I ≤ I * I
⊢ I ≤ I • I

Tactic:
rw [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I * I

Tactic:
e.ge

Premises used: Eq.ge, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I * I

Tactic:
exact e.ge

Premises used: Eq.ge
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
mp : ∀ (r : R) (hr : r ∈ I) (hr' : ∀ n ∈ I, r • n = n), ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e

Tactic:
obtain ⟨r, hr, hr'⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
        (by
          rw [smul_eq_mul]
          exact e.ge)

Premises used: Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e

Tactic:
⟨r, hr' r hr, antisymm ?_ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩

Premises used: Iff.mpr, And.intro, antisymm, Exists.intro, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
mp : I ≤ R ∙ r
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e

Tactic:
refine ⟨r, hr' r hr, antisymm ?_ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
mp : Membership.mem (γ := Submodule R R) (R ∙ r) (r * x)
⊢ Membership.mem (γ := Submodule R R) (R ∙ r) x

Tactic:
rw [← hr' x hx]
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ Membership.mem (γ := Submodule R R) (R ∙ r) (r * x)

Tactic:
Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', Set.Mem, setOf, Exists.intro, mul_comm
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ Membership.mem (γ := Submodule R R) (R ∙ r) (r * x)

Tactic:
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', Exists.intro
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ IsIdempotentElem (M := Ideal R) (R ∙ e)

Tactic:
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]

Premises used: Ideal.span_singleton_mul_span_singleton, IsIdempotentElem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : I.FG
mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
mpr : I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
mp :
  ∀ (e : R) (he : IsIdempotentElem e) (h : FG (R ∙ e)) (H : IsIdempotentElem (M := Ideal R) (R ∙ e)),
    Eq (α := Ideal R) (R ∙ e) ⊥ ∨ Eq (α := Ideal R) (R ∙ e) ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H

Premises used: Ideal.isIdempotentElem_iff_of_fg, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
H : IsIdempotentElem (M := Ideal R) (R ∙ e)
mp : e = 0 ∨ Eq (α := Ideal R) (span {e}) ⊤
⊢ Eq (α := Ideal R) (R ∙ e) ⊥ ∨ Eq (α := Ideal R) (R ∙ e) ⊤

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ideal.submodule_span_eq
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
H : IsIdempotentElem (M := Ideal R) (R ∙ e)
apply : e = 1 → Eq (α := Ideal R) (span {e}) ⊤
⊢ e = 0 ∨ Eq (α := Ideal R) (span {e}) ⊤

Tactic:
apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)

Premises used: id, IsIdempotentElem.iff_eq_zero_or_one, Iff.mp, Or.imp
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
he : IsIdempotentElem.{u_1} (M := R) 1
h : FG (R ∙ 1)
H : IsIdempotentElem (M := Ideal R) (R ∙ 1)
⊢ Eq (α := Ideal R) (span {1}) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : FG.{u_1} (R := R) ⊥
⊢ IsIdempotentElem.{u_1} (M := Ideal R) ⊥

Tactic:
simp [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Ideal.IdempotentFG
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : FG.{u_1} (R := R) ⊤
⊢ IsIdempotentElem.{u_1} (M := Ideal R) ⊤

Tactic:
simp [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) x ↔
      Membership.mem (γ := Set R) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical} x
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}

Tactic:
ext x