awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
⊢ IsPushout R S R' S' ↔ IsPushout R R' S S'

Tactic:
⟨Algebra.IsPushout.symm, Algebra.IsPushout.symm⟩

Premises used: Iff.intro, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
x : S
⊢ Eq.{v₃ + 1} (α := S) ((TensorProduct.lid R S : (a : R ⊗[R] S) → S) (1 ⊗ₜ[R] x) : S)
    ((AlgHom.toLinearMap (toAlgHom R S S) : (a : S) → S) x : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
⊢ Algebra.IsPushout R S R S

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
M : Type v₁
N : Type v₂
S_1 : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R_1
inst_3 : CommSemiring S_1
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 M
inst_6 : Module R_1 N
inst_7 : Module S_1 N
inst_8 : IsScalarTower R_1 S_1 N
f : M →ₗ[R_1] N
h : IsBaseChange S_1 f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R_1 P
inst_11 : AddCommMonoid Q
inst_12 : Module S_1 Q
inst_13 : Module R_1 Q
inst_14 : IsScalarTower R_1 S_1 Q
f' : P →ₗ[R_1] Q
T_1 : Type u_4
O : Type u_5
inst_15 : CommSemiring T_1
inst_16 : Algebra R_1 T_1
inst_17 : Algebra S_1 T_1
inst_18 : IsScalarTower R_1 S_1 T_1
inst_19 : AddCommMonoid O
inst_20 : Module R_1 O
inst_21 : Module S_1 O
inst_22 : Module T_1 O
inst_23 : IsScalarTower S_1 T_1 O
inst_24 : IsScalarTower R_1 S_1 O
inst_25 : IsScalarTower R_1 T_1 O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R_1 R'
inst_29 : Algebra S_1 S'
inst_30 : Algebra R' S'
inst_31 : Algebra R_1 S'
inst_32 : IsScalarTower R_1 R' S'
inst_33 : IsScalarTower R_1 S_1 S'
R : Type u_8
S : Type u_9
T : Type u_10
inst_34 : CommSemiring R
inst_35 : CommSemiring S
inst_36 : CommSemiring T
inst_37 : Algebra R S
inst_38 : Algebra R T
⊢ Algebra.IsPushout R S T (S ⊗[R] T)

Tactic:
⟨TensorProduct.isBaseChange R T S⟩

Premises used: Algebra.IsPushout.mk, TensorProduct.isBaseChange
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
M : Type v₁
N : Type v₂
S_1 : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R_1
inst_3 : CommSemiring S_1
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 M
inst_6 : Module R_1 N
inst_7 : Module S_1 N
inst_8 : IsScalarTower R_1 S_1 N
f : M →ₗ[R_1] N
h : IsBaseChange S_1 f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R_1 P
inst_11 : AddCommMonoid Q
inst_12 : Module S_1 Q
inst_13 : Module R_1 Q
inst_14 : IsScalarTower R_1 S_1 Q
f' : P →ₗ[R_1] Q
T_1 : Type u_4
O : Type u_5
inst_15 : CommSemiring T_1
inst_16 : Algebra R_1 T_1
inst_17 : Algebra S_1 T_1
inst_18 : IsScalarTower R_1 S_1 T_1
inst_19 : AddCommMonoid O
inst_20 : Module R_1 O
inst_21 : Module S_1 O
inst_22 : Module T_1 O
inst_23 : IsScalarTower S_1 T_1 O
inst_24 : IsScalarTower R_1 S_1 O
inst_25 : IsScalarTower R_1 T_1 O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R_1 R'
inst_29 : Algebra S_1 S'
inst_30 : Algebra R' S'
inst_31 : Algebra R_1 S'
inst_32 : IsScalarTower R_1 R' S'
inst_33 : IsScalarTower R_1 S_1 S'
R : Type u_8
S : Type u_9
T : Type u_10
inst_34 : CommSemiring R
inst_35 : CommSemiring S
inst_36 : CommSemiring T
inst_37 : Algebra R S
inst_38 : Algebra R T
⊢ Algebra.IsPushout R T S (S ⊗[R] T)

Tactic:
Algebra.IsPushout.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
out : IsBaseChange (M := A ⊗[R] S) (N := B ⊗[R] S) B (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
⊢ IsPushout A B (A ⊗[R] S) (B ⊗[R] S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
⊢ IsBaseChange (M := A ⊗[R] S) (N := B ⊗[R] S) B
    (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id : A ⊗[R] S →ₗ[A] B ⊗[R] S)

Tactic:
isBaseChange_tensorProduct_map (R := R) (P := S) _ (IsBaseChange.linearMap A B)

Premises used: isBaseChange_tensorProduct_map, IsBaseChange.linearMap
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h_1 : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
h :
  Eq (α := AddCommMonoid (A ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid →
    Eq (α := AddCommMonoid (B ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid →
      HEq (α := Module A (A ⊗[R] S)) toModule (β := Module A (A ⊗[R] S)) leftModule →
        HEq (α := Module A (B ⊗[R] S)) toModule (β := Module A (B ⊗[R] S)) leftModule →
          Eq (α := A ⊗[R] S →ₗ[A] B ⊗[R] S) (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
            (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)
⊢ IsBaseChange (M := A ⊗[R] S) (N := B ⊗[R] S) B (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))

Tactic:
convert! isBaseChange_tensorProduct_map (R := R) (P := S) _ (IsBaseChange.linearMap A B)

Premises used: isBaseChange_tensorProduct_map, IsBaseChange.linearMap
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h_1 : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
e_5 : Eq (α := AddCommMonoid (A ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_6 : Eq (α := AddCommMonoid (B ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_10 : HEq (α := Module A (A ⊗[R] S)) toModule (β := Module A (A ⊗[R] S)) leftModule
e_11 : HEq (α := Module A (B ⊗[R] S)) toModule (β := Module A (B ⊗[R] S)) leftModule
h :
  ∀ (s : S),
    Eq (α := B ⊗[R] S)
      ((((AlgebraTensorModule.curry (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S))) :
                  A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
                (a : A) → S →ₗ[R] B ⊗[R] S)
              1 :
            (a : S) → B ⊗[R] S)
          s :
        B ⊗[R] S)
      ((((AlgebraTensorModule.curry (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id) :
                  A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
                (a : A) → S →ₗ[R] B ⊗[R] S)
              1 :
            (a : S) → B ⊗[R] S)
          s :
        B ⊗[R] S)
⊢ Eq (α := A ⊗[R] S →ₗ[A] B ⊗[R] S) (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)))
    (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)

Tactic:
ext s
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : IsScalarTower R A B
inst_8 : Algebra R S
x : Algebra (A ⊗[R] S) (B ⊗[R] S)
h : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H :
  Eq (α := S →+* B ⊗[R] S)
    (@RingHom.comp _ (A ⊗[R] S) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⊗[R] S) (B ⊗[R] S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
e_5 : Eq (α := AddCommMonoid (A ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_6 : Eq (α := AddCommMonoid (B ⊗[R] S)) NonUnitalNonAssocSemiring.toAddCommMonoid addCommMonoid
e_10 : HEq (α := Module A (A ⊗[R] S)) toModule (β := Module A (A ⊗[R] S)) leftModule
e_11 : HEq (α := Module A (B ⊗[R] S)) toModule (β := Module A (B ⊗[R] S)) leftModule
s : S
⊢ Eq (α := B ⊗[R] S)
    ((((AlgebraTensorModule.curry (AlgHom.toLinearMap (toAlgHom A (A ⊗[R] S) (B ⊗[R] S))) : A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
              (a : A) → S →ₗ[R] B ⊗[R] S)
            1 :
          (a : S) → B ⊗[R] S)
        s :
      B ⊗[R] S)
    ((((AlgebraTensorModule.curry (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id) :
                A →ₗ[A] S →ₗ[R] B ⊗[R] S) :
              (a : A) → S →ₗ[R] B ⊗[R] S)
            1 :
          (a : S) → B ⊗[R] S)
        s :
      B ⊗[R] S)

Tactic:
simpa using congr($H s)
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
A : Type u_8
inst_12 : Semiring A
inst_13 : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H :
  ∀ (x : S) (y : R'),
    HMul.hMul (α := A) (β := A) ((f : (a : S) → A) x : A) ((g : (a : R') → A) y : A) =
      HMul.hMul (α := A) (β := A) ((g : (a : R') → A) y : A) ((f : (a : S) → A) x : A)
x : S
⊢ Eq.{u_8 + 1} (α := A) ((pushoutDesc S' f g H : (a : S') → A) ((algebraMap S S' : (a : S) → S') x : S') : A)
    ((f : (a : S) → A) x : A)

Tactic:
simp [Algebra.pushoutDesc_apply]

Premises used: Algebra.pushoutDesc_apply
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
A : Type u_8
inst_12 : Semiring A
inst_13 : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H :
  ∀ (x : S) (y : R'),
    HMul.hMul (α := A) (β := A) ((f : (a : S) → A) x : A) ((g : (a : R') → A) y : A) =
      HMul.hMul (α := A) (β := A) ((g : (a : R') → A) y : A) ((f : (a : S) → A) x : A)
⊢ AlgHom.comp (pushoutDesc S' f g H) (toAlgHom R S S') = f

Tactic:
AlgHom.ext fun x => (Algebra.pushoutDesc_left S' f g H x :)

Premises used: AlgHom.ext, Algebra.pushoutDesc_left
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
A : Type u_8
inst_12 : Semiring A
inst_13 : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H :
  ∀ (x : S) (y : R'),
    HMul.hMul (α := A) (β := A) ((f : (a : S) → A) x : A) ((g : (a : R') → A) y : A) =
      HMul.hMul (α := A) (β := A) ((g : (a : R') → A) y : A) ((f : (a : S) → A) x : A)
x : R'
⊢ Eq.{u_8 + 1} (α := A) ((pushoutDesc S' f g H : (a : S') → A) ((algebraMap R' S' : (a : R') → S') x : S') : A)
    ((g : (a : R') → A) x : A)

Tactic:
simp [Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right]

Premises used: Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
A : Type u_8
inst_12 : Semiring A
inst_13 : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H :
  ∀ (x : S) (y : R'),
    HMul.hMul (α := A) (β := A) ((f : (a : S) → A) x : A) ((g : (a : R') → A) y : A) =
      HMul.hMul (α := A) (β := A) ((g : (a : R') → A) y : A) ((f : (a : S) → A) x : A)
⊢ AlgHom.comp (pushoutDesc S' f g H) (toAlgHom R R' S') = g

Tactic:
AlgHom.ext fun x => (Algebra.pushoutDesc_right S' f g H x :)

Premises used: Algebra.pushoutDesc_right, AlgHom.ext
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
H₁ : ∀ (x : S'), Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)

Tactic:
H.1.inductionOn x _ ?_ ?_ ?_ ?_

Premises used: IsBaseChange.inductionOn, Algebra.IsPushout.out, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
H₁ : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)
H₂ :
  ∀ (m : R'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
      ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
H₃ :
  ∀ (s : S) (n : S'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n : A) ((g : (a : S') → A) n : A) →
      Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s • n) : A) ((g : (a : S') → A) (s • n) : A)
H₄ :
  ∀ (n₁ n₂ : S'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n₁ : A) ((g : (a : S') → A) n₁ : A) →
      Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) n₂ : A) ((g : (a : S') → A) n₂ : A) →
        Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (n₁ + n₂) : A) ((g : (a : S') → A) (n₁ + n₂) : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) x : A) ((g : (a : S') → A) x : A)

Tactic:
refine H.1.inductionOn x _ ?_ ?_ ?_ ?_
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) 0 : A) ((g : (a : S') → A) 0 : A)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
⊢ ∀ (m : R'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
      ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)

Tactic:
AlgHom.congr_fun h₁

Premises used: AlgHom.congr_fun
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
⊢ ∀ (m : R'),
    Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)
      ((g : (a : S') → A) ((AlgHom.toLinearMap (toAlgHom R R' S') : (a : R') → S') m : S') : A)

Tactic:
exact AlgHom.congr_fun h₁

Premises used: AlgHom.congr_fun
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
H₁ :
  HMul.hMul (α := A) (β := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A) =
    HMul.hMul (α := A) (β := A) ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A)
⊢ Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) (s • s') : A) ((g : (a : S') → A) (s • s') : A)

Tactic:
rw [Algebra.smul_def, map_mul, map_mul, e]

Premises used: map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
S : Type v₃
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_6
S' : Type u_7
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst_11 : Semiring A
inst_12 : Algebra R A
f g : S' →ₐ[R] A
h₁ : Eq (α := R' →ₐ[R] A) (f.comp (toAlgHom R R' S')) (g.comp (toAlgHom R R' S'))
h₂ : Eq (α := S →ₐ[R] A) (f.comp (toAlgHom R S S')) (g.comp (toAlgHom R S S'))
x : S'
s : S
s' : S'
e : Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) s' : A) ((g : (a : S') → A) s' : A)
H₁ :
  Eq.{u_8 + 1} (α := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
    ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
⊢ HMul.hMul (α := A) (β := A) ((f : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A) =
    HMul.hMul (α := A) (β := A) ((g : (a : S') → A) ((algebraMap S S' : (a : S) → S') s : S') : A)
      ((g : (a : S') → A) s' : A)

Tactic:
congr 1