awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)
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)
⊢ 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:
convert_to (((Algebra.TensorProduct.comm _ _ _).trans
      (Algebra.TensorProduct.cancelBaseChange R S S S' T)).toAlgHom.comp
    Algebra.TensorProduct.includeLeft).Finite

Premises used: AlgHom.Finite, AlgEquiv.toAlgHom, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.comm, AlgEquiv.trans, Algebra.TensorProduct.cancelBaseChange, AlgHom.comp
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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 :
  ∀ (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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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'
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:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)
    (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:
(RingEquiv.finite _).comp (finite_algebraMap.mpr inferInstance)

Premises used: Iff.mpr, AlgHom.Finite, RingHom.Finite.comp, inferInstance, RingHom.finite_algebraMap, RingEquiv.finite
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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)
    (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:
exact (RingEquiv.finite _).comp (finite_algebraMap.mpr inferInstance)

Premises used: Iff.mpr, RingHom.Finite.comp, inferInstance, RingHom.finite_algebraMap, RingEquiv.finite
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
⊢ Finite (A := TensorProduct R S T) (B := 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))))))

Tactic:
RingHom.Finite.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite |>.comp <|
        RingHom.Finite.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite

Premises used: _private.0.RingHom.Finite.tensorProductMap_id, RingHom.Finite.comp, RingEquiv.finite
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
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')
⊢ 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))))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_toRingHom, AlgEquiv.toRingEquiv_toRingHom, AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
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')
⊢ 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:
congr
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
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:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Finite
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
x : T
⊢ Eq (α := TensorProduct R S' T')
    ((AlgHom.comp (B := TensorProduct R S T)
            (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T'))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (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'))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
s : S
⊢ (includeLeftSubRight R S : (a : S) → S ⊗[R] S) s = HSub.hSub (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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)
⊢ 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

Premises used: Set.mem_range, Iff.mp
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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:
simp [← hr, algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
r : R
⊢ Eq (α := S ⊗[R] S) ((includeLeftSubRight R S : (a : S) → S ⊗[R] S) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] S)
    (0 : S ⊗[R] S)

Tactic:
includeLeftSubRight_zero_of_mem_range (Set.mem_range.mp (exists_apply_eq_apply _ _))

Premises used: Set.mem_range, Iff.mp, Algebra.TensorProduct.includeLeftSubRight_zero_of_mem_range, exists_apply_eq_apply
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
x : T ⊗[R] S
⊢ Eq (α := T ⊗[R] S ⊗[T] (T ⊗[R] S))
    ((TensorProduct.AlgebraTensorModule.distribBaseChange R T S S : (a : T ⊗[R] (S ⊗[R] S)) → T ⊗[R] S ⊗[T] (T ⊗[R] S))
        ((LinearMap.lTensor T (includeLeftSubRight R S) : (a : T ⊗[R] S) → T ⊗[R] (S ⊗[R] S)) x) :
      T ⊗[R] S ⊗[T] (T ⊗[R] S))
    ((includeLeftSubRight T (T ⊗[R] S) : (a : T ⊗[R] S) → T ⊗[R] S ⊗[T] (T ⊗[R] S)) x : T ⊗[R] S ⊗[T] (T ⊗[R] S))

Tactic:
congr($(distribBaseChange_comp_includeLeftSubRight _) x)

Premises used: congrArg, id, Algebra.TensorProduct.distribBaseChange_comp_includeLeftSubRight, DFunLike.coe
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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
⊢ (↑(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)

Tactic:
ext s
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
h_1 : Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)) s
w : R
hr : (algebraMap R S : (a : R) → S) w = s
⊢ s ∈
    (↑(RingHom.eqLocus (S := S ⊗[R] S) TensorProduct.includeLeftRingHom (AlgHom.toRingHom TensorProduct.includeRight)) :
      Set S)

Tactic:
simp [← hr]
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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
⊢ 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]⟩
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
hs :
  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:
(h s).mp <| (TensorProduct.includeLeftSubRight_apply (R := R) s).symm ▸ sub_eq_zero.mpr hs

Premises used: Iff.mpr, Set.Mem, sub_eq_zero, Eq.rec, Iff.mp, Eq.symm, Algebra.TensorProduct.includeLeftSubRight_apply
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
hs :
  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:
exact (h s).mp <| (TensorProduct.includeLeftSubRight_apply (R := R) s).symm ▸ sub_eq_zero.mpr hs

Premises used: Iff.mp
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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

Tactic:
⟨?_, TensorProduct.includeLeftSubRight_zero_of_mem_range⟩

Premises used: Iff.intro, Algebra.TensorProduct.includeLeftSubRight_zero_of_mem_range
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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
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
⊢ 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⟩
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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 : (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) = s
⊢ Membership.mem (γ := Set S) (Set.range.{u_2, u_1 + 1} (ι := R) (⇑(Algebra.linearMap R S) : (a : R) → S)) s

Tactic:
use g s

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
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)
    ((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)
⊢ (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) = s

Tactic:
apply (TensorProduct.lid R S).symm.injective

Premises used: AlgEquiv.symm, Algebra.TensorProduct.lid, AlgEquiv.injective