awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
apply :
  HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
      (r ^ n₁ a • (↑a : B)) ∈
    B'
⊢ Membership.mem (γ := Submodule R B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) B' : Submodule R B)
    (HPow.hPow (α := B) ((algebraMap A B : (a : A) → B) r : B) (n - n₁ a) *
      HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
        (r ^ n₁ a • (↑a : B)))

Tactic:
apply Subalgebra.mul_mem _ (Subalgebra.pow_mem _ hr _) _

Premises used: Subalgebra.mul_mem, Subalgebra.pow_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
      (r ^ n₁ a • (↑a : B)) ∈
    B'

Tactic:
Subalgebra.smul_mem _ ?_ _

Premises used: Subalgebra.smul_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
refine : r ^ n₁ a • (↑a : B) ∈ B'
⊢ HSMul.hSMul.{uR, uB, uB} (α := R) ((l : (a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)) → R) a : R)
      (r ^ n₁ a • (↑a : B)) ∈
    B'

Tactic:
refine Subalgebra.smul_mem _ ?_ _

Premises used: Subalgebra.smul_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
rw : Membership.mem (γ := Submonoid B) (Submonoid.closure (↑B'.toSubmonoid : Set B)) (r ^ n₁ a • (↑a : B))
⊢ r ^ n₁ a • (↑a : B) ∈ B'.toSubmonoid

Tactic:
rw [← Submonoid.closure_eq B'.toSubmonoid]

Premises used: Subalgebra.toSubsemiring, Subsemiring.toSubmonoid, Submonoid.closure_eq
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ (↑B' : Set B)
hr : Membership.mem (α := B) B' ((algebraMap A B : (a : A) → B) r : B)
l : Finsupp.{uB, uR} (↑(↑(Submonoid.closure s) : Set B) : Type uB) R
n₁ : (x : ↥(Submonoid.closure s)) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), Membership.mem (γ := Submonoid B) (Submonoid.closure (r • s)) (r ^ n₁ x • (↑x : B))
n : ℕ
hn : n ≥ l.support.sup n₁
a : (↑(↑(Submonoid.closure s) : Set B) : Type uB)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ Membership.mem (γ := Submonoid B) (Submonoid.closure (↑B'.toSubmonoid : Set B)) (r ^ n₁ a • (↑a : B))

Tactic:
apply Submonoid.closure_mono hs (n₂ a)

Premises used: Submonoid.closure_mono
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
r : R
s : Set A
x : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
⊢ ∃ (n₀ : ℕ), ∀ n ≥ n₀, Membership.mem (γ := Subalgebra R A) (adjoin R (r • s)) (r ^ n • x)

Tactic:
pow_smul_mem_of_smul_subset_of_mem_adjoin r s _ subset_adjoin hx (Subalgebra.algebraMap_mem _ _)

Premises used: Algebra.subset_adjoin, Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin, Subalgebra.algebraMap_mem
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s : NonUnitalSubalgebra R A
rw : span R (↑(Submonoid.closure (↑s : Set A)) : Set A) = R ∙ 1 ⊔ s.toSubmodule
rw₁ : span R ({1} ∪ (↑(Subsemigroup.closure (↑s : Set A)) : Set A)) = R ∙ 1 ⊔ s.toSubmodule
rw₂ : R ∙ 1 ⊔ span R (↑(Subsemigroup.closure (↑s : Set A)) : Set A) = R ∙ 1 ⊔ s.toSubmodule
rw₃ : R ∙ 1 ⊔ NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
rw₄ rw₅ : R ∙ 1 ⊔ s.toSubmodule = R ∙ 1 ⊔ s.toSubmodule
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalAlgebra.adjoin_eq_span,
      NonUnitalAlgebra.adjoin_eq]

Premises used: Submonoid.closure_eq_one_union, Algebra.adjoin_eq_span, Submodule.span_union, NonUnitalAlgebra.adjoin_eq, NonUnitalAlgebra.adjoin_eq_span
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : CommSemiring E
inst_1 : Semiring K
inst_2 : SMul F E
inst_3 : Algebra E K
inst_4 : CommSemiring F
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
L : Subalgebra F K
ι : Type u_4
bL : Basis.{u_4, u_1, u_3} ι F ↥L
⊢ Eq (α := Submodule F K) ((toSubmodule : (a : Subalgebra F K) → Submodule F K) L : Submodule F K)
    (span F (Set.range fun (i : ι) ↦ (↑((bL : (a : ι) → ↥L) i) : K)) : Submodule F K)

Tactic:
simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
      using congr_arg (Submodule.map (L.val : L →ₗ[F] K)) bL.span_eq.symm

Premises used: Set.range_comp, Submodule.map_top, Subalgebra.val, Subalgebra.range_val, congr_arg, SemilinearMapClass.semilinearMap, Submodule.map_span, Submodule.map, Module.Basis.span_eq, Eq.symm
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_4
inst : CommSemiring F
E : Type u_5
inst_1 : CommSemiring E
inst_2 : Algebra F E
K : Subalgebra F E
S : Set E
rw : adjoin F ((↑K : Set E) ∪ S)
| Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)

Tactic:
rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

Premises used: Algebra.adjoin_eq, Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_4
inst : CommSemiring F
E : Type u_5
inst_1 : CommSemiring E
inst_2 : Algebra F E
K : Subalgebra F E
S : Set E
conv_lhs :
  Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
conv_lhs₁ : Eq (α := Subalgebra F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑K : Set E) ∪ S))
⊢ Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))

Tactic:
conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

Premises used: Algebra.adjoin_eq, Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst : CommSemiring F
inst_1 : CommSemiring L
inst_2 : CommSemiring L'
inst_3 : Semiring E
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : Algebra F L'
inst_7 : Algebra L' E
inst_8 : Algebra F E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_6 + 1, u_7 + 1, u_5 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : Subalgebra F E
h : K.toSubsemiring = K'.toSubsemiring
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : (↑K.toSubsemiring : Set E) = (↑K'.toSubsemiring : Set E)), (↑K : Set E) = (↑K' : Set E)
⊢ K = K'

Tactic:
rwa [SetLike.ext'_iff] at h ⊢

Premises used: SetLike.ext'_iff
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst : CommSemiring F
inst_1 : CommSemiring L
inst_2 : CommSemiring L'
inst_3 : Semiring E
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : Algebra F L'
inst_7 : Algebra L' E
inst_8 : Algebra F E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_6 + 1, u_7 + 1, u_5 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
apply_fun :
  Eq (α := Subsemiring E) (toSubsemiring (Subalgebra.restrictScalars F (adjoin L S)))
    (toSubsemiring (Subalgebra.restrictScalars F (adjoin L' S)))
⊢ Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (adjoin L S)) (Subalgebra.restrictScalars F (adjoin L' S))

Tactic:
apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢

Premises used: Subalgebra.toSubsemiring
-- Module: Mathlib.RingTheory.Adjoin.Basic
Goal:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst : CommSemiring F
inst_1 : CommSemiring L
inst_2 : CommSemiring L'
inst_3 : Semiring E
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : Algebra F L'
inst_7 : Algebra L' E
inst_8 : Algebra F E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_6 + 1, u_7 + 1, u_5 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
rw :
  Eq (α := Subsemiring E)
    (closure
      (Set.range.{u_5, u_6 + 1} (ι := L)
          (Function.comp.{u_6 + 1, u_7 + 1, u_5 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E)
            (⇑i : (a : L) → L')) ∪
        S))
    (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))
rw₁ :
  Eq (α := Subsemiring E)
    (closure
      (Set.image.{u_7, u_5} (α := L') (⇑(algebraMap L' E) : (a : L') → E)
          (Set.range.{u_7, u_6 + 1} (ι := L) (⇑i : (a : L) → L')) ∪
        S))
    (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))
rw₂ :
  Eq (α := Subsemiring E) (closure (Set.image.{u_7, u_5} (α := L') (⇑(algebraMap L' E) : (a : L') → E) Set.univ ∪ S))
    (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))
rw₃ rw₄ :
  Eq (α := Subsemiring E) (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))
    (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))
⊢ Eq (α := Subsemiring E) (closure (Set.range.{u_5, u_6 + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E) ∪ S))
    (closure (Set.range.{u_5, u_7 + 1} (ι := L') (⇑(algebraMap L' E) : (a : L') → E) ∪ S))

Tactic:
rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]

Premises used: Set.range_comp, Set.image_univ, EquivLike.range_eq_univ
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
obtain : ∀ (ιA : Type v) (bA : Basis ιA R ↥A), Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)

Premises used: Membership.mem, Subtype, Module.Free.exists_basis
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
obtain : ∀ (ιB : Type v) (bB : Basis ιB R ↥B), Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
obtain ⟨ιB, bB⟩ := Free.exists_basis (R := R) (M := B)

Premises used: Membership.mem, Subtype, Module.Free.exists_basis
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
⊢ (toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R ((↑A : Set S) ∪ (↑B : Set S))) =
    HMul.hMul (α := Submodule R S) (β := Submodule R S)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑A : Set S)) : Submodule R S)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑B : Set S)) : Submodule R S)

Tactic:
have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
change :
  Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S) ≤
    Module.rank R ↥A * Module.rank R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _

Premises used: Membership.mem, Subtype, Max.max, Subalgebra.toSubmodule, Module.rank, DFunLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
rw :
  Module.rank R
      ↥(Submodule.span R
          (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
            (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)))) ≤
    Cardinal.mk ιA * Cardinal.mk ιB
⊢ Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S) ≤
    Module.rank R ↥A * Module.rank R ↥B

Tactic:
rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']

Premises used: Module.Basis.mk_eq_rank''
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
⊢ Module.rank R
      ↥(Submodule.span R
          (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
            (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)))) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Tactic:
(rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_

Premises used: rank_span_le, Cardinal.mk_mul_le, LE.le.trans
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
refine :
  Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) *
      Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤
    Cardinal.mk ιA * Cardinal.mk ιB
⊢ Module.rank R
      ↥(Submodule.span R
          (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
            (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)))) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Tactic:
refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_

Premises used: rank_span_le, Cardinal.mk_mul_le, LE.le.trans
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
h₁ : Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) ≤ Cardinal.mk ιA
h₂ : Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤ Cardinal.mk ιB
⊢ Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) *
      Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤
    Cardinal.mk ιA * Cardinal.mk ιB

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
⊢ Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) ≤ Cardinal.mk ιA

Tactic:
Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
⊢ Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) ≤ Cardinal.mk ιA

Tactic:
exact Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
⊢ Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤ Cardinal.mk ιB

Tactic:
Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h :
  Eq (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
    (Submodule.span R
        (HMul.hMul (α := Set S) (Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S))
          (Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S))) :
      Submodule R S)
⊢ Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤ Cardinal.mk ιB

Tactic:
exact Cardinal.mk_range_le

Premises used: Cardinal.mk_range_le
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
pos :
  ∀ (h : Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
neg :
  ∀ (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
by_cases h : Module.Finite R A ∧ Module.Finite R B

Premises used: Membership.mem, Subtype, Module.Finite
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B
⊢ Module.Finite.{u, v} R ↥A

Tactic:
obtain ⟨_, _⟩ := h
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B
left : Module.Finite.{u, v} R ↥A
⊢ Module.Finite.{u, v} R ↥B

Tactic:
obtain ⟨_, _⟩ := h