awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
⊢ Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)

Tactic:
have hf : Function.Injective f := RingHom.injective _
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
simp_rw : AlgHom.range (A := R[X]) (aeval ((fa : (a : A) → A ⊗[R] B) a)) ≤ fa.range ⊓ fb.range
⊢ gab.range ≤ fa.range ⊓ fb.range

Tactic:
simp_rw [gab, ga, ← aeval_algHom]

Premises used: Polynomial.aeval_algHom
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
rw : R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range
⊢ AlgHom.range (A := R[X]) (aeval ((fa : (a : A) → A ⊗[R] B) a)) ≤ fa.range ⊓ fb.range

Tactic:
rw [Algebra.TensorProduct.includeLeft_apply, ← Algebra.adjoin_singleton_eq_range_aeval]

Premises used: Algebra.TensorProduct.includeLeft_apply, Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
simp_rw :
  (∃ (y : A), Eq (α := A ⊗[R] B) ((fa : (a : A) → A ⊗[R] B) y : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)) ∧
    ∃ (y : B), Eq (α := A ⊗[R] B) ((fb : (a : B) → A ⊗[R] B) y : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)
⊢ R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range

Tactic:
simp_rw [Algebra.adjoin_le_iff, Set.singleton_subset_iff, Algebra.coe_inf, Set.mem_inter_iff,
      AlgHom.coe_range, Set.mem_range]

Premises used: Set.singleton_subset_iff, Set.mem_range, AlgHom.coe_range, Set.mem_inter_iff, Algebra.adjoin_le_iff, Algebra.coe_inf
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
⊢ Eq (α := A ⊗[R] B) ((fa : (a : A) → A ⊗[R] B) a : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)

Tactic:
simp [fa]
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
refine :
  Eq (α := TensorProduct.{u, v, w} R[X] A B)
    ((f : (a : A ⊗[R] B) → A ⊗[R[X]] B) ((fb : (a : B) → A ⊗[R] B) b) : TensorProduct.{u, v, w} R[X] A B)
    ((f : (a : A ⊗[R] B) → A ⊗[R[X]] B) (a ⊗ₜ[R] 1) : TensorProduct.{u, v, w} R[X] A B)
⊢ (∃ (y : A), Eq (α := A ⊗[R] B) ((fa : (a : A) → A ⊗[R] B) y : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)) ∧
    ∃ (y : B), Eq (α := A ⊗[R] B) ((fb : (a : B) → A ⊗[R] B) y : A ⊗[R] B) (a ⊗ₜ[R] 1 : A ⊗[R] B)

Tactic:
refine ⟨⟨a, by simp [fa]⟩, ⟨b, hf ?_⟩⟩
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
simp_rw : Eq (α := TensorProduct.{u, v, w} R[X] A B) (1 ⊗ₜ[R[X]] b) (a ⊗ₜ[R[X]] 1)
⊢ Eq (α := TensorProduct.{u, v, w} R[X] A B)
    ((f : (a : A ⊗[R] B) → A ⊗[R[X]] B) ((fb : (a : B) → A ⊗[R] B) b) : TensorProduct.{u, v, w} R[X] A B)
    ((f : (a : A ⊗[R] B) → A ⊗[R[X]] B) (a ⊗ₜ[R] 1) : TensorProduct.{u, v, w} R[X] A B)

Tactic:
simp_rw [fb, Algebra.TensorProduct.includeRight_apply, f,
      Algebra.TensorProduct.mapOfCompatibleSMul_tmul]

Premises used: Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.mapOfCompatibleSMul_tmul
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
⊢ Eq (α := TensorProduct.{u, v, w} R[X] A B) (1 ⊗ₜ[R[X]] HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1)
    (HSMul.hSMul.{u, v, v} (α := R[X]) (β := A) X 1 ⊗ₜ[R[X]] 1)

Tactic:
(TensorProduct.smul_tmul (R := R[X]) (R' := R[X]) (M := A) (N := B) X 1 1).symm

Premises used: TensorProduct.smul_tmul, OfNat.ofNat, Eq.symm, Polynomial.X
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
h : HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1 = b
h₁ : HSMul.hSMul.{u, v, v} (α := R[X]) (β := A) X 1 = a
⊢ Eq (α := TensorProduct.{u, v, w} R[X] A B) (1 ⊗ₜ[R[X]] b) (a ⊗ₜ[R[X]] 1)

Tactic:
convert! ← (TensorProduct.smul_tmul (R := R[X]) (R' := R[X]) (M := A) (N := B) X 1 1).symm

Premises used: TensorProduct.smul_tmul, OfNat.ofNat, Eq.symm, Polynomial.X
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
h : (algebraMap R[X] B : (a : R[X]) → B) X = b
⊢ HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1 = b

Tactic:
simp_rw [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
B : Type w
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Flat R A
inst_6 : Flat R B
inst_7 : Algebra.Transcendental R A
inst_8 : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this_1 : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
this_2 : IsDomain A
this_3 : IsDomain B
this_4 : IsDomain R
this_5 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)
htb : Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)
htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
algInst : Algebra.{u, v} R[X] A := ga.toAlgebra
algInst_1 : Algebra.{u, w} R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] TensorProduct.{u, v, w} R[X] A B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (TensorProduct.{u, v, w} R[X] A B)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
⊢ (algebraMap R[X] B : (a : R[X]) → B) X = b

Tactic:
aeval_X _

Premises used: Polynomial.aeval_X