awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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
⊢ False
have this₁ : IsDomain B
Tactic: haveI := hfb.isDomain fb.toRingHom
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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
⊢ False
have this₁ : IsDomain R
Tactic: haveI := ha.isDomain _
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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
⊢ False
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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))
⊢ False
have key1 : 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
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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
⊢ False
have hta₁ : 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
Cleared hypotheses: hta
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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)
⊢ False
have htb₁ : 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
Cleared hypotheses: htb
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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)
⊢ False
have htab : Function.Injective (α := R[X]) (β := A ⊗[R] B) (⇑gab : (a : R[X]) → A ⊗[R] B)
Tactic: have htab : Function.Injective gab := hfa.comp hta
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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
⊢ False
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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)
⊢ False
have hf : 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 _
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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
have simp_rw : AlgHom.range (A := R[X]) (aeval ((fa : (a : A) → A ⊗[R] B) a)) ≤ fa.range ⊓ fb.range
Tactic: simp_rw [gab, ga, ← aeval_algHom]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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)
⊢ AlgHom.range (A := R[X]) (aeval ((fa : (a : A) → A ⊗[R] B) a)) ≤ fa.range ⊓ fb.range
have rw : R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range
Tactic: rw [Algebra.TensorProduct.includeLeft_apply, ← Algebra.adjoin_singleton_eq_range_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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)
⊢ R[a ⊗ₜ[R] 1] ≤ fa.range ⊓ fb.range
have 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)
Tactic: simp_rw [Algebra.adjoin_le_iff, Set.singleton_subset_iff, Algebra.coe_inf, Set.mem_inter_iff,
      AlgHom.coe_range, Set.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: refine ⟨⟨a, by simp [fa]⟩, ⟨b, hf ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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)
    ((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)
have simp_rw : Eq (α := TensorProduct.{u, v, w} R[X] A B) (1 ⊗ₜ[R[X]] b) (a ⊗ₜ[R[X]] 1)
Tactic: simp_rw [fb, Algebra.TensorProduct.includeRight_apply, f,
      Algebra.TensorProduct.mapOfCompatibleSMul_tmul]