awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have pos : ∀ (H : length R R = ⊤),
  length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
Tactic: by_cases H : Module.length R R = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
pos :
  ∀ (H : length R R = ⊤),
    length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have neg : ∀ (H : ¬length R R = ⊤),
  length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
Tactic: by_cases H : Module.length R R = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : length R R = ⊤
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have pos : Eq (α := ℕ∞) (if ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0 then 0 else ⊤)
  (if Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞) then 0 else ⊤)
Tactic: rw [b.repr.length_eq, Module.length_finsupp, H, ENat.mul_top', ENat.mul_top']
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : length R R = ⊤
⊢ Eq (α := ℕ∞) (if ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0 then 0 else ⊤)
    (if Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞) then 0 else ⊤)
have pos : (ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0) =
  Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : ¬length R R = ⊤
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have H₁ : IsNoetherian R R ∧ IsArtinian R R
Tactic: rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : IsNoetherian R R ∧ IsArtinian R R
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have left : IsNoetherian R R
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : IsNoetherian R R ∧ IsArtinian R R
left : IsNoetherian R R
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have right : IsArtinian R R
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b_1 : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
left : IsNoetherian R R
right : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have neg : length R (Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) =
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
Tactic: rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b_1 : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
left : IsNoetherian R R
right : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
neg :
  length R (Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have neg₁ : ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
Tactic: rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b_1 : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
left : IsNoetherian R R
right : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
neg :
  length R (Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg₁ :
  ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have neg₂ : ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
    (length R R)
Tactic: rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b_1 : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
left : IsNoetherian R R
right : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
neg :
  length R (Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg₁ :
  ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg₂ :
  ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
      (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have neg₃ : HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
    (length R R) =
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
    (length R R)
Tactic: rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
inst_5 : Module.Finite R M
⊢ length R M = (↑(finrank R M) : ℕ∞) * length R R
have rw : HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R) =
  (↑(finrank R M) : ℕ∞) * length R R
Tactic: rw [length_of_free, Cardinal.toENat_eq_natCast.mpr (finrank_eq_rank _ _).symm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
inst_5 : Module.Finite R M
rw :
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R) =
    (↑(finrank R M) : ℕ∞) * length R R
⊢ length R M = (↑(finrank R M) : ℕ∞) * length R R
have rw₁ : (↑(finrank R M) : ℕ∞) * length R R = (↑(finrank R M) : ℕ∞) * length R R
Tactic: rw [length_of_free, Cardinal.toENat_eq_natCast.mpr (finrank_eq_rank _ _).symm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M = 1 ↔ IsSimpleModule R M
have rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
⊢ length R M = 1 ↔ IsSimpleModule R M
have rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
⊢ length R M = 1 ↔ IsSimpleModule R M
have rw₂ : Order.krullDim.{u_2} (Submodule R M) = 1 ↔ IsSimpleModule R M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 1 ↔ IsSimpleModule R M
⊢ length R M = 1 ↔ IsSimpleModule R M
have rw₃ : IsSimpleOrder.{u_2} (Submodule R M) ↔ IsSimpleModule R M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 1 ↔ IsSimpleModule R M
rw₃ : IsSimpleOrder.{u_2} (Submodule R M) ↔ IsSimpleModule R M
⊢ length R M = 1 ↔ IsSimpleModule R M
have rw₄ : IsSimpleOrder.{u_2} (Submodule R M) ↔ IsSimpleOrder.{u_2} (Submodule R M)
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_5
inst_3 : Ring A
inst_4 : SMul A R
inst_5 : Module A M
inst_6 : IsScalarTower A R M
p : Submodule R M
⊢ Module.length.{u_1, u_2} R ↥p ≤ Module.length.{u_5, u_2} A ↥(restrictScalars A p)
have rw : Order.krullDim.{u_2} (Submodule R ↥p) ≤ Order.krullDim.{u_2} (Submodule A ↥(restrictScalars A p))
Tactic: rw [← WithBot.coe_le_coe, Module.coe_length, Module.coe_length]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Module.length.{u_1, u_2} R (M ⧸ p) < Module.length R M
have rw : Order.coheight p < Order.coheight.{u_2} (α := Submodule R M) ⊥
Tactic: rw [Module.length_quotient, Module.length, WithBot.lt_unbot_iff, ← Order.coheight_bot_eq_krullDim,
    WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
B : Subalgebra R S
⊢ Subalgebra.LinearDisjoint ⊥ B
have rw : Submodule.LinearDisjoint.{u, v} (R := R) (S := S) 1 ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)
Tactic: rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ A.LinearDisjoint ⊥
have rw : Submodule.LinearDisjoint.{u, v} (R := R) (S := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) 1
Tactic: rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
B : Type w
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Subalgebra.LinearDisjoint (R := R) (S := A ⊗[R] B) (AlgHom.range Algebra.TensorProduct.includeLeft)
    (AlgHom.range Algebra.TensorProduct.includeRight)
have rw : Function.Injective (α :=
  ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
          (AlgHom.range Algebra.TensorProduct.includeLeft) :
        Submodule R (A ⊗[R] B)) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
          (AlgHom.range Algebra.TensorProduct.includeRight) :
        Submodule R (A ⊗[R] B)))
  (β := A ⊗[R] B)
  (⇑(Submodule.mulMap
        ((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
          (AlgHom.range Algebra.TensorProduct.includeLeft))
        ((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
          (AlgHom.range Algebra.TensorProduct.includeRight))) :
    (a :
        ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
              Algebra.TensorProduct.includeLeft.range) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
              Algebra.TensorProduct.includeRight.range)) →
      A ⊗[R] B)
Tactic: rw [Subalgebra.LinearDisjoint, Submodule.linearDisjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ A.LinearDisjoint B ↔ Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)
have rw : Function.Injective.{v + 1, v + 1} (α :=
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
    (β := S)
    (⇑(Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
          ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) :
      (a :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
        S) ↔
  Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)
Tactic: rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ Eq (α := Subalgebra (↥A) S)
    (AlgHom.range (A := ↥A ⊗[R] ↥B)
      (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S))
    ⊤
have a : Eq (α := Subalgebra R S)
  (restrictScalars R (S := ↥A)
    (AlgHom.range (A := ↥A ⊗[R] ↥B)
      (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)))
  (restrictScalars R (S := ↥A) ⊤)
Tactic: apply Subalgebra.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ Eq (α := Subalgebra R S)
    (restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)))
    (restrictScalars R (S := ↥A) ⊤)
have a : restrictScalars R (S := ↥A)
    (AlgHom.range (A := ↥A ⊗[R] ↥B)
      (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)) =
  A ⊔ B
Tactic: rw [restrictScalars_top, ← H']
-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis.{u_1, u, v} ι R ↥B
x : ↥B
⊢ Eq (α := Matrix.{u_1, u_1, v} ι ι ↥A)
    ((Algebra.leftMulMatrix (H.basisOfBasisRight H' b) : (a : S) → Matrix ι ι ↥A)
        ((algebraMap (↥B) S : (a : ↥B) → S) x) :
      Matrix.{u_1, u_1, v} ι ι ↥A)
    ((RingHom.mapMatrix (algebraMap R ↥A) : (a : Matrix ι ι R) → Matrix ι ι ↥A)
        ((Algebra.leftMulMatrix b : (a : ↥B) → Matrix ι ι R) x) :
      Matrix.{u_1, u_1, v} ι ι ↥A)
have a : ∀ (i j : ι),
  Eq.{v + 1} (α := S)
    (↑((Algebra.leftMulMatrix (H.basisOfBasisRight H' b) : (a : S) → Matrix ι ι ↥A)
          ((algebraMap (↥B) S : (a : ↥B) → S) x) i j) :
      S)
    (↑((RingHom.mapMatrix (algebraMap R ↥A) : (a : Matrix ι ι R) → Matrix ι ι ↥A)
          ((Algebra.leftMulMatrix b : (a : ↥B) → Matrix ι ι R) x) i j) :
      S)
Tactic: ext
-- 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
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
⊢ LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)
have h : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
  (LinearMap.ker
    (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) a))
  ⊥
Tactic: have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha
-- 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
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) a))
    ⊥
⊢ LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)
have rwa : ∀ (h : LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)),
  LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)
Tactic: rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at 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 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis.{u_1, u, v} ι R ↥A
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥B.op (M := Sᵐᵒᵖ)
    (MulOpposite.op ∘ Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑a : (a : ι) → ↥A))
⊢ A.LinearDisjoint B
have H₁ : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
  (LinearMap.ker
    (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑a : (a : ι) → ↥A)))
  ⊥
Tactic: rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at 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 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
⊢ LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)
have h : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
  (LinearMap.ker
    (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
      (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) b))
  ⊥
Tactic: have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb
-- 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
inst_3 : Flat.{u, v} R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
        (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) b))
    ⊥
⊢ LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)
have rwa : ∀ (h : LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)),
  LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)
Tactic: rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at 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 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis.{u_1, u, v} ι R ↥B
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥A (M := S)
    (Function.comp (β := ↥B) (⇑B.val : (a : ↥B) → S) (⇑b : (a : ι) → ↥B))
⊢ A.LinearDisjoint B
have H₁ : Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
  (LinearMap.ker
    (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
      (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑b : (a : ι) → ↥B)))
  ⊥
Tactic: rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at 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 : 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)
⊢ Module.rank R ↥(A ⊓ B) = 1
have a : Nontrivial R
Tactic: nontriviality R