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)
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:
exact aeval_X _

Premises used: Polynomial.aeval_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] A : (a : R[X]) → A) X = a
⊢ HSMul.hSMul.{u, v, v} (α := R[X]) (β := A) X 1 = a

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] A : (a : R[X]) → A) X = a

Tactic:
aeval_X _

Premises used: Polynomial.aeval_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)
⊢ (algebraMap R[X] A : (a : R[X]) → A) X = a

Tactic:
exact aeval_X _

Premises used: Polynomial.aeval_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)
⊢ gab.range ≤ fa.range ⊓ fb.range

Tactic:
have key2 : gab.range ≤ fa.range ⊓ fb.range := by
    simp_rw [gab, ga, ← aeval_algHom]
    rw [Algebra.TensorProduct.includeLeft_apply, ← Algebra.adjoin_singleton_eq_range_aeval]
    simp_rw [Algebra.adjoin_le_iff, Set.singleton_subset_iff, Algebra.coe_inf, Set.mem_inter_iff,
      AlgHom.coe_range, Set.mem_range]
    refine ⟨⟨a, by simp [fa]⟩, ⟨b, hf ?_⟩⟩
    simp_rw [fb, Algebra.TensorProduct.includeRight_apply, f,
      Algebra.TensorProduct.mapOfCompatibleSMul_tmul]
    convert! ← (TensorProduct.smul_tmul (R := R[X]) (R' := R[X]) (M := A) (N := B) X 1 1).symm <;>
      (simp_rw [Algebra.smul_def, mul_one]; exact aeval_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)
key2 : gab.range ≤ fa.range ⊓ fb.range
⊢ lift.{max v w, u} (Module.rank R R[X]) ≤ lift.{u, max v w} (Module.rank R ↥(fa.range ⊓ fb.range))

Tactic:
have key3 := (Subalgebra.inclusion key2).comp (AlgEquiv.ofInjective gab htab).toAlgHom
    |>.toLinearMap.lift_rank_le_of_injective
      ((Subalgebra.inclusion_injective key2).comp (AlgEquiv.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)
key2 : gab.range ≤ fa.range ⊓ fb.range
key3 : lift.{max v w, u} (Module.rank R R[X]) ≤ lift.{u, max v w} (Module.rank R ↥(fa.range ⊓ fb.range))
⊢ Module.rank R R[X] = lift.{u, 0} #ℕ

Tactic:
have := lift_uzero.{u} _ ▸ (basisMonomials R).mk_eq_rank.symm
-- 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_6 : 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)
key2 : gab.range ≤ fa.range ⊓ fb.range
key3 : lift.{max v w, u} (Module.rank R R[X]) ≤ lift.{u, max v w} (Module.rank R ↥(fa.range ⊓ fb.range))
this : Module.rank R R[X] = lift.{u, 0} #ℕ
⊢ ℵ₀ ≤ Module.rank R ↥(fa.range ⊓ fb.range)

Tactic:
simp only [this, mk_eq_aleph0, lift_aleph0, aleph0_le_lift] at key3

Premises used: Cardinal.mk_eq_aleph0, Cardinal.aleph0_le_lift, Cardinal.lift_aleph0
-- 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_6 : 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)
key2 : gab.range ≤ fa.range ⊓ fb.range
this : Module.rank R R[X] = lift.{u, 0} #ℕ
key3 : ℵ₀ ≤ Module.rank R ↥(fa.range ⊓ fb.range)
⊢ False

Tactic:
(key3.trans key1).not_gt one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, LE.le.not_gt, LE.le.trans
-- 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_6 : 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)
key2 : gab.range ≤ fa.range ⊓ fb.range
this : Module.rank R R[X] = lift.{u, 0} #ℕ
key3 : ℵ₀ ≤ Module.rank R ↥(fa.range ⊓ fb.range)
⊢ False

Tactic:
exact (key3.trans key1).not_gt one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, LE.le.not_gt, LE.le.trans
-- 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
H : IsField (A ⊗[R] B)
by_contra! : ∀ (h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B), False
⊢ Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

Tactic:
by_contra! h
-- 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
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ Algebra.Transcendental R A ∧ Algebra.Transcendental R B

Tactic:
simp_rw [← Algebra.transcendental_iff_not_isAlgebraic] at h

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- 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
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ Algebra.Transcendental R A

Tactic:
obtain ⟨_, _⟩ := h
-- 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
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
left : Algebra.Transcendental R A
⊢ Algebra.Transcendental R B

Tactic:
obtain ⟨_, _⟩ := h
-- 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
H : IsField (A ⊗[R] B)
left : Algebra.Transcendental R A
right : Algebra.Transcendental R B
⊢ False

Tactic:
Algebra.TensorProduct.not_isField_of_transcendental R A B H

Premises used: Algebra.TensorProduct.not_isField_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
H : IsField (A ⊗[R] B)
left : Algebra.Transcendental R A
right : Algebra.Transcendental R B
⊢ False

Tactic:
exact Algebra.TensorProduct.not_isField_of_transcendental R A B H

Premises used: Algebra.TensorProduct.not_isField_of_transcendental
-- 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
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_of_inj hf (fun _ _ ↦ mul_comm _ _) hinj

Premises used: Set.Mem, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, mul_comm, 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
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_left_of_inj (fun _ _ ↦ mul_comm _ _) hinj

Premises used: Set.Mem, mul_comm, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, Subtype.val