awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
y : A
hy : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) y
z : A
hz : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A) z
⊢ y * z ∈ S ⊔ T

Tactic:
exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)

Premises used: Algebra.mem_sup_left, Algebra.mem_sup_right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
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) S : Submodule R A) ≤
    (toSubmodule : (a : Subalgebra R A) → Submodule R A) S
a₁ :
  (toSubmodule : (a : Subalgebra R A) → Submodule R A) S ≤
    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) S : Submodule R A)
⊢ IsIdempotentElem (M := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra 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) S : Submodule R A) ≤
    (toSubmodule : (a : Subalgebra R A) → Submodule R A) S

Tactic:
(mul_toSubmodule_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, Subalgebra.mul_toSubmodule_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
a :
  Eq (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ S) : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : 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) S : Submodule R A) ≤
    (toSubmodule : (a : Subalgebra R A) → Submodule R A) S

Tactic:
refine (mul_toSubmodule_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, Subalgebra.mul_toSubmodule_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
a a₁ :
  Eq (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
⊢ Eq (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ S) : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)

Tactic:
rw [sup_idem]

Premises used: sup_idem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
hx1 : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
a :
  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) S : 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) S : Submodule R A)

Tactic:
rw [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
hx1 : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ 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) S : Submodule R A)

Tactic:
Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

Premises used: Submodule.mul_mem_mul, Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : A
hx1 : Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
⊢ 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) S : Submodule R A)

Tactic:
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

Premises used: Submodule.mul_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
⊢ 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) =
    (toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ T)

Tactic:
le_antisymm (mul_toSubmodule_le _ _) ?_

Premises used: Subalgebra.mul_toSubmodule_le, le_antisymm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
refine :
  (toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ T) ≤
    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) =
    (toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ T)

Tactic:
refine le_antisymm (mul_toSubmodule_le _ _) ?_

Premises used: Subalgebra.mul_toSubmodule_le, le_antisymm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
⊢ 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:
Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx

Premises used: Algebra.adjoin_induction
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
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)
⊢ 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:
refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
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)
⊢ 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
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
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)
⊢ 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 [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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 * 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:
Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)

Premises used: Submodule.mul_mem_mul, Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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 * 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:
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)

Premises used: Submodule.mul_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
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)
⊢ 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]

Premises used: one_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
⊢ 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:
Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT

Premises used: Submodule.mul_mem_mul, Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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)
⊢ 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:
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT

Premises used: Submodule.mul_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
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)
⊢ 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:
rw [← one_mul (algebraMap _ _ _)]

Premises used: Algebra.algebraMap, DFunLike.coe, one_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
⊢ 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:
Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)

Premises used: Submodule.mul_mem_mul, Set.Mem, algebraMap_mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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
⊢ 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:
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)

Premises used: Submodule.mul_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
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) *
      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
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
R' : Type u_3
inst_3 : Semiring R'
inst_4 : MulSemiringAction R' A
inst_5 : SMulCommClass R' R A
m : R'
S : Subalgebra R A
⊢ (↑(m • S) : Set A) = m • (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
R' : Type u_3
inst_3 : Semiring R'
inst_4 : MulSemiringAction R' A
inst_5 : SMulCommClass R' R A
m : R'
S : Subalgebra R A
⊢ (m • S).toSubsemiring = m • S.toSubsemiring

Tactic:
rfl

Premises used: MulSemiringAction.toRingHom, RingHomClass.toRingHom, MulDistribMulAction.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
R' : Type u_3
inst_3 : Semiring R'
inst_4 : MulSemiringAction R' A
inst_5 : SMulCommClass R' R A
m : R'
S : Subalgebra R A
⊢ (toSubmodule : (a : Subalgebra R A) → Submodule R A) (m • S) =
    HSMul.hSMul (β := Submodule R A) m ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, Submodule.map, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R' : Type u_4
R : Type u_5
A : Type u_6
inst : Semiring R'
inst_1 : CommRing R
inst_2 : Ring A
inst_3 : MulSemiringAction R' A
inst_4 : Algebra R A
inst_5 : SMulCommClass R' R A
m : R'
S : Subalgebra R A
⊢ (m • S).toSubring = m • S.toSubring

Tactic:
rfl

Premises used: Subring.map, Subsemiring.map, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
R' : Type u_3
inst_3 : Semiring R'
inst_4 : MulSemiringAction R' A
inst_5 : SMulCommClass R' R A
m : R'
r : A
S : Subalgebra R A
⊢ r ∈ S → m • r ∈ m • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set A))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
R' : Type u_3
inst_3 : Semiring R'
inst_4 : MulSemiringAction R' A
inst_5 : SMulCommClass R' R A
⊢ CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => map_mono⟩

Premises used: CovariantClass.mk, Subalgebra.map_mono
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
S : Subalgebra R A
S₁ : Subalgebra R B
⊢ (↑(S.prod S₁) : Set (A × B)) = (↑S : Set A) ×ˢ (↑S₁ : Set B)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
S : Subalgebra R A
S₁ : Subalgebra R B
⊢ Eq (α := Submodule R (A × B))
    ((toSubmodule : (a : Subalgebra R (A × B)) → Submodule R (A × B)) (S.prod S₁) : Submodule R (A × B))
    (Submodule.prod ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
        ((toSubmodule : (a : Subalgebra R B) → Submodule R B) S₁) :
      Submodule R (A × B))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Submodule.prod, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
S : Subalgebra R A
S₁ : Subalgebra R B
x : A × B
⊢ x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

Tactic:
Set.mem_prod

Premises used: Set.Mem, setOf, Set.prod, Set.mem_prod
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
h :
  ∀ (x : A × B),
    Membership.mem (γ := Subalgebra R (A × B)) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Subalgebra R (A × B)) ⊤ x
⊢ Eq (α := Subalgebra R (A × B)) (prod ⊤ ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
x : A × B
⊢ Membership.mem (γ := Subalgebra R (A × B)) (prod ⊤ ⊤) x ↔ Membership.mem (γ := Subalgebra R (A × B)) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
S T : Subalgebra R A
S₁ T₁ : Subalgebra R B
⊢ S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

Tactic:
Set.prod_mono

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Prod
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
S T : Subalgebra R A
S₁ T₁ : Subalgebra R B
⊢ S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

Tactic:
SetLike.coe_injective Set.prod_inter_prod

Premises used: SetLike.coe_injective, Set.prod_inter_prod