awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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 (γ := 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)))
have 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'
Tactic: apply Subalgebra.mul_mem _ (Subalgebra.pow_mem _ hr _) _
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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'
have refine : r ^ n₁ a • (↑a : B) ∈ B'
Tactic: refine Subalgebra.smul_mem _ ?_ _
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ r ^ n₁ a • (↑a : B) ∈ B'.toSubmonoid
have rw : Membership.mem (γ := Submonoid B) (Submonoid.closure (↑B'.toSubmonoid : Set B)) (r ^ n₁ a • (↑a : B))
Tactic: rw [← Submonoid.closure_eq B'.toSubmonoid]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s : NonUnitalSubalgebra R A
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
have rw : span R (↑(Submonoid.closure (↑s : Set A)) : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
have rw₁ : span R ({1} ∪ (↑(Subsemigroup.closure (↑s : Set A)) : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
have rw₂ : R ∙ 1 ⊔ span R (↑(Subsemigroup.closure (↑s : Set A)) : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
have rw₃ : R ∙ 1 ⊔ NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (↑s : Set A)) = R ∙ 1 ⊔ s.toSubmodule
have rw₄ : R ∙ 1 ⊔ s.toSubmodule = R ∙ 1 ⊔ s.toSubmodule
Tactic: rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalAlgebra.adjoin_eq_span,
      NonUnitalAlgebra.adjoin_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
| Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)
have rw : adjoin F ((↑K : Set E) ∪ S)
Tactic: rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
have conv_lhs : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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))
⊢ Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (S := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))
have conv_lhs₁ : Eq (α := Subalgebra F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑K : Set E) ∪ S))
Tactic: conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ K = K'
have rwa : ∀ (h : (↑K.toSubsemiring : Set E) = (↑K'.toSubsemiring : Set E)), (↑K : Set E) = (↑K' : Set E)
Tactic: rwa [SetLike.ext'_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ Eq (α := Subalgebra F E) (Subalgebra.restrictScalars F (adjoin L S)) (Subalgebra.restrictScalars F (adjoin L' S))
have apply_fun : Eq (α := Subsemiring E) (toSubsemiring (Subalgebra.restrictScalars F (adjoin L S)))
  (toSubsemiring (Subalgebra.restrictScalars F (adjoin L' S)))
Tactic: apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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
⊢ 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))
have 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))
Tactic: rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
have obtain : ∀ (ιA : Type v) (bA : Basis ιA R ↥A), Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
Tactic: obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
have obtain : ∀ (ιB : Type v) (bB : Basis ιB 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)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
have h : (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)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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 ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
have 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
Tactic: change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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 ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S) ≤
    Module.rank R ↥A * Module.rank R ↥B
have 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
Tactic: rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
have 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
Tactic: refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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 (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤
    Cardinal.mk ιA * Cardinal.mk ιB
have h₁ : Cardinal.mk (↑(Set.range fun (i : ιA) ↦ (↑((bA : (a : ιA) → ↥A) i) : S)) : Type v) ≤ Cardinal.mk ιA
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ 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
have h₂ : Cardinal.mk (↑(Set.range fun (i : ιB) ↦ (↑((bB : (a : ιB) → ↥B) i) : S)) : Type v) ≤ Cardinal.mk ιB
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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
Tactic: by_cases h : Module.Finite R A ∧ Module.Finite R B