awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
⊢ Nontrivial.{u_2} (M ⊗[R] M)
have this : Nontrivial.{u_1} (R ⧸ I)
Tactic: have : Nontrivial (R ⧸ I) := by rwa [Submodule.Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x : R ⧸ I
⊢ ∃ (a : M ⊗[R] M), (ψ : (a : M ⊗[R] M) → R ⧸ I) a = x
have obtain : ∀ (x : M),
  ∃ (a : M ⊗[R] M), Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)
Tactic: obtain ⟨x, rfl⟩ := hϕ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x : M
⊢ ∃ (a : M ⊗[R] M), Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)
have obtain : ∀ (y : M) (hy : Eq.{u_1 + 1} (α := R ⧸ I) ((ϕ : (a : M) → R ⧸ I) y : R ⧸ I) (1 : R ⧸ I)),
  ∃ (a : M ⊗[R] M), Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)
Tactic: obtain ⟨y, hy⟩ := hϕ 1
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
⊢ Nontrivial.{u_2} (M ⊗[R] M)
have this₁ : Surjective.{u_2 + 1, u_1 + 1} (α := M ⊗[R] M) (β := R ⧸ I) (⇑ψ : (a : M ⊗[R] M) → R ⧸ I)
Tactic: have : Function.Surjective ψ := by
    intro x; obtain ⟨x, rfl⟩ := hϕ x; obtain ⟨y, hy⟩ := hϕ 1; exact ⟨x ⊗ₜ y, by simp [ψ, hy]⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : Algebra K L
E1 E2 : Subalgebra K L
inst_3 : Module.Finite.{u_1, u_2} K ↥E1
inst_4 : Module.Finite.{u_1, u_2} K ↥E2
⊢ Module.Finite.{u_1, u_2} K ↥(E1 ⊔ E2)
have rw : Module.Finite.{u_1, u_2} K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range
Tactic: rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this : Algebra S S' := f.toAlgebra
⊢ Finite (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T) : TensorProduct R S T →ₐ[R] TensorProduct R S' T))
have this₁ : IsScalarTower R S S'
Tactic: have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (hypothesis)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Finite (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T) : TensorProduct R S T →ₐ[R] TensorProduct R S' T))
have this₁ : Module.Finite S S'
Tactic: have : Module.Finite S S' := finite_algebraMap.mp Hf
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this_2 : IsScalarTower R S S'
this : Module.Finite S S'
⊢ Finite (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T) : TensorProduct R S T →ₐ[R] TensorProduct R S' T))
have change : AlgHom.Finite (R := S) (A := TensorProduct R S T) (B := TensorProduct R S' T)
  (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))
Tactic: change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).Finite
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this_2 : IsScalarTower R S S'
this : Module.Finite S S'
⊢ AlgHom.Finite (R := S) (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))
have h : Eq (α := TensorProduct R S T →ₐ[S] TensorProduct R S' T)
  (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : TensorProduct R S T →ₐ[S] TensorProduct R S' T)
  (AlgHom.comp
      (↑(AlgEquiv.trans (Algebra.TensorProduct.comm S (TensorProduct R S T) S')
            (Algebra.TensorProduct.cancelBaseChange R S S S' T)) :
        TensorProduct S (TensorProduct R S T) S' →ₐ[S] TensorProduct R S' T)
      Algebra.TensorProduct.includeLeft :
    TensorProduct R S T →ₐ[S] TensorProduct R S' T)
Tactic: convert_to (((Algebra.TensorProduct.comm _ _ _).trans
      (Algebra.TensorProduct.cancelBaseChange R S S S' T)).toAlgHom.comp
    Algebra.TensorProduct.includeLeft).Finite
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this_2 : IsScalarTower R S S'
this : Module.Finite S S'
h :
  Eq (α := TensorProduct R S T →ₐ[S] TensorProduct R S' T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : TensorProduct R S T →ₐ[S] TensorProduct R S' T)
    (AlgHom.comp
        (↑(AlgEquiv.trans (Algebra.TensorProduct.comm S (TensorProduct R S T) S')
              (Algebra.TensorProduct.cancelBaseChange R S S S' T)) :
          TensorProduct S (TensorProduct R S T) S' →ₐ[S] TensorProduct R S' T)
        Algebra.TensorProduct.includeLeft :
      TensorProduct R S T →ₐ[S] TensorProduct R S' T)
⊢ AlgHom.Finite (R := S) (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))
have convert_to : AlgHom.Finite (R := S) (A := TensorProduct R S T) (B := TensorProduct R S' T)
  (AlgHom.comp
    (↑(AlgEquiv.trans (Algebra.TensorProduct.comm S (TensorProduct R S T) S')
          (Algebra.TensorProduct.cancelBaseChange R S S S' T)) :
      TensorProduct S (TensorProduct R S T) S' →ₐ[S] TensorProduct R S' T)
    Algebra.TensorProduct.includeLeft)
Tactic: convert_to (((Algebra.TensorProduct.comm _ _ _).trans
      (Algebra.TensorProduct.cancelBaseChange R S S S' T)).toAlgHom.comp
    Algebra.TensorProduct.includeLeft).Finite
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this_2 : IsScalarTower R S S'
this : Module.Finite S S'
⊢ Eq (α := TensorProduct R S T →ₐ[S] TensorProduct R S' T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : TensorProduct R S T →ₐ[S] TensorProduct R S' T)
    (AlgHom.comp
        (↑(AlgEquiv.trans (Algebra.TensorProduct.comm S (TensorProduct R S T) S')
              (Algebra.TensorProduct.cancelBaseChange R S S S' T)) :
          TensorProduct S (TensorProduct R S T) S' →ₐ[S] TensorProduct R S' T)
        Algebra.TensorProduct.includeLeft :
      TensorProduct R S T →ₐ[S] TensorProduct R S' T)
have h : ∀ (x : T),
  Eq (α := TensorProduct R S' T)
    ((AlgHom.comp (B := TensorProduct R S T)
            (AlgHom.restrictScalars R
              (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) :
                TensorProduct R S T →ₐ[S] TensorProduct R S' T))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T)
        x :
      TensorProduct R S' T)
    ((AlgHom.comp (B := TensorProduct R S T)
            (AlgHom.restrictScalars R
              (AlgHom.comp
                  (↑(AlgEquiv.trans (Algebra.TensorProduct.comm S (TensorProduct R S T) S')
                        (Algebra.TensorProduct.cancelBaseChange R S S S' T)) :
                    TensorProduct S (TensorProduct R S T) S' →ₐ[S] TensorProduct R S' T)
                  Algebra.TensorProduct.includeLeft :
                TensorProduct R S T →ₐ[S] TensorProduct R S' T))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T)
        x :
      TensorProduct R S' T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ Eq (α := TensorProduct R S T →+* TensorProduct R S' T')
    (AlgHom.toRingHom (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T'))
    (RingHom.comp
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T'))
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R T' S)))
        (RingHom.comp
          (AlgHom.toRingHom
            (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S))
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R S T))))))
have h : Eq (α := TensorProduct R S T →+* TensorProduct R S' T')
  (↑(Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T') :
    TensorProduct R S T →+* TensorProduct R S' T')
  (↑(AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
          (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
              (AlgHom.comp
                (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
                ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                  TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
            TensorProduct R S T →ₐ[R] TensorProduct R S T') :
        TensorProduct R S T →ₐ[R] TensorProduct R S' T') :
    TensorProduct R S T →+* TensorProduct R S' T')
Tactic: simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ Eq (α := TensorProduct R S T →+* TensorProduct R S' T')
    (↑(Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T') :
      TensorProduct R S T →+* TensorProduct R S' T')
    (↑(AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
            (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
                (AlgHom.comp
                  (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
                  ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                    TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
              TensorProduct R S T →ₐ[R] TensorProduct R S T') :
          TensorProduct R S T →ₐ[R] TensorProduct R S' T') :
      TensorProduct R S T →+* TensorProduct R S' T')
have h : Eq (α := TensorProduct R S T →ₐ[R] TensorProduct R S' T')
  (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T')
  (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
      (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
          (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
            ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
              TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
        TensorProduct R S T →ₐ[R] TensorProduct R S T') :
    TensorProduct R S T →ₐ[R] TensorProduct R S' T')
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ Eq (α := TensorProduct R S T →ₐ[R] TensorProduct R S' T')
    (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T')
    (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
        (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
            (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
              ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
          TensorProduct R S T →ₐ[R] TensorProduct R S T') :
      TensorProduct R S T →ₐ[R] TensorProduct R S' T')
have h : ∀ (x : S),
  Eq (α := TensorProduct R S' T')
    (((AlgHom.comp (B := TensorProduct R S T)
              (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T')
              (Algebra.TensorProduct.includeLeft : S →ₐ[R] TensorProduct R S T) :
            S →ₐ[R] TensorProduct R S' T') :
          (a : S) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')
    (((AlgHom.comp
              (AlgHom.comp
                (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
                (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
                    (AlgHom.comp
                      (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
                      ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                        TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
                  TensorProduct R S T →ₐ[R] TensorProduct R S T'))
              Algebra.TensorProduct.includeLeft :
            S →ₐ[R] TensorProduct R S' T') :
          (a : S) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)) s
⊢ Eq (α := S ⊗[R] S) ((includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
have obtain : ∀ (w : R) (hr : (algebraMap R S : (a : R) → S) w = s),
  Eq (α := S ⊗[R] S) ((includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
Tactic: obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
h : IsEffective R S
⊢ (↑(RingHom.eqLocus (S := S ⊗[R] S) TensorProduct.includeLeftRingHom (AlgHom.toRingHom TensorProduct.includeRight)) :
      Set S) =
    Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
have h₁ : ∀ (s : S),
  s ∈
      (↑(RingHom.eqLocus (S := S ⊗[R] S) TensorProduct.includeLeftRingHom
            (AlgHom.toRingHom TensorProduct.includeRight)) :
        Set S) ↔
    Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
h : IsEffective R S
s : S
⊢ s ∈
      (↑(RingHom.eqLocus (S := S ⊗[R] S) TensorProduct.includeLeftRingHom
            (AlgHom.toRingHom TensorProduct.includeRight)) :
        Set S) ↔
    Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)) s
have h₁ : s ∈
    (↑(RingHom.eqLocus (S := S ⊗[R] S) TensorProduct.includeLeftRingHom (AlgHom.toRingHom TensorProduct.includeRight)) :
      Set S) →
  Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)) s
Tactic: refine ⟨?_, fun ⟨_, hr⟩ ↦ by simp [← hr]⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
⊢ Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S) ↔
    Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(Algebra.linearMap R S) : (a : R) → S)) s
have refine : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S) →
  Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(Algebra.linearMap R S) : (a : R) → S)) s
Tactic: refine ⟨?_, TensorProduct.includeLeftSubRight_zero_of_mem_range⟩
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
⊢ Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(Algebra.linearMap R S) : (a : R) → S)) s
have h : (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) = s
Tactic: use g s
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
⊢ (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) = s
have h : Eq (α := R ⊗[R] S)
  ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
      ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
    R ⊗[R] S)
  ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
Tactic: apply (TensorProduct.lid R S).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
  ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₁ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
  (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]