awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw :
  (f : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) a) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
⊢ (f : (a : A) → B) (hI.dpow m (hI.dpow n a)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
have rw₁ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (↑(m.uniformBell n) : A) : B)
    ((f : (a : A) → B) (hI.dpow (m * n) a) : B) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
Tactic: rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw :
  (f : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) a) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
rw₁ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (↑(m.uniformBell n) : A) : B)
      ((f : (a : A) → B) (hI.dpow (m * n) a) : B) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
⊢ (f : (a : A) → B) (hI.dpow m (hI.dpow n a)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
have rw₂ : HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
Tactic: rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw : dpow hI f n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
Tactic: rw [dpow_def, dpow_apply' hI hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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 : dpow hI f n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
⊢ (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [dpow_def, dpow_apply' hI hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [dpow_apply hI hf hIJ hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ hquot.dpow n x = (dividedPowers hI hf hIJ hIf).dpow n x
have 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)
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ hquot.dpow n ((f : (a : A) → B) a) = (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a)
have rw : (f : (a : A) → B) (hI.dpow n 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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ hquot.dpow n ((f : (a : A) → B) a) = (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a)
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [hm.2 a ha, dpow_apply hI hf hIJ hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (hypothesis)
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))
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))
have this : Etale.{u_1, u_2} R (S ⊗[R] S)
Tactic: have : Etale R (S ⊗[R] S) := .comp _ S _
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (hypothesis)
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)
⊢ RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))
have this₁ : Etale (S ⊗[R] S) S
Tactic: have : Etale (S ⊗[R] S) S := .of_restrictScalars R _ _
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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)
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (hypothesis)
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))
⊢ RingHom.Flat (R := T ⊗[R] S ⊗[T] (T ⊗[R] S)) (S := T ⊗[R] S) (AlgHom.toRingHom (TensorProduct.lmul' T))
have 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)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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 (TensorProduct.lmul' T))
have 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))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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))))
have refine_1 : RingHom.Flat (AlgHom.toRingHom (AlgHom.id T T))
Tactic: refine .comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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))
⊢ 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))))
have refine_2 : RingHom.Flat.{u_2, u_2} (R := S ⊗[R] S) (S := S) (AlgHom.toRingHom (TensorProduct.lmul' R))
Tactic: refine .comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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
⊢ WeaklyEtale R T
have 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)
Tactic: rw [← ulift_iff.{max u₁ u₂ u₃, max u₁ u₂ u₃}] at *
Cleared hypotheses: inst_7, inst_8
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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)
have 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)))
Tactic: refine ⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
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))
have ha : ∀ (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: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (hypothesis)
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)
⊢ 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)))
have 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))
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