awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring 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
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
⊢ Module.rank R ↥(A ⊓ B) = 1
have refine : 1 ≤ Module.rank R ↥(A ⊓ B)
Tactic: refine le_antisymm (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat H hf hc) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring 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
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
have this : Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)
Tactic: have : Cardinal.lift.{u} (Module.rank R (⊥ : Subalgebra R S)) =
      Cardinal.lift.{v} (Module.rank R R) :=
    lift_rank_range_of_injective (Algebra.linearMap R S) hinj
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring 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
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
have this₁ : Module.rank R ↥⊥ = 1
Tactic: rw [Module.rank_self, Cardinal.lift_one, Cardinal.lift_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring 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
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
have rw : Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring 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
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)
have change : Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ≤
  Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊓ B) : Submodule R S)
Tactic: change Module.rank R (toSubmodule (⊥ : Subalgebra R S)) ≤
    Module.rank R (toSubmodule (A ⊓ B))
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst_3 : Flat.{u, v} R ↥A
hc : ∀ (a b : ↥A), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥A = 1
have rw : ∀ (hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S))
  (hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
  Module.rank R ↥(A ⊓ A) = 1
Tactic: rw [← inf_of_le_left (le_refl A)] at hc ⊢
Cleared hypotheses: hc, hinj
-- 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
H' : A ⊔ B = ⊤
inst_3 : Free.{u, v} R ↥B
inst_4 : Module.Finite.{u, v} R ↥B
x : ↥B
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.trace R ↥B : (a : ↥B) → R) x) : ↥A)
have simp_rw : Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
  ((algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.trace.{v, u} (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)
Tactic: simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
    Matrix.diag_apply, Matrix.map_apply]
-- 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
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.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.trace.{v, u} (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)
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.trace R ↥B : (a : ↥B) → R) x) : ↥A)
have simp_rw₁ : Eq.{v + 1} (α := ↥A)
  (Matrix.trace (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.trace.{v, u} (n := Free.ChooseBasisIndex R ↥B)
      ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
          (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
        x)))
Tactic: simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
    Matrix.diag_apply, Matrix.map_apply]
-- 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
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.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.trace.{v, u} (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.trace (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.trace.{v, u} (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.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.trace R ↥B : (a : ↥B) → R) x) : ↥A)
have simp_rw₂ : Eq.{v + 1} (α := ↥A)
  (∑ i : Free.ChooseBasisIndex R ↥B,
    Matrix.diag
      ((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))
      i)
  ((algebraMap R ↥A : (a : R) → ↥A)
    (∑ i : Free.ChooseBasisIndex R ↥B,
      Matrix.diag
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)
        i))
Tactic: simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
    Matrix.diag_apply, Matrix.map_apply]
-- 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
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.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.trace.{v, u} (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.trace (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.trace.{v, u} (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)
    (∑ i : Free.ChooseBasisIndex R ↥B,
      Matrix.diag
        ((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))
        i)
    ((algebraMap R ↥A : (a : R) → ↥A)
      (∑ i : Free.ChooseBasisIndex R ↥B,
        Matrix.diag
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)
          i))
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.trace R ↥B : (a : ↥B) → R) x) : ↥A)
have simp_rw₃ : Eq.{v + 1} (α := ↥A)
  (∑ i : Free.ChooseBasisIndex R ↥B,
    Matrix.diag
      ((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))
      i)
  (∑ x_1 : Free.ChooseBasisIndex R ↥B,
    (algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.diag
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)
        x_1))
Tactic: simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
    Matrix.diag_apply, Matrix.map_apply]
-- 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
H' : A ⊔ B = ⊤
inst_3 : Free.{u, v} R ↥B
inst_4 : Module.Finite.{u, v} R ↥B
x : ↥B
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)))
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]
-- 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
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)))
⊢ 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)
have 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)))
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]
-- 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 : IsField.{v} (↥A ⊗[R] ↥B)
⊢ A.LinearDisjoint B
have a : Nontrivial S
Tactic: nontriviality S
-- 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 : IsField.{v} (↥A ⊗[R] ↥B)
h : Nontrivial S
⊢ A.LinearDisjoint B
have rw : Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)
Tactic: rw [linearDisjoint_iff_injective]
-- 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 : 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)
⊢ fa.range.LinearDisjoint fb.range
have H₁ : IsField.{v} (↥fa.range ⊗[R] ↥fb.range)
Tactic: apply of_isField
-- 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 : Field (A ⊗[R] B) := H.toField
⊢ False
have obtain : ∀ (a : A) (hta : Transcendental R a), False
Tactic: obtain ⟨a, hta⟩ := ‹Algebra.Transcendental R A›
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
⊢ False
have obtain : ∀ (b : B) (htb : Transcendental R b), False
Tactic: obtain ⟨b, htb⟩ := ‹Algebra.Transcendental R B›
-- 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 : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
⊢ False
have ha : 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
-- 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 : 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)
⊢ False
have hb : 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
-- 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 : 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
⊢ False
have hfa : Function.Injective (α := A) (β := A ⊗[R] B) (⇑fa : (a : A) → A ⊗[R] B)
Tactic: have hfa : Function.Injective fa := Algebra.TensorProduct.includeLeft_injective hb
-- 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 : 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)
⊢ False
have hfb : Function.Injective (α := B) (β := A ⊗[R] B) (⇑fb : (a : B) → A ⊗[R] B)
Tactic: have hfb : Function.Injective fb := Algebra.TensorProduct.includeRight_injective ha
-- 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 : 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)
⊢ False
have this₁ : IsDomain A
Tactic: haveI := hfa.isDomain fa.toRingHom