awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
rw rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
⊢ (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
rw [dpow_apply hI hf hIJ hIf ha]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers J
hm : hI.IsDPMorphism hquot f
n : ℕ
x : B
hx : x ∈ J
obtain :
  ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)),
    hquot.dpow n ((f : (a : A) → B) a) = (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a)
⊢ hquot.dpow n x = (dividedPowers hI hf hIJ hIf).dpow n x

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers J
hm : hI.IsDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw : (f : (a : A) → B) (hI.dpow n a) = (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a)
rw₁ rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
⊢ hquot.dpow n ((f : (a : A) → B) a) = (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a)

Tactic:
rw [hm.2 a ha, dpow_apply hI hf hIJ hIf ha]

Premises used: DividedPowers.IsDPMorphism.dpow_comp, DividedPowers.Quotient.OfSurjective.dpow_apply
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
⊢ hI.IsSubDPIdeal (RingHom.ker (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) ⊓ I)

Tactic:
simpa [Ideal.mk_ker] using hIJ

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
n : ℕ
a : A
ha : a ∈ I
⊢ Eq (α := A ⧸ J) (sorry : A ⧸ J) ((Ideal.Quotient.mk J : (a : A) → A ⧸ J) (hI.dpow n a) : A ⧸ J)

Tactic:
DividedPowers.Quotient.OfSurjective.dpow_apply
    hI Ideal.Quotient.mk_surjective (refl _) (isSubDPIdeal_aux hI hIJ) ha

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Ideal.Quotient.mk_surjective, Bool.true, DividedPowers.Quotient.OfSurjective.dpow_apply, Function.const, Lean.Name, _private.0.DividedPowers.Quotient.isSubDPIdeal_aux, OfNat.ofNat, refl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.IsDPMorphism sorry (Ideal.Quotient.mk J)

Tactic:
DividedPowers.Quotient.OfSurjective.isDPMorphism
    hI Ideal.Quotient.mk_surjective (refl _) (isSubDPIdeal_aux hI hIJ)

Premises used: Unit.unit, DividedPowers.Quotient.OfSurjective.isDPMorphism, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Ideal.Quotient.mk_surjective, Bool.true, Function.const, Lean.Name, _private.0.DividedPowers.Quotient.isSubDPIdeal_aux, OfNat.ofNat, refl
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
algInst : Algebra (S ⊗[R] S) S := RingHom.toAlgebra (AlgHom.toRingHom (TensorProduct.lmul' R))
⊢ Etale.{u_1, u_2} R (S ⊗[R] S)

Tactic:
have : Etale R (S ⊗[R] S) := .comp _ S _
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
algInst : Algebra (S ⊗[R] S) S := RingHom.toAlgebra (AlgHom.toRingHom (TensorProduct.lmul' R))
this : Etale.{u_1, u_2} R (S ⊗[R] S)
⊢ Etale (S ⊗[R] S) S

Tactic:
have : Etale (S ⊗[R] S) S := .of_restrictScalars R _ _
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
algInst : Algebra (S ⊗[R] S) S := RingHom.toAlgebra (AlgHom.toRingHom (TensorProduct.lmul' R))
this_1 : Etale.{u_1, u_2} R (S ⊗[R] S)
this : Etale (S ⊗[R] S) S
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))

Tactic:
Smooth.flat (S ⊗[R] S) S

Premises used: RingHom.Flat, Algebra.Smooth.flat, TensorProduct
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
algInst : Algebra (S ⊗[R] S) S := RingHom.toAlgebra (AlgHom.toRingHom (TensorProduct.lmul' R))
this_1 : Etale.{u_1, u_2} R (S ⊗[R] S)
this : Etale (S ⊗[R] S) S
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))

Tactic:
exact Smooth.flat (S ⊗[R] S) S

Premises used: Algebra.Smooth.flat, TensorProduct
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
ha :
  ∀ (x : S),
    Eq (α := T ⊗[R] S)
      (((AlgHom.comp (B := T ⊗[R] S)
                (AlgHom.restrictScalars R
                  (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (TensorProduct.lmul' T) TensorProduct.includeLeft))
                TensorProduct.includeRight :
              S →ₐ[R] T ⊗[R] S) :
            (a : S) → T ⊗[R] S)
          x :
        T ⊗[R] S)
      (((AlgHom.comp (B := T ⊗[R] S)
                (AlgHom.restrictScalars R (S := T)
                  (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S))
                    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
                      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
                    TensorProduct.includeLeft))
                TensorProduct.includeRight :
              S →ₐ[R] T ⊗[R] S) :
            (a : S) → T ⊗[R] S)
          x :
        T ⊗[R] S)
hb :
  ∀ (x : S),
    Eq (α := T ⊗[R] S)
      (((AlgHom.comp (B := T ⊗[R] S)
                (AlgHom.restrictScalars R
                  (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S))
                    (AlgHom.restrictScalars T (S := T) (TensorProduct.lmul' T)) TensorProduct.includeRight))
                TensorProduct.includeRight :
              S →ₐ[R] T ⊗[R] S) :
            (a : S) → T ⊗[R] S)
          x :
        T ⊗[R] S)
      (((AlgHom.comp (B := T ⊗[R] S)
                (AlgHom.restrictScalars R (S := T)
                  (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S))
                    (AlgHom.restrictScalars T (S := T)
                      (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
                        (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S))))
                    TensorProduct.includeRight))
                TensorProduct.includeRight :
              S →ₐ[R] T ⊗[R] S) :
            (a : S) → T ⊗[R] S)
          x :
        T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
x : S
⊢ Eq (α := T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (TensorProduct.lmul' T) TensorProduct.includeLeft))
              TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R (S := T)
                (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S))
                  (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
                    (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
                  TensorProduct.includeLeft))
              TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        x :
      T ⊗[R] S)

Tactic:
simp [e, TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
x : S
⊢ Eq (α := T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (AlgHom.restrictScalars T (S := T) (TensorProduct.lmul' T))
                  TensorProduct.includeRight))
              TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R (S := T)
                (AlgHom.comp (B := T ⊗[R] S ⊗[T] (T ⊗[R] S))
                  (AlgHom.restrictScalars T (S := T)
                    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
                      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S))))
                  TensorProduct.includeRight))
              TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        x :
      T ⊗[R] S)

Tactic:
simp [e, TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
⊢ Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))

Tactic:
have : TensorProduct.lmul' T (S := T ⊗[R] S) =
        (TensorProduct.map (.id T T) (TensorProduct.lmul' R)).comp e.toAlgHom := by
      ext <;> simp [e, TensorProduct.one_def]
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
rw :
  RingHom.Flat (R := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (S := T ⊗[R] S)
    (AlgHom.toRingHom (R := T)
      (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
        (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S))))
⊢ RingHom.Flat (R := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (S := T ⊗[R] S) (AlgHom.toRingHom (TensorProduct.lmul' T))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
⊢ RingHom.Flat (R := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (S := T ⊗[R] S)
    (AlgHom.toRingHom (R := T)
      (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
        (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S))))

Tactic:
.comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)

Premises used: RingHom.Flat.tensorProductMap, RingHom.Flat.comp, AlgEquiv.bijective, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
refine_1 : RingHom.Flat (AlgHom.toRingHom (AlgHom.id T T))
refine_2 : RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))
⊢ RingHom.Flat (R := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (S := T ⊗[R] S)
    (AlgHom.toRingHom (R := T)
      (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
        (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S))))

Tactic:
refine .comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
⊢ RingHom.Flat (AlgHom.toRingHom (AlgHom.id T T))

Tactic:
.of_bijective Function.bijective_id

Premises used: Function.bijective_id, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
⊢ RingHom.Flat (AlgHom.toRingHom (AlgHom.id T T))

Tactic:
exact .of_bijective Function.bijective_id
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))

Tactic:
WeaklyEtale.flat_lmul' R S

Premises used: Algebra.WeaklyEtale.flat_lmul'
-- Module: Mathlib.RingTheory.Etale.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S) :=
  AlgEquiv.trans (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] S ⊗[R] S)
    (TensorProduct.assoc R R T T S S : T ⊗[R] S ⊗[R] S ≃ₐ[T] TensorProduct.{u_1, u_3, u_2} R T (S ⊗[R] S))
this :
  Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] S) (TensorProduct.lmul' T)
    (AlgHom.comp (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R))
      (↑e : T ⊗[R] S ⊗[T] (T ⊗[R] S) →ₐ[T] T ⊗[R] (S ⊗[R] S)))
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))

Tactic:
exact WeaklyEtale.flat_lmul' R S

Premises used: Algebra.WeaklyEtale.flat_lmul'
-- 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 R S
inst_8 : WeaklyEtale S T
rw :
  WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S) →
    WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T) →
      WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ WeaklyEtale R T

Tactic:
rw [← ulift_iff.{max u₁ u₂ u₃, max u₁ u₂ u₃}] at *
-- 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)
⊢ WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T)

Tactic:
⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩

Premises used: ULift, Algebra.WeaklyEtale.mk, Module.Flat.trans
-- 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)
refine :
  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)))
⊢ WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T)

Tactic:
refine ⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩
-- 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 (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)) TensorProduct.includeLeft :
          (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.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.includeLeft :
          (a : ULift.{max u₁ u₂ u₃, u₃} T) → ULift.{max u₁ u₂ u₃, u₃} T)
        x))

Tactic:
simp