awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (1 ⊗ₜ[R[X]] b) (a ⊗ₜ[R[X]] 1)
have h : HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1 = b
Tactic: convert! ← (TensorProduct.smul_tmul (R := R[X]) (R' := R[X]) (M := A) (N := B) X 1 1).symm
-- 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)
h : HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1 = b
⊢ Eq (α := TensorProduct.{u, v, w} R[X] A B) (1 ⊗ₜ[R[X]] b) (a ⊗ₜ[R[X]] 1)
have h₁ : HSMul.hSMul.{u, v, v} (α := R[X]) (β := A) X 1 = a
Tactic: convert! ← (TensorProduct.smul_tmul (R := R[X]) (R' := R[X]) (M := A) (N := B) X 1 1).symm
-- 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)
⊢ HSMul.hSMul.{u, w, w} (α := R[X]) (β := B) X 1 = b
have h : (algebraMap R[X] B : (a : R[X]) → B) X = b
Tactic: simp_rw [Algebra.smul_def, mul_one]
-- 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)
⊢ HSMul.hSMul.{u, v, v} (α := R[X]) (β := A) X 1 = a
have h : (algebraMap R[X] A : (a : R[X]) → A) X = a
Tactic: simp_rw [Algebra.smul_def, mul_one]
-- 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)
hf : Function.Injective (α := A ⊗[R] B) (β := TensorProduct.{u, v, w} R[X] A B) (⇑f : (a : A ⊗[R] B) → A ⊗[R[X]] B)
⊢ False
have key2 : 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 _)
-- 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)
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
⊢ False
have key3 : 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 _))
-- 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)
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))
⊢ False
have this₁ : Module.rank R R[X] = lift.{u, 0} #ℕ
Tactic: have := lift_uzero.{u} _ ▸ (basisMonomials R).mk_eq_rank.symm
-- 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_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} #ℕ
⊢ False
have key3₁ : ℵ₀ ≤ Module.rank R ↥(fa.range ⊓ fb.range)
Tactic: simp only [this, mk_eq_aleph0, lift_aleph0, aleph0_le_lift] at key3
Cleared hypotheses: key3
-- 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
H : IsField (A ⊗[R] B)
⊢ Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B
have by_contra! : ∀ (h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B), False
Tactic: by_contra! h
-- 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
H : IsField (A ⊗[R] B)
h : ¬Algebra.IsAlgebraic R A ∧ ¬Algebra.IsAlgebraic R B
⊢ False
have h₁ : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
Tactic: simp_rw [← Algebra.transcendental_iff_not_isAlgebraic] at h
Cleared hypotheses: h
-- 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
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ False
have left : Algebra.Transcendental R A
Tactic: obtain ⟨_, _⟩ := h
Cleared hypotheses: h
-- 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
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
left : Algebra.Transcendental R A
⊢ False
have right : Algebra.Transcendental R B
Tactic: obtain ⟨_, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
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 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
h : Nontrivial R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B
have rw : Module.rank R ↥(A ⊔ B) = Module.rank R (↥A ⊗[R] ↥B)
Tactic: rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
h : Nontrivial R
rw : Module.rank R ↥(A ⊔ B) = Module.rank R (↥A ⊗[R] ↥B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B
have rw₁ : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(A ⊔ B)
Tactic: rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Module.Finite.{u, v} R ↥A
inst_6 : Module.Finite.{u, v} R ↥B
H : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
⊢ A.LinearDisjoint B
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Module.Finite.{u, v} R ↥A
inst_6 : Module.Finite.{u, v} R ↥B
H : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
h : Nontrivial R
⊢ A.LinearDisjoint B
have H₁ : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)
Tactic: rw [← Module.finrank_tensorProduct] at H
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Module.Finite.{u, v} R ↥A
inst_6 : Module.Finite.{u, v} R ↥B
H : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)
h : Nontrivial R
⊢ A.LinearDisjoint B
have obtain : ∀ (j : Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)) (hj : LinearIndependent R j), A.LinearDisjoint B
Tactic: obtain ⟨j, hj⟩ := exists_linearIndependent_of_le_finrank H.ge
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Module.Finite.{u, v} R ↥A
inst_6 : Module.Finite.{u, v} R ↥B
H : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)
h : Nontrivial R
j : Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : LinearIndependent R j
⊢ A.LinearDisjoint B
have hj₁ : Function.Injective.{max 1 (u + 1), v + 1} (α := Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) →₀ R) (β := ↥(A ⊔ B))
  (⇑(Finsupp.linearCombination R j) : (a : Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R) → ↥(A ⊔ B))
Tactic: rw [LinearIndependent] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Module.Finite.{u, v} R ↥A
inst_6 : Module.Finite.{u, v} R ↥B
H : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)
h : Nontrivial R
j : Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj :
  Function.Injective.{max 1 (u + 1), v + 1} (α := Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) →₀ R) (β := ↥(A ⊔ B))
    (⇑(Finsupp.linearCombination R j) : (a : Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R) → ↥(A ⊔ B))
j' : ↥A ⊗[R] ↥B →ₗ[R] ↥(A ⊔ B) :=
  Finsupp.linearCombination R j ∘ₗ
    (↑(LinearEquiv.ofFinrankEq (↥A ⊗[R] ↥B) (Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) →₀ R) ⋯) :
      ↥A ⊗[R] ↥B →ₗ[R] Fin (finrank R (↥A ⊗[R] ↥B)) →₀ R)
⊢ A.LinearDisjoint B
have hj₁ : Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
Tactic: replace hj : Function.Injective j' := by simpa [j']
Cleared hypotheses: hj