awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
refine_1 :
  ∀ (x : A) (hx : x ∈ (↑S : Set A) ∪ (↑T : Set A)),
    x ∈
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_2 : ∀ (r : R),
  Membership.mem (α := A)
    (HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A))
    ((algebraMap R A : (a : R) → A) r : A)
Tactic: refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
refine_1 :
  ∀ (x : A) (hx : x ∈ (↑S : Set A) ∪ (↑T : Set A)),
    x ∈
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
refine_2 :
  ∀ (r : R),
    Membership.mem (α := A)
      (HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A))
      ((algebraMap R A : (a : R) → A) r : A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_3 : ∀ (x y : A),
  Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x →
    Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) y →
      ∀
        (hx :
          x ∈
            HMul.hMul (α := Submodule R A) (β := Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A))
        (hy :
          y ∈
            HMul.hMul (α := Submodule R A) (β := Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)),
        x * y ∈
          HMul.hMul (α := Submodule R A) (β := Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x : A
hx : x ∈ (↑S : Set A) ∪ (↑T : Set A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_1 : ∀ (hxS : x ∈ (↑S : Set A)),
  x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rcases hx with hxS | hxT
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x : A
hx : x ∈ (↑S : Set A) ∪ (↑T : Set A)
refine_1 :
  ∀ (hxS : x ∈ (↑S : Set A)),
    x ∈
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_1₁ : ∀ (hxT : x ∈ (↑T : Set A)),
  x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rcases hx with hxS | hxT
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x : A
hxS : x ∈ (↑S : Set A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_1 : x * 1 ∈
  HMul.hMul (α := Submodule R A) (β := Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rw [← mul_one x]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x : A
hxT : x ∈ (↑T : Set A)
⊢ x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_1 : 1 * x ∈
  HMul.hMul (α := Submodule R A) (β := Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rw [← one_mul x]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
r : R
⊢ Membership.mem (α := A)
    (HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A))
    ((algebraMap R A : (a : R) → A) r : A)
have refine_2 : HMul.hMul (α := A) (β := A) (1 : A) ((algebraMap R A : (a : R) → A) r : A) ∈
  HMul.hMul (α := Submodule R A) (β := Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rw [← one_mul (algebraMap _ _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (hypothesis)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x y : A
h : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
h_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) y
hx :
  x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
hy :
  y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
⊢ x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have this : x * y ∈
  HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A) *
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: have := Submodule.mul_mem_mul hx hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x y : A
h : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
h_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) y
hx :
  x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
hy :
  y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
this :
  x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A) *
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
⊢ x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_3 : ∀
  (this :
    x * y ∈
      HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        (HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
          (HMul.hMul (α := Submodule R A) (β := Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)))),
  x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
    isIdempotentElem_toSubmodule, mul_comm T.toSubmodule, ← mul_assoc,
    isIdempotentElem_toSubmodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := Subalgebra R (A × B)) (prod ⊤ ⊤) ⊤
have h : ∀ (x : A × B), Membership.mem (γ := Subalgebra R (A × B)) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Subalgebra R (A × B)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have inl : Subsingleton R → Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
Tactic: rcases subsingleton_or_nontrivial R with _ | _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
inl : Subsingleton R → Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have inr : Nontrivial R → Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
Tactic: rcases subsingleton_or_nontrivial R with _ | _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Subsingleton R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have this : Subsingleton S
Tactic: haveI := Module.subsingleton R S
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have a : Nontrivial S
Tactic: nontriviality S using rank_subsingleton'
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have this₁ : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
Tactic: haveI : IsScalarTower R A (Algebra.adjoin A (B : Set S)) :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
have rw : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A (↑B : Set S))
Tactic: rw [rank_mul_rank R A (Algebra.adjoin A (B : Set S))]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A (↑B : Set S))
have change : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (S := ↥A) (Algebra.adjoin ↥A (↑B : Set S)))
Tactic: change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥A
inst_4 : Free.{u_2, u_2} ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
h : Nontrivial R
h_1 : Nontrivial S
this_1 : Algebra ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) := algebra (Algebra.adjoin ↥A (↑B : Set S))
this_2 : SMul ↥A ↥(Algebra.adjoin ↥A (↑B : Set S)) :=
  @Algebra.toSMul _ _ A.toCommSemiring (toSemiring (Algebra.adjoin ↥A (↑B : Set S))) _
this : IsScalarTower.{u_1, u_2, u_2} R ↥A ↥(Algebra.adjoin ↥A (↑B : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (S := ↥A) (Algebra.adjoin ↥A (↑B : Set S)))
have rw : Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin R ((↑A : Set S) ∪ (↑B : Set S)))
Tactic: rw [Algebra.restrictScalars_adjoin]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
have rw : Module.rank R ↥(B ⊔ A) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
Tactic: rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw : Module.rank R ↥(B ⊔ A) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
have rw₁ : Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) =
  Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
Tactic: rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ finrank.{u_1, u_2} R ↥(A ⊔ B) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
have rw : finrank.{u_1, u_2} R ↥(B ⊔ A) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
Tactic: rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Rank (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Free.{u_1, u_2} R ↥B
inst_4 : Free.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
rw : finrank.{u_1, u_2} R ↥(B ⊔ A) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
⊢ finrank.{u_1, u_2} R ↥(A ⊔ B) = finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
have rw₁ : finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S)) =
  finrank.{u_1, u_2} R ↥B * finrank.{u_2, u_2} ↥B ↥(Algebra.adjoin ↥B (↑A : Set S))
Tactic: rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra R A
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ Membership.mem (α := A) U.carrier ((algebraMap R A : (a : R) → A) x : A)
have rw : Membership.mem (α := A) U.carrier ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) x : S) : A)
Tactic: rw [IsScalarTower.algebraMap_apply R S A]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U V : Subalgebra S A
H : Eq (α := Subalgebra R A) (restrictScalars R U) (restrictScalars R V)
x : A
⊢ x ∈ U ↔ x ∈ V
have rw : Membership.mem (γ := Subalgebra R A) (restrictScalars R U) x ↔ x ∈ V
Tactic: rw [← mem_restrictScalars R, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U V : Subalgebra S A
H : Eq (α := Subalgebra R A) (restrictScalars R U) (restrictScalars R V)
x : A
rw : Membership.mem (γ := Subalgebra R A) (restrictScalars R U) x ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V
have rw₁ : Membership.mem (γ := Subalgebra R A) (restrictScalars R V) x ↔ x ∈ V
Tactic: rw [← mem_restrictScalars R, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
U V : Subalgebra S A
H : Eq (α := Subalgebra R A) (restrictScalars R U) (restrictScalars R V)
x : A
rw : Membership.mem (γ := Subalgebra R A) (restrictScalars R U) x ↔ x ∈ V
rw₁ : Membership.mem (γ := Subalgebra R A) (restrictScalars R V) x ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V
have rw₂ : x ∈ V ↔ x ∈ V
Tactic: rw [← mem_restrictScalars R, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Eq.{w + 1} (α := Submodule R A) (Submodule.restrictScalars R (R := ↥S) 1)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
have h : ∀ (x : A),
  Membership.mem (γ := Submodule R A) (Submodule.restrictScalars R (R := ↥S) 1) x ↔
    Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
Tactic: ext