awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
hj : Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
⊢ A.LinearDisjoint B
have hf : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B).toLinearMap : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
Tactic: have hf : Function.Surjective (mulMap' A B).toLinearMap := mulMap'_surjective A B
-- 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)
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)
hj : Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
hf : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B).toLinearMap : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
⊢ A.LinearDisjoint B
have this : Module.Finite.{u, v} R ↥(A ⊔ B)
Tactic: haveI := Subalgebra.finite_sup A B
-- 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
j : Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) → ↥(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)
hj : Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
hf : Function.Surjective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑(A.mulMap' B).toLinearMap : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))
this : Module.Finite.{u, v} R ↥(A ⊔ B)
⊢ A.LinearDisjoint B
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)
Tactic: rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
-- 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 : Flat.{u, v} R ↥B
inst_5 : Nontrivial R
inst_6 : Nontrivial S
⊢ Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) = Module.rank R ↥A
have rw : Module.rank ↥B
    ↥(Submodule.span (↥B)
        (Set.range fun (i : Free.ChooseBasisIndex R ↥A) ↦
          (↑((Free.chooseBasis R ↥A : (a : Free.ChooseBasisIndex R ↥A) → ↥A) i) : S))) =
  Cardinal.mk (Free.ChooseBasisIndex R ↥A)
Tactic: rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex R A,
    A.adjoin_eq_span_basis B (Module.Free.chooseBasis R A)]
-- 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 : Flat.{u, v} R ↥B
inst_5 : Nontrivial R
inst_6 : Nontrivial S
⊢ Module.rank ↥B
      ↥(Submodule.span (↥B)
          (Set.range fun (i : Free.ChooseBasisIndex R ↥A) ↦
            (↑((Free.chooseBasis R ↥A : (a : Free.ChooseBasisIndex R ↥A) → ↥A) i) : S))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
have change : Module.rank ↥B
    ↥(Submodule.span (↥B)
        (Set.range (ι := Free.ChooseBasisIndex R ↥A)
          (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
            (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A)))) =
  Cardinal.mk (Free.ChooseBasisIndex R ↥A)
Tactic: change Module.rank B (Submodule.span B (Set.range (A.val ∘ Module.Free.chooseBasis R A))) = _
-- 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 : Flat.{u, v} R ↥B
inst_5 : Nontrivial R
inst_6 : Nontrivial S
⊢ Module.rank ↥B
      ↥(Submodule.span (↥B)
          (Set.range (ι := Free.ChooseBasisIndex R ↥A)
            (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
              (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A)))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
have this : LinearIndependent (ι := Free.ChooseBasisIndex R ↥A) ↥B (M := S)
  (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A))
Tactic: have := H.linearIndependent_left_of_flat (Module.Free.chooseBasis R A).linearIndependent
-- 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 : Flat.{u, v} R ↥B
inst_5 : Nontrivial R
inst_6 : Nontrivial S
this :
  LinearIndependent (ι := Free.ChooseBasisIndex R ↥A) ↥B (M := S)
    (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A))
⊢ Module.rank ↥B
      ↥(Submodule.span (↥B)
          (Set.range (ι := Free.ChooseBasisIndex R ↥A)
            (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
              (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A)))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
have rw : Cardinal.mk
    (↑(Set.range (ι := Free.ChooseBasisIndex R ↥A)
          (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
            (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A))) :
      Type v) =
  Cardinal.mk (Free.ChooseBasisIndex R ↥A)
Tactic: rw [rank_span this, Cardinal.mk_range_eq _ this.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 B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Free.{u, v} R ↥A
inst_4 : Flat.{u, v} R ↥B
inst_5 : Nontrivial R
inst_6 : Nontrivial S
this :
  LinearIndependent (ι := Free.ChooseBasisIndex R ↥A) ↥B (M := S)
    (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A))
rw :
  Cardinal.mk
      (↑(Set.range (ι := Free.ChooseBasisIndex R ↥A)
            (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
              (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A))) :
        Type v) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
⊢ Module.rank ↥B
      ↥(Submodule.span (↥B)
          (Set.range (ι := Free.ChooseBasisIndex R ↥A)
            (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S)
              (⇑(Free.chooseBasis R ↥A) : (a : Free.ChooseBasisIndex R ↥A) → ↥A)))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
have rw₁ : Cardinal.mk (Free.ChooseBasisIndex R ↥A) = Cardinal.mk (Free.ChooseBasisIndex R ↥A)
Tactic: rw [rank_span this, Cardinal.mk_range_eq _ this.injective]
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
⊢ A.LinearDisjoint 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
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
⊢ A.LinearDisjoint B
have pos : ∀ (h1 : finrank.{u, v} R ↥A = 0), A.LinearDisjoint B
Tactic: by_cases h1 : Module.finrank R A = 0
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
pos : ∀ (h1 : finrank.{u, v} R ↥A = 0), A.LinearDisjoint B
⊢ A.LinearDisjoint B
have neg : ∀ (h1 : ¬finrank.{u, v} R ↥A = 0), A.LinearDisjoint B
Tactic: by_cases h1 : Module.finrank R A = 0
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : finrank.{u, v} R ↥A = 0
⊢ A.LinearDisjoint B
have H₁ : finrank.{u, v} R ↥B = 1
Tactic: rw [h1, Nat.coprime_zero_left] at H
Cleared hypotheses: H, h, h1
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : finrank.{u, v} R ↥B = 1
h : Nontrivial R
h1 : finrank.{u, v} R ↥A = 0
⊢ A.LinearDisjoint B
have pos : A.LinearDisjoint ⊥
Tactic: rw [eq_bot_of_finrank_one 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
⊢ A.LinearDisjoint B
have pos : ∀ (h2 : finrank.{u, v} R ↥B = 0), A.LinearDisjoint B
Tactic: by_cases h2 : Module.finrank R B = 0
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
pos : ∀ (h2 : finrank.{u, v} R ↥B = 0), A.LinearDisjoint B
⊢ A.LinearDisjoint B
have neg : ∀ (h2 : ¬finrank.{u, v} R ↥B = 0), A.LinearDisjoint B
Tactic: by_cases h2 : Module.finrank R B = 0
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
⊢ A.LinearDisjoint B
have H₁ : finrank.{u, v} R ↥A = 1
Tactic: rw [h2, Nat.coprime_zero_right] at H
Cleared hypotheses: H, h, h1, h2
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : finrank.{u, v} R ↥A = 1
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : finrank.{u, v} R ↥B = 0
⊢ A.LinearDisjoint B
have pos : Subalgebra.LinearDisjoint ⊥ B
Tactic: rw [eq_bot_of_finrank_one 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
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
inst_5 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
⊢ A.LinearDisjoint B
have this : Module.Finite.{u, v} R ↥A
Tactic: haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h1)
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this : Module.Finite.{u, v} R ↥A
⊢ A.LinearDisjoint B
have this₁ : Module.Finite.{u, v} R ↥B
Tactic: haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h2)
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this : Module.Finite.{u, v} R ↥B
⊢ A.LinearDisjoint B
have this₁ : Module.Finite.{u, v} R ↥(A ⊔ B)
Tactic: haveI := finite_sup A B
-- 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 : Free.{v, v} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inst_6 : Free.{v, v} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
H : (finrank.{u, v} R ↥A).Coprime (finrank.{u, v} R ↥B)
h : Nontrivial R
h1 : ¬finrank.{u, v} R ↥A = 0
h2 : ¬finrank.{u, v} R ↥B = 0
this_1 : Module.Finite.{u, v} R ↥A
this_2 : Module.Finite.{u, v} R ↥B
this : Module.Finite.{u, v} R ↥(A ⊔ B)
⊢ A.LinearDisjoint B
have this₁ : finrank.{u, v} R ↥A ≤ finrank.{u, v} R ↥(A ⊔ B)
Tactic: have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
    LinearMap.finrank_le_finrank_of_injective <|
      Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)
-- 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 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
⊢ A.LinearDisjoint B
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)
Tactic: rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
-- 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 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((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)
hxy :
  Eq (α := 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)
        x :
      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)
        y :
      S)
⊢ x = y
have obtain : ∀ (M' : Submodule R S) (hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
  (hf : Module.Finite.{u, v} R ↥M')
  (h :
    {x, y} ⊆
      (↑(LinearMap.range
            (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
              (Submodule.inclusion hM))) :
        Set
          (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))),
  x = y
Tactic: obtain ⟨M', hM, hf, h⟩ :=
    TensorProduct.exists_finite_submodule_left_of_setFinite' {x, y} (Set.toFinite _)
-- 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 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((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)
hxy :
  Eq (α := 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)
        x :
      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)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
⊢ x = y
have obtain : ∀ (s : Finset S) (hs : Submodule.span R (↑s : Set S) = M'), x = y
Tactic: obtain ⟨s, hs⟩ : M'.FG := .of_finite
-- 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 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((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)
hxy :
  Eq (α := 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)
        x :
      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)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
⊢ (↑s : Set S) ⊆ (↑A : Set S)
have rwa : ∀
  (hM :
    LE.le (α := Submodule R S) (Submodule.span R (↑s : Set S)) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A))
  (hs : Submodule.span R (↑s : Set S) = M'), (↑s : Set S) ⊆ (↑A : Set S)
Tactic: rwa [← hs, Submodule.span_le] at hM
Cleared hypotheses: hs