awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LinearDisjoint
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 : Flat.{u, v} R ↥B
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_right_of_inj (fun _ _ ↦ mul_comm _ _) hinj

Premises used: Set.Mem, mul_comm, Subtype.val, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst_3 : Flat.{u, v} R ↥A
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥A = 1

Tactic:
H.rank_eq_one_of_commute_of_flat_of_self_of_inj (fun _ _ ↦ mul_comm _ _) hinj

Premises used: Set.Mem, Subalgebra.LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj, mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
rw₁ rw₂ : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(A ⊔ B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B

Tactic:
rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]

Premises used: LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, Subalgebra.LinearDisjoint.mulMap, rank_tensorProduct'
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup_of_free))

Premises used: map_mul
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)

Tactic:
rw [← Module.finrank_tensorProduct] at H

Premises used: Module.finrank_tensorProduct
-- Module: Mathlib.RingTheory.LinearDisjoint
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
H₁ : finrank.{u, v} R ↥(A ⊔ B) = finrank.{u, v} R (↥A ⊗[R] ↥B)
⊢ Nontrivial R

Tactic:
rw [← Module.finrank_tensorProduct] at H

Premises used: Module.finrank_tensorProduct
-- Module: Mathlib.RingTheory.LinearDisjoint
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
obtain : ∀ (j : Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)) (hj : LinearIndependent R j), A.LinearDisjoint B
⊢ A.LinearDisjoint B

Tactic:
obtain ⟨j, hj⟩ := exists_linearIndependent_of_le_finrank H.ge

Premises used: exists_linearIndependent_of_le_finrank, Eq.ge
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ 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

Premises used: LinearIndependent
-- Module: Mathlib.RingTheory.LinearDisjoint
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))
⊢ finrank.{u, v} R (↥A ⊗[R] ↥B) = finrank R (Fin (finrank.{u, v} R (↥A ⊗[R] ↥B)) →₀ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
⊢ Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))

Tactic:
simpa [j']
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
⊢ Function.Injective (α := ↥A ⊗[R] ↥B) (β := ↥(A ⊔ B)) (⇑j' : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B))

Tactic:
replace hj : Function.Injective j' := by simpa [j']
-- Module: Mathlib.RingTheory.LinearDisjoint
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))
⊢ 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
-- Module: Mathlib.RingTheory.LinearDisjoint
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))
⊢ Module.Finite.{u, v} R ↥(A ⊔ B)

Tactic:
haveI := Subalgebra.finite_sup A B
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
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)
⊢ A.LinearDisjoint B

Tactic:
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]

Premises used: Submodule.linearDisjoint_iff, Subalgebra.linearDisjoint_iff
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
⊢ 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:
Subtype.val_injective.comp (OrzechProperty.injective_of_surjective_of_injective j' _ hj hf)

Premises used: Quotient.liftOn', Set.Mem, Subtype.val_injective, AddCon.liftOn, OrzechProperty.injective_of_surjective_of_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
⊢ 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:
exact Subtype.val_injective.comp (OrzechProperty.injective_of_surjective_of_injective j' _ hj hf)

Premises used: Subtype.val_injective, OrzechProperty.injective_of_surjective_of_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.LinearDisjoint
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
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)
⊢ Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) = Module.rank 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)]

Premises used: Membership.mem, Subtype, Subalgebra.adjoin_eq_span_basis, Module.Free.rank_eq_card_chooseBasisIndex, Subalgebra.rank_toSubmodule, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.LinearDisjoint
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
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)
⊢ 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:
change Module.rank B (Submodule.span B (Set.range (A.val ∘ Module.Free.chooseBasis R A))) = _

Premises used: Subalgebra.val, Function.comp, Membership.mem, Subtype, Submodule.span, Set.range, Module.rank, DFunLike.coe, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ 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
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
rw₁ rw₂ : Cardinal.mk (Free.ChooseBasisIndex R ↥A) = 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)

Tactic:
rw [rank_span this, Cardinal.mk_range_eq _ this.injective]

Premises used: LinearIndependent.injective, rank_span, Cardinal.mk_range_eq
-- Module: Mathlib.RingTheory.LinearDisjoint
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 ↥B
inst_4 : Flat.{u, v} R ↥A
inst_5 : Nontrivial R
inst_6 : Nontrivial S
⊢ Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) = Module.rank R ↥B

Tactic:
H.symm.adjoin_rank_eq_rank_left

Premises used: Subalgebra.LinearDisjoint.symm, Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left
-- Module: Mathlib.RingTheory.LinearDisjoint
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)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.LinearDisjoint
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
neg : ∀ (h1 : ¬finrank.{u, v} R ↥A = 0), A.LinearDisjoint B
⊢ A.LinearDisjoint B

Tactic:
by_cases h1 : Module.finrank R A = 0

Premises used: Membership.mem, Subtype, Module.finrank
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ finrank.{u, v} R ↥B = 1

Tactic:
rw [h1, Nat.coprime_zero_left] at H

Premises used: Nat.coprime_zero_left
-- Module: Mathlib.RingTheory.LinearDisjoint
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
H₁ : finrank.{u, v} R ↥B = 1
⊢ Nontrivial R

Tactic:
rw [h1, Nat.coprime_zero_left] at H

Premises used: Nat.coprime_zero_left
-- Module: Mathlib.RingTheory.LinearDisjoint
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
H₁ : finrank.{u, v} R ↥B = 1
a : Nontrivial R
⊢ finrank.{u, v} R ↥A = 0

Tactic:
rw [h1, Nat.coprime_zero_left] at H

Premises used: Nat.coprime_zero_left
-- Module: Mathlib.RingTheory.LinearDisjoint
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
pos : A.LinearDisjoint ⊥
⊢ A.LinearDisjoint B

Tactic:
rw [eq_bot_of_finrank_one H]

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.RingTheory.LinearDisjoint
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 ⊥

Tactic:
bot_right _

Premises used: Subalgebra.LinearDisjoint.bot_right
-- Module: Mathlib.RingTheory.LinearDisjoint
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 ⊥

Tactic:
exact bot_right _

Premises used: Subalgebra.LinearDisjoint.bot_right
-- Module: Mathlib.RingTheory.LinearDisjoint
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
neg : ∀ (h2 : ¬finrank.{u, v} R ↥B = 0), A.LinearDisjoint B
⊢ A.LinearDisjoint B

Tactic:
by_cases h2 : Module.finrank R B = 0

Premises used: Membership.mem, Subtype, Module.finrank
-- Module: Mathlib.RingTheory.LinearDisjoint
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
⊢ finrank.{u, v} R ↥A = 1

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Premises used: Nat.coprime_zero_right