awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subsemiring Aᵐᵒᵖ)
    (Subsemiring.closure
      (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪
        MulOpposite.unop ⁻¹' s))
    (Subsemiring.closure
      (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s))
have a : ∀ (x : Aᵐᵒᵖ),
  Membership.mem (γ := Set Aᵐᵒᵖ)
      (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x ↔
    Membership.mem (γ := Set Aᵐᵒᵖ) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ)) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ (y : R), (algebraMap R A : (a : R) → A) y = MulOpposite.unop x) ↔
    ∃ (y : R), MulOpposite.op ((algebraMap R A : (a : R) → A) y) = x
have a : ∀ (x_1 : R),
  (algebraMap R A : (a : R) → A) x_1 = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
Tactic: congr!
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x_1 : R
⊢ (algebraMap R A : (a : R) → A) x_1 = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
have a : MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = MulOpposite.op (MulOpposite.unop x) ↔
  MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
Tactic: rw [← MulOpposite.op_injective.eq_iff (b := x.unop), MulOpposite.op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x_1 : R
a :
  MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = MulOpposite.op (MulOpposite.unop x) ↔
    MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
⊢ (algebraMap R A : (a : R) → A) x_1 = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
have a₁ : MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
Tactic: rw [← MulOpposite.op_injective.eq_iff (b := x.unop), MulOpposite.op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Eq (α := Subalgebra R A) (Subalgebra.unop (Algebra.adjoin R s)) (Algebra.adjoin R (MulOpposite.op ⁻¹' s))
have a : Eq (α := Subsemiring A) (toSubsemiring (Subalgebra.unop (Algebra.adjoin R s)))
  (toSubsemiring (Algebra.adjoin R (MulOpposite.op ⁻¹' s)))
Tactic: apply toSubsemiring_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Eq (α := Subsemiring A) (toSubsemiring (Subalgebra.unop (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.op ⁻¹' s)))
have a : Eq (α := Subsemiring A)
  (Subsemiring.closure
    (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪
      MulOpposite.op ⁻¹' s))
  (Subsemiring.closure (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ MulOpposite.op ⁻¹' s))
Tactic: simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Eq (α := Subsemiring A)
    (Subsemiring.closure
      (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪
        MulOpposite.op ⁻¹' s))
    (Subsemiring.closure (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ MulOpposite.op ⁻¹' s))
have a : ∀ (x : A),
  Membership.mem (γ := Set A)
      (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ)) x ↔
    Membership.mem (γ := Set A) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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'
this :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
⊢ x ∈ S'
have obtain : ∀ (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: obtain ⟨x, rfl⟩ := this
Cleared hypotheses: x, H, this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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'
⊢ x ∈ S'
have suffices : Membership.mem (γ := Submodule (↥S') S)
  ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
Tactic: suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
    obtain ⟨x, rfl⟩ := this
    exact x.2
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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'
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
have 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
Tactic: choose n hn using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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
have a : Eq.{u_2 + 1} (α := S) (↑(∑ i ∈ ι', l' i * s' i) : S) (↑1 : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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) : S) (↑1 : S)
have a : Eq (α := S) ((S'.subtype : (a : ↥S'.toSubsemiring) → S) (∑ i ∈ ι', l' i * s' i) : S) (1 : S)
Tactic: change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (hypothesis)
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) ⋯
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
have e' : 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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 ι))) ⊤
have rw : Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (∑ i ∈ ι', l' i * s' i)
Tactic: rw [Ideal.eq_top_iff_one, ← e']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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
⊢ Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (∑ i ∈ ι', l' i * s' i)
have h : ∀ c ∈ ι', Membership.mem (γ := Ideal ↥S') (Ideal.span (s' '' (↑ι' : Set ι))) (l' c * s' c)
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (hypothesis)
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
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (hypothesis)
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
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
have hN : Eq (α := Ideal ↥S') (Ideal.span ((fun (x : ↥S') ↦ x ^ N) '' s' '' (↑ι' : Set ι))) ⊤
Tactic: have hN := Ideal.span_pow_eq_top _ this N
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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 ι))) ⊤
⊢ Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
have 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)
Tactic: apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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)
    ((↑(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)
have 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)
Tactic: change s' i ^ N • x ∈ _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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 • x)
have 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)
Tactic: rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Operations (goal)
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)
have 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)
Tactic: refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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
⊢ 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)
have 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)
Tactic: rw [Submodule.mul_le]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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
⊢ IsIdempotentElem (M := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
have 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: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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
⊢ IsIdempotentElem (M := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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
have 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: refine (mul_toSubmodule_le _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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
⊢ 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)
have 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)
Tactic: rw [sup_idem]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
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 ∈
    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)
have 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)
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
⊢ 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)
have 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)
Tactic: refine le_antisymm (mul_toSubmodule_le _ _) ?_
-- 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
⊢ 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 : 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)
Tactic: refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx