awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst_3 : Free.{u, v} R ↥B
inst_4 : Module.Finite.{u, v} R ↥B
x : ↥B
simp_rw :
  Eq (α := ↥A) ((Algebra.norm ↥A : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.det.{u, v} (n := Free.ChooseBasisIndex R ↥B)
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)) :
      ↥A)
simp_rw₁ :
  Eq.{v + 1} (α := ↥A)
    (Matrix.det (n := Free.ChooseBasisIndex R ↥B)
      ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B)) :
          (a : S) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
        ((algebraMap (↥B) S : (a : ↥B) → S) x : S)))
    ((algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.det.{u, v} (n := Free.ChooseBasisIndex R ↥B)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)))
simp_rw₂ :
  Eq.{v + 1} (α := ↥A)
    (Matrix.det (n := Free.ChooseBasisIndex R ↥B)
      ((RingHom.mapMatrix (algebraMap R ↥A) :
          (a : Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R) →
            Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)))
    ((algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.det.{u, v} (n := Free.ChooseBasisIndex R ↥B)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)))
⊢ Eq (α := ↥A) ((Algebra.norm ↥A : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.norm R : (a : ↥B) → R) x) : ↥A)

Tactic:
simp_rw [Algebra.norm_eq_matrix_det (Module.Free.chooseBasis R B),
    Algebra.norm_eq_matrix_det (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.map_det]

Premises used: Algebra.norm_eq_matrix_det, Membership.mem, Subtype, RingHom.map_det, Subalgebra.LinearDisjoint.basisOfBasisRight, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
⊢ LinearIndependent ↥B (M := S) ((⇑A.val : (a : ↥A) → S) ∘ a)

Tactic:
H.linearIndependent_left_of_flat_of_commute ha fun _ _ ↦ mul_comm _ _

Premises used: Set.Mem, mul_comm, Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute, Subtype.val
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis.{u_1, u, v} ι R ↥A
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥B (M := S)
    (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑a : (a : ι) → ↥A))
⊢ A.LinearDisjoint B

Tactic:
of_basis_left_of_commute A B a H fun _ _ ↦ mul_comm _ _

Premises used: mul_comm, Subtype.val, Subalgebra.LinearDisjoint.of_basis_left_of_commute
-- 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 : IsDomain (A ⊗[R] 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)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective (α := A ⊗[R] B) (β := K) (⇑i : (a : A ⊗[R] B) → K)
⊢ (i.comp Algebra.TensorProduct.includeLeft).range.LinearDisjoint (i.comp Algebra.TensorProduct.includeRight).range

Tactic:
simpa only [AlgHom.range_comp] using (include_range R A B).map i hi

Premises used: Subalgebra.LinearDisjoint.include_range, Subalgebra.LinearDisjoint.map, AlgHom.range_comp
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : IsField.{v} (↥A ⊗[R] ↥B)
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : IsField.{v} (↥A ⊗[R] ↥B)
h : Nontrivial S
rw : Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)
⊢ A.LinearDisjoint B

Tactic:
rw [linearDisjoint_iff_injective]

Premises used: Subalgebra.linearDisjoint_iff_injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : IsField.{v} (↥A ⊗[R] ↥B)
h : Nontrivial S
this_1 : Field (↥A ⊗[R] ↥B) := H.toField
this : NonAssocRing (↥A ⊗[R] ↥B) := Ring.toNonAssocRing
⊢ Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)

Tactic:
RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : IsField.{v} (↥A ⊗[R] ↥B)
h : Nontrivial S
this_1 : Field (↥A ⊗[R] ↥B) := H.toField
this : NonAssocRing (↥A ⊗[R] ↥B) := Ring.toNonAssocRing
⊢ Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)

Tactic:
exact RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type v
inst_3 : Ring A
B : Type w
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective (α := A) (β := S) (⇑fa : (a : A) → S)
hfb : Function.Injective.{w + 1, v + 1} (α := B) (β := S) (⇑fb : (a : B) → S)
H₁ : IsField.{v} (↥fa.range ⊗[R] ↥fb.range)
⊢ fa.range.LinearDisjoint fb.range

Tactic:
apply of_isField

Premises used: Subalgebra.LinearDisjoint.of_isField
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type v
inst_3 : Ring A
B : Type w
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective (α := A) (β := S) (⇑fa : (a : A) → S)
hfb : Function.Injective.{w + 1, v + 1} (α := B) (β := S) (⇑fb : (a : B) → S)
⊢ IsField.{v} (↥fa.range ⊗[R] ↥fb.range)

Tactic:
Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa)
    (AlgEquiv.ofInjective fb hfb) |>.symm.toMulEquiv.isField H

Premises used: AlgEquiv.symm, AlgEquiv.toMulEquiv, AlgEquiv.ofInjective, MulEquiv.isField, Algebra.TensorProduct.congr
-- 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 : Field (A ⊗[R] B) := H.toField
obtain : ∀ (a : A) (hta : Transcendental R a), False
⊢ False

Tactic:
obtain ⟨a, hta⟩ := ‹Algebra.Transcendental R A›

Premises used: Algebra.Transcendental
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
obtain : ∀ (b : B) (htb : Transcendental R b), False
⊢ False

Tactic:
obtain ⟨b, htb⟩ := ‹Algebra.Transcendental R B›

Premises used: Algebra.Transcendental
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
have ha : Function.Injective (algebraMap R A) := Algebra.injective_of_transcendental
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
ha : Function.Injective.{u + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Function.Injective.{u + 1, w + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)

Tactic:
have hb : Function.Injective (algebraMap R B) := Algebra.injective_of_transcendental
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R 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
⊢ Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)

Tactic:
have hfa : Function.Injective fa := Algebra.TensorProduct.includeLeft_injective hb
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R 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)
⊢ Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)

Tactic:
have hfb : Function.Injective fb := Algebra.TensorProduct.includeRight_injective ha
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R 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)
⊢ IsDomain A

Tactic:
haveI := hfa.isDomain fa.toRingHom
-- 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
hta : Transcendental R a
b : B
htb : Transcendental R 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 : IsDomain A
⊢ IsDomain B

Tactic:
haveI := hfb.isDomain fb.toRingHom
-- 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
hta : Transcendental R a
b : B
htb : Transcendental R 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 : IsDomain B
⊢ IsDomain R

Tactic:
haveI := ha.isDomain _
-- 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
hta : Transcendental R a
b : B
htb : Transcendental R 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 : IsDomain R
⊢ Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))

Tactic:
haveI : Module.Flat R (toSubmodule fa.range) :=
    .of_linearEquiv (AlgEquiv.ofInjective fa hfa).symm.toLinearEquiv
-- 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
hta : Transcendental R a
b : B
htb : Transcendental R 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 :
  Flat R ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B)) fa.range : Submodule R (A ⊗[R] B))
⊢ Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1

Tactic:
have key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1 :=
    (include_range R A B).rank_inf_le_one_of_flat_left
-- 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
hta : Transcendental R a
b : B
htb : Transcendental R 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 :
  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
⊢ Function.Injective.{u + 1, v + 1} (α := R[X]) (β := A) (⇑ga : (a : R[X]) → A)

Tactic:
replace hta : Function.Injective ga := transcendental_iff_injective.1 hta
-- 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
htb : Transcendental R 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 :
  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)
⊢ Function.Injective.{u + 1, w + 1} (α := R[X]) (β := B) (⇑gb : (a : R[X]) → B)

Tactic:
replace htb : Function.Injective gb := transcendental_iff_injective.1 htb
-- 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 :
  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)
⊢ Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)

Tactic:
have htab : Function.Injective gab := hfa.comp hta
-- 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 :
  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
⊢ Nontrivial (TensorProduct.{u, v, w} R[X] A B)

Tactic:
haveI := Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain R[X] A B hta htb