awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : ↥S'
H : ∀ (i : ι), ∃ (n : ℕ), HSMul.hSMul (β := S) (s i ^ n) ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S) ∈ S'
⊢ Membership.mem (α := S) S' ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S)

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : ↥S'
H : ∀ (i : ι), ∃ (n : ℕ), HSMul.hSMul (β := S) (s i ^ n) ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S) ∈ S'
⊢ Membership.mem (α := S) S' ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
H : ∀ (i : ι), ∃ (n : ℕ), s i ^ n • x ∈ S'
suffices :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
⊢ x ∈ S'

Tactic:
suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
    obtain ⟨x, rfl⟩ := this
    exact x.2
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
H : ∀ (i : ι), ∃ (n : ℕ), s i ^ n • x ∈ S'
choose :
  ∀ (n : (i : ι) → ℕ) (hn : ∀ (i : ι), s i ^ n i • x ∈ S'),
    Membership.mem (γ := Submodule (↥S') S)
      ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x

Tactic:
choose n hn using H
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
a : Eq.{u_2 + 1} (α := S) (↑(∑ i ∈ ι', l' i * s' i) : S) (↑1 : S)
⊢ Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
a : Eq (α := S) ((S'.subtype : (a : ↥S'.toSubsemiring) → S) (∑ i ∈ ι', l' i * s' i) : S) (1 : S)
⊢ Eq.{u_2 + 1} (α := S) (↑(∑ i ∈ ι', l' i * s' i) : S) (↑1 : S)

Tactic:
change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1

Premises used: HMul.hMul, Subsemiring.subtype, Subalgebra.toSubsemiring, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
⊢ Eq (α := S) ((S'.subtype : (a : ↥S'.toSubsemiring) → S) (∑ i ∈ ι', l' i * s' i) : S) (1 : S)

Tactic:
simpa only [map_sum, map_mul] using e

Premises used: map_sum, map_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
⊢ Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1

Tactic:
have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
    ext
    change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
    simpa only [map_sum, map_mul] using e
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
rw : Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (∑ i ∈ ι', l' i * s' i)
⊢ Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤

Tactic:
rw [Ideal.eq_top_iff_one, ← e']

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
h : ∀ c ∈ ι', Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (l' c * s' c)
⊢ Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (∑ i ∈ ι', l' i * s' i)

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
i : ι
hi : i ∈ ι'
⊢ Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (l' i * s' i)

Tactic:
Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi

Premises used: Ideal.subset_span, Set.mem_image_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
i : ι
hi : i ∈ ι'
⊢ Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (l' i * s' i)

Tactic:
exact Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi

Premises used: Ideal.subset_span, Set.mem_image_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
⊢ Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤

Tactic:
have : Ideal.span (s' '' ι') = ⊤ := by
    rw [Ideal.eq_top_iff_one, ← e']
    apply sum_mem
    intro i hi
    exact Ideal.mul_mem_left _ _ <| Ideal.subset_span <| Set.mem_image_of_mem s' hi
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
⊢ Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤

Tactic:
have hN := Ideal.span_pow_eq_top _ this N
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
H :
  ∀ (r : (↑((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι)) : Type u_2)),
    Membership.mem (γ := Submodule (↥S') S)
      ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
      ((↑r : ↥S') • x)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x

Tactic:
apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN

Premises used: Membership.mem, Subtype, Submodule.mem_of_span_top_of_smul_mem, Algebra.ofId, Subalgebra.toSubmodule, DFunLike.coe, AlgHom.range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
H :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ N • x)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    ((↑(Subtype.mk (p := fun (x : ↥S') ↦
            Membership.mem (γ := Set ↥S') ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι)) x)
            ((fun (x : ↥S') ↦ x ^ N) (s' i)) ⋯) :
        ↥S') •
      x)

Tactic:
change s' i ^ N • x ∈ _
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
H :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ (N - n i) • s' i ^ n i • x)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ N • x)

Tactic:
rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]

Premises used: pow_add, tsub_add_cancel_of_le, SemigroupAction.mul_smul, Finset.le_sup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ (N - n i) • s' i ^ n i • x)

Tactic:
Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_

Premises used: Set.Mem, Subtype.mk, pow_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
H :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ n i • x)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ (N - n i) • s' i ^ n i • x)

Tactic:
refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_

Premises used: Subtype.mk, pow_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ n i • x)

Tactic:
⟨⟨_, hn i⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : (i : ι) → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (s x) ⋯
l' : ι → ↥S' := fun (x : ι) ↦ Subtype.mk (p := fun (x : S) ↦ x ∈ S') (l x) ⋯
e' : Eq.{u_2 + 1} (α := ↥S') (∑ i ∈ ι', l' i * s' i) 1
this : Eq (α := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) ⊤
N : ℕ := ι'.sup n
hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
i : ι
hi : i ∈ (↑ι' : Set ι)
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S)
    (s' i ^ n i • x)

Tactic:
exact ⟨⟨_, hn i⟩, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
s : Set S
l : (↑s : Type u_2) →₀ S
hs :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ s)) : (a : { x : S // x ∈ s } →₀ S) → S) l : S)
    (1 : S)
hs' : s ⊆ (↑S' : Set S)
hl : ∀ (i : (↑s : Type u_2)), Membership.mem (α := S) S' ((l : (a : (↑s : Type u_2)) → S) i : S)
x : S
H : ∀ (r : (↑s : Type u_2)), ∃ (n : ℕ), (↑r : S) ^ n • x ∈ S'
⊢ x ∈ S'

Tactic:
mem_of_finsetSum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H

Premises used: Finsupp.support, Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Order
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : PartialOrder A
inst_3 : IsOrderedRing A
inst_4 : Algebra R A
S : Subalgebra R A
⊢ IsOrderedRing.{u_2} ↥S

Tactic:
S.toSubsemiring.toIsOrderedRing

Premises used: Subsemiring.toIsOrderedRing, Set.Mem, Subalgebra.toSubsemiring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Order
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : PartialOrder A
inst_3 : IsStrictOrderedRing A
inst_4 : Algebra R A
S : Subalgebra R A
⊢ IsStrictOrderedRing.{u_2} ↥S

Tactic:
S.toSubsemiring.toIsStrictOrderedRing

Premises used: Set.Mem, Subsemiring.toIsStrictOrderedRing, Subalgebra.toSubsemiring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pi
Goal:
ι : Type u_1
R : Type u_2
S : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (S i)
s : Set ι
t : (i : ι) → Subalgebra R (S i)
x : (i : ι) → S i
⊢ x ∈ pi (S := S) s t ↔ ∀ i ∈ s, x i ∈ t i

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pi
Goal:
ι : Type u_1
R : Type u_2
S : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (S i)
s : Set ι
t : (i : ι) → Subalgebra R (S i)
⊢ Eq (α := Submodule R ((i : ι) → S i))
    ((toSubmodule : (a : Subalgebra R ((i : ι) → S i)) → Submodule R ((i : ι) → S i)) (pi (S := S) s t) :
      Submodule R ((i : ι) → S i))
    (Submodule.pi (φ := S) s fun (i : ι) ↦ (toSubmodule : (a : Subalgebra R (S i)) → Submodule R (S i)) (t i) :
      Submodule R ((i : ι) → S i))

Tactic:
rfl

Premises used: Submodule.pi, setOf, Set.pi, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pi
Goal:
ι : Type u_1
R : Type u_2
S : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (S i)
s : Set ι
⊢ Eq (α := Subalgebra R ((i : ι) → S i)) (pi (S := S) s fun (i : ι) ↦ ⊤) ⊤

Tactic:
SetLike.coe_injective <| Set.pi_univ _

Premises used: SetLike.coe_injective, Set.pi_univ
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Pi
Goal:
ι : Type u_1
R : Type u_2
S : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (S i)
s : Set ι
t₁ t₂ : (i : ι) → Subalgebra R (S i)
h : ∀ i ∈ s, t₁ i ≤ t₂ i
⊢ pi (S := S) s t₁ ≤ pi (S := S) s t₂

Tactic:
Set.pi_mono h

Premises used: Set.Mem, setOf, Set.Subset, Set.pi, Set.pi_mono
-- 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
rw :
  ∀ (m : A),
    Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) m →
      ∀ (n : A),
        Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A) n →
          Membership.mem (γ := Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊔ T) : Submodule R A) (m * n)
⊢ 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:
rw [Submodule.mul_le]

Premises used: Submodule.mul_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 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:
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