[GOAL]
⊢ StableUnderComposition @FiniteType
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : FiniteType f
hg : FiniteType g
⊢ FiniteType (comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ HoldsForLocalizationAway @FiniteType
[PROOFSTEP]
introv R _
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ FiniteType (algebraMap R S)
[PROOFSTEP]
suffices Algebra.FiniteType R S by
  rw [RingHom.FiniteType]
  convert this; ext; rw [Algebra.smul_def]; rfl
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ FiniteType (algebraMap R S)
[PROOFSTEP]
rw [RingHom.FiniteType]
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ Algebra.FiniteType R S
[PROOFSTEP]
convert this
[GOAL]
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ toAlgebra (algebraMap R S) = inst✝¹
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := toAlgebra (algebraMap R S);
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := toAlgebra (algebraMap R S);
    r✝ • x✝) =
    ↑(algebraMap R S) r✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FiniteType R S
[PROOFSTEP]
exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S
[GOAL]
⊢ OfLocalizationSpanTarget @FiniteType
[PROOFSTEP]
rw [ofLocalizationSpanTarget_iff_finite]
[GOAL]
⊢ OfLocalizationFiniteSpanTarget @FiniteType
[PROOFSTEP]
introv R hs H
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
⊢ FiniteType f
[PROOFSTEP]
classical
letI := f.toAlgebra
replace H : ∀ r : s, Algebra.FiniteType R (Localization.Away (r : S))
· intro r; simp_rw [RingHom.FiniteType] at H ; convert H r; ext; simp_rw [Algebra.smul_def]; rfl
replace H := fun r => (H r).1
constructor
  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
    -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
    -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
choose t ht using H
obtain ⟨l, hl⟩ :=
  (Finsupp.mem_span_iff_total S (s : Set S) 1).mp (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
use s.attach.biUnion sf ∪ s ∪ l.support.image l
rw [eq_top_iff]
  -- We need to show that every `x` falls in the subalgebra generated by those elements.
    -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
    -- the algebra for each `sᵢ` and some `nᵢ`.
rintro x -
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
· intro x hx
  apply Algebra.subset_adjoin
  rw [Finset.coe_union, Finset.coe_union]
  exact Or.inl (Or.inr hx)
· intro i
  by_cases h : l i = 0; · rw [h]; exact zero_mem _
  apply Algebra.subset_adjoin
  rw [Finset.coe_union, Finset.coe_image]
  exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
· intro r
  rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
    -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
        -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
        -- Porting note: The following `obtain` fails because Lean wants to know right away what the
        -- placeholders are, so we need to provide a little more guidance
        -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
        --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
  rw [show
      ∀ A : Set S,
        (∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔
          (∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A)
      by {exact fun _ => by simp [Submonoid.mem_powers_iff]
    }]
  refine IsLocalization.exists_smul_mem_of_mem_adjoin (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
  · intro x hx
    apply Algebra.subset_adjoin
    exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
  · rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
    apply Algebra.subset_adjoin
    exact Or.inl (Or.inr r.2)
  · rw [ht]; trivial
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
⊢ FiniteType f
[PROOFSTEP]
letI := f.toAlgebra
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
⊢ FiniteType f
[PROOFSTEP]
replace H : ∀ r : s, Algebra.FiniteType R (Localization.Away (r : S))
[GOAL]
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
⊢ ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
intro r
[GOAL]
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
simp_rw [RingHom.FiniteType] at H
[GOAL]
case H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
convert H r
[GOAL]
case h.e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
⊢ Localization.algebra = toAlgebra (comp (algebraMap S (Localization.Away ↑r)) f)
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
r✝ : R
x✝ : Localization (Submonoid.powers ↑r)
⊢ (let_fun I := Localization.algebra;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
r✝ : R
x✝ : Localization (Submonoid.powers ↑r)
⊢ ↑(algebraMap R (Localization (Submonoid.powers ↑r))) r✝ * x✝ = r✝ • x✝
[PROOFSTEP]
rfl
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
⊢ FiniteType f
[PROOFSTEP]
replace H := fun r => (H r).1
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Subalgebra.FG ⊤
⊢ FiniteType f
[PROOFSTEP]
constructor
  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
    -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
    -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
[GOAL]
case out
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Subalgebra.FG ⊤
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
choose t ht using H
[GOAL]
case out
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
obtain ⟨l, hl⟩ :=
  (Finsupp.mem_span_iff_total S (s : Set S) 1).mp (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ 1 ∈ Ideal.span ↑s
[PROOFSTEP]
rw [hs]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case out.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
[GOAL]
case out.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
use s.attach.biUnion sf ∪ s ∪ l.support.image l
[GOAL]
case h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
  -- We need to show that every `x` falls in the subalgebra generated by those elements.
    -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
    -- the algebra for each `sᵢ` and some `nᵢ`.
[GOAL]
case h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ ⊤ ≤ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rintro x -
[GOAL]
case h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ x ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support))
[PROOFSTEP]
intro x hx
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_union]
[GOAL]
case a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(Finset.biUnion (Finset.attach s) sf) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inr hx)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ ∀ (i : ↑↑s), ↑l i ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
intro i
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
⊢ ↑l i ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
by_cases h : l i = 0
[GOAL]
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ↑l i = 0
⊢ ↑l i ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [h]
[GOAL]
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ↑l i = 0
⊢ 0 ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
exact zero_mem _
[GOAL]
case neg
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬↑l i = 0
⊢ ↑l i ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case neg.a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬↑l i = 0
⊢ ↑l i ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_image]
[GOAL]
case neg.a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬↑l i = 0
⊢ ↑l i ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s) ∪ ↑l '' ↑l.support
[PROOFSTEP]
exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ ∀ (r : ↑↑s),
    ∃ n, ↑r ^ n • x ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
intro r
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
  -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
      -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
      -- Porting note: The following `obtain` fails because Lean wants to know right away what the
      -- placeholders are, so we need to provide a little more guidance
      -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
      --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ n,
    ↑r ^ n • x ∈
      Algebra.adjoin R
        ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support))
[PROOFSTEP]
rw [show
    ∀ A : Set S,
      (∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔ (∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A)
    by {exact fun _ => by simp [Submonoid.mem_powers_iff]
  }]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∀ (A : Set S), (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R A) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R A
[PROOFSTEP]
{exact fun _ => by simp [Submonoid.mem_powers_iff]
}
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∀ (A : Set S), (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R A) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R A
[PROOFSTEP]
exact fun _ => by simp [Submonoid.mem_powers_iff]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
x✝ : Set S
⊢ (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R x✝) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R x✝
[PROOFSTEP]
simp [Submonoid.mem_powers_iff]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ m,
    ↑m • x ∈
      Algebra.adjoin R
        ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support))
[PROOFSTEP]
refine IsLocalization.exists_smul_mem_of_mem_adjoin (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
[GOAL]
case refine_1
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r)) ⊆
    ↑(Algebra.adjoin R
        ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)))
[PROOFSTEP]
intro x hx
[GOAL]
case refine_1
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ : S
r : ↑↑s
x : S
hx : x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r))
⊢ x ∈
    ↑(Algebra.adjoin R
        ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case refine_1.a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x✝ : S
r : ↑↑s
x : S
hx : x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r))
⊢ x ∈ (⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
[GOAL]
case refine_2
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ Submonoid.powers ↑r ≤
    (Algebra.adjoin R
          ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪
            ↑(Finset.image (↑l) l.support))).toSubsemiring.toSubmonoid
[PROOFSTEP]
rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
[GOAL]
case refine_2
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑r ∈
    ↑(Algebra.adjoin R
            ((⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪
              ↑(Finset.image (↑l) l.support))).toSubsemiring.toSubmonoid
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case refine_2.a
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑r ∈ (⋃ (x : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inr r.2)
[GOAL]
case refine_3
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑(algebraMap S (Localization.Away ↑r)) x ∈ Algebra.adjoin R ↑(t r)
[PROOFSTEP]
rw [ht]
[GOAL]
case refine_3
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑(algebraMap S (Localization.Away ↑r)) x ∈ ⊤
[PROOFSTEP]
trivial


[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ esymm (map f s.val) n = ∑ t in Finset.powersetLen n s, Finset.prod t f
[PROOFSTEP]
simp only [esymm, powersetLen_map, ← Finset.map_val_val_powersetLen, map_map]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ sum (map ((fun x => prod x) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetLen n s).val) =
    ∑ t in Finset.powersetLen n s, Finset.prod t f
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha : a✝ ∈ setOf IsSymmetric
hb : b✝ ∈ setOf IsSymmetric
e : Perm σ
⊢ ↑(rename ↑e) (a✝ * b✝) = a✝ * b✝
[PROOFSTEP]
rw [AlgHom.map_mul, ha, hb]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha :
  a✝ ∈
    {
          toSubsemigroup :=
            { carrier := setOf IsSymmetric,
              mul_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ setOf IsSymmetric → b ∈ setOf IsSymmetric → ∀ (e : Perm σ), ↑(rename ↑e) (a * b) = a * b) },
          one_mem' := (_ : 1 ∈ setOf IsSymmetric) }.toSubsemigroup.carrier
hb :
  b✝ ∈
    {
          toSubsemigroup :=
            { carrier := setOf IsSymmetric,
              mul_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ setOf IsSymmetric → b ∈ setOf IsSymmetric → ∀ (e : Perm σ), ↑(rename ↑e) (a * b) = a * b) },
          one_mem' := (_ : 1 ∈ setOf IsSymmetric) }.toSubsemigroup.carrier
e : Perm σ
⊢ ↑(rename ↑e) (a✝ + b✝) = a✝ + b✝
[PROOFSTEP]
rw [AlgHom.map_add, ha, hb]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ ψ : MvPolynomial σ R
hφ : IsSymmetric φ
f : R →+* S
e : Perm σ
⊢ ↑(rename ↑e) (↑(MvPolynomial.map f) φ) = ↑(MvPolynomial.map f) φ
[PROOFSTEP]
rw [← map_rename, hφ]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R = Multiset.esymm (Multiset.map X univ.val)
[PROOFSTEP]
refine' funext fun n => (Finset.esymm_map_val X _ n).symm
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Algebra R S
f : σ → S
n : ℕ
⊢ ↑(aeval f) (esymm σ R n) = Multiset.esymm (Multiset.map f univ.val) n
[PROOFSTEP]
simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, Finset.esymm_map_val]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ t in powersetLen n univ, ↑(monomial (∑ i in t, Finsupp.single i 1)) 1
[PROOFSTEP]
simp_rw [monomial_sum_one]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ x in powersetLen n univ, ∏ x in x, ↑(monomial (Finsupp.single x 1)) 1
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R 0 = 1
[PROOFSTEP]
simp only [esymm, powersetLen_zero, sum_singleton, prod_empty]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
f : R →+* S
⊢ ↑(map f) (esymm σ R n) = esymm σ S n
[PROOFSTEP]
simp_rw [esymm, map_sum, map_prod, map_X]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ↑(rename ↑e) (esymm σ R n) = ∑ x in powersetLen n univ, ∏ i in x, X (↑e i)
[PROOFSTEP]
simp_rw [esymm, map_sum, map_prod, rename_X]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ i in x, X (↑e i) =
    ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i
[PROOFSTEP]
simp [Finset.powersetLen_map, -Finset.map_univ_equiv]
  --Porting note: Why did `mapEmbedding_apply` not work?
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in ↑(mapEmbedding (Equiv.toEmbedding e)) x, X i
[PROOFSTEP]
dsimp [mapEmbedding, OrderEmbedding.ofMapLEIff]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in Finset.map (Equiv.toEmbedding e) x, X i
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i = ∑ t in powersetLen n univ, ∏ i in t, X i
[PROOFSTEP]
rw [Finset.map_univ_equiv]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ IsSymmetric (esymm σ R n)
[PROOFSTEP]
intro
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e✝ : Perm σ
⊢ ↑(rename ↑e✝) (esymm σ R n) = esymm σ R n
[PROOFSTEP]
rw [rename_esymm]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [esymm_eq_sum_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (∑ t in powersetLen n univ, ↑(monomial (∑ i in t, Finsupp.single i 1)) 1) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
simp only [← single_eq_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (∑ x in powersetLen n univ, Finsupp.single (∑ i in x, Finsupp.single i 1) 1) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
refine' Finsupp.support_sum_eq_biUnion (powersetLen n (univ : Finset σ)) _
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ ∀ (i₁ i₂ : Finset σ),
    i₁ ≠ i₂ →
      Disjoint (Finsupp.single (∑ i in i₁, Finsupp.single i 1) 1).support
        (Finsupp.single (∑ i in i₂, Finsupp.single i 1) 1).support
[PROOFSTEP]
intro s t hst
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ Disjoint (Finsupp.single (∑ i in s, Finsupp.single i 1) 1).support
    (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [Finset.disjoint_left, Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i in s, Finsupp.single i 1} → ¬a ∈ (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i in s, Finsupp.single i 1} → ¬a ∈ {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
simp only [one_ne_zero, mem_singleton, Finsupp.mem_support_iff]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a = ∑ i in s, Finsupp.single i 1 → ¬a = ∑ i in t, Finsupp.single i 1
[PROOFSTEP]
rintro a h rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
⊢ False
[PROOFSTEP]
have := congr_arg Finsupp.support h
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ False
[PROOFSTEP]
rw [Finsupp.support_sum_eq_biUnion, Finsupp.support_sum_eq_biUnion] at this
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = { x } :=
  by
  intros _ x _
  rw [Finsupp.support_single_ne_zero x one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
⊢ ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
[PROOFSTEP]
intros _ x _
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
s✝ : Finset σ
x : σ
a✝ : x ∈ s✝
⊢ (Finsupp.single x 1).support = {x}
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero x one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
rw [hs, ht] at this
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun a => {a}) = Finset.biUnion s fun a => {a}
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
⊢ False
[PROOFSTEP]
simp only [biUnion_singleton_eq_self] at this
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
this : t = s
⊢ False
[PROOFSTEP]
exact absurd this hst.symm
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
all_goals intro x y; simp [Finsupp.support_single_disjoint]
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
intro x y
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
x y : σ
⊢ x ≠ y → Disjoint (Finsupp.single x 1).support (Finsupp.single y 1).support
[PROOFSTEP]
simp [Finsupp.support_single_disjoint]
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
intro x y
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
x y : σ
⊢ x ≠ y → Disjoint (Finsupp.single x 1).support (Finsupp.single y 1).support
[PROOFSTEP]
simp [Finsupp.support_single_disjoint]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) = Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
rw [support_esymm'']
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support) =
    Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
congr
[GOAL]
case e_t
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support) = fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
funext
[GOAL]
case e_t.h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
x✝ : Finset σ
⊢ (Finsupp.single (∑ i in x✝, Finsupp.single i 1) 1).support = {∑ i in x✝, Finsupp.single i 1}
[PROOFSTEP]
exact Finsupp.support_single_ne_zero _ one_ne_zero
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) = image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
[PROOFSTEP]
rw [support_esymm']
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}) =
    image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
[PROOFSTEP]
exact biUnion_singleton
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
classical
have : (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i : σ in t, Finsupp.single i 1) = Finset.val :=
  by
  funext
  simp [Finsupp.toMultiset_sum_single]
rw [degrees_def, support_esymm, sup_image, this]
have : ((powersetLen n univ).sup (fun (x : Finset σ) => x)).val = sup (powersetLen n univ) val :=
  by
  refine' comp_sup_eq_sup_comp _ _ _
  · intros
    simp only [union_val, sup_eq_union]
    congr
  · rfl
rw [← this]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
simpa using powersetLen_sup _ _ (Nat.lt_of_succ_le hn)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
have : (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i : σ in t, Finsupp.single i 1) = Finset.val :=
  by
  funext
  simp [Finsupp.toMultiset_sum_single]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
[PROOFSTEP]
funext
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) x✝ = x✝.val
[PROOFSTEP]
simp [Finsupp.toMultiset_sum_single]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
rw [degrees_def, support_esymm, sup_image, this]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ sup (powersetLen n univ) val = univ.val
[PROOFSTEP]
have : ((powersetLen n univ).sup (fun (x : Finset σ) => x)).val = sup (powersetLen n univ) val :=
  by
  refine' comp_sup_eq_sup_comp _ _ _
  · intros
    simp only [union_val, sup_eq_union]
    congr
  · rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
[PROOFSTEP]
refine' comp_sup_eq_sup_comp _ _ _
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val
[PROOFSTEP]
intros
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val
[PROOFSTEP]
simp only [union_val, sup_eq_union]
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val
[PROOFSTEP]
congr
[GOAL]
case refine'_2
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ sup (powersetLen n univ) val = univ.val
[PROOFSTEP]
rw [← this]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ (sup (powersetLen n univ) fun x => x).val = univ.val
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
[GOAL]
case intro
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < Nat.succ k
hn : Nat.succ k ≤ Fintype.card σ
this : (sup (powersetLen (Nat.succ k) univ) fun x => x).val = sup (powersetLen (Nat.succ k) univ) val
⊢ (sup (powersetLen (Nat.succ k) univ) fun x => x).val = univ.val
[PROOFSTEP]
simpa using powersetLen_sup _ _ (Nat.lt_of_succ_le hn)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ psum σ R 0 = ↑(Fintype.card σ)
[PROOFSTEP]
simp only [psum, _root_.pow_zero, ← cast_card]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ ↑(card univ) = ↑(Fintype.card σ)
[PROOFSTEP]
exact rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ psum σ R 1 = ∑ i : σ, X i
[PROOFSTEP]
simp only [psum, _root_.pow_one]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ↑(rename ↑e) (psum σ R n) = psum τ R n
[PROOFSTEP]
simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]


[GOAL]
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n : ℕ
⊢ ↑n ∈ s
[PROOFSTEP]
induction n
[GOAL]
case zero
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
⊢ ↑Nat.zero ∈ s
[PROOFSTEP]
simp [zero_mem, add_mem, one_mem, *]
[GOAL]
case succ
S : Type u_1
R : Type u_2
inst✝² : AddMonoidWithOne R
inst✝¹ : SetLike S R
s : S
inst✝ : AddSubmonoidWithOneClass S R
n✝ : ℕ
n_ih✝ : ↑n✝ ∈ s
⊢ ↑(Nat.succ n✝) ∈ s
[PROOFSTEP]
simp [zero_mem, add_mem, one_mem, *]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝¹ : NonAssocSemiring R
M : Submonoid R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
n : ℕ
⊢ ↑n ∈ s
[PROOFSTEP]
rw [← nsmul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝¹ : NonAssocSemiring R
M : Submonoid R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
n : ℕ
⊢ n • 1 ∈ s
[PROOFSTEP]
exact nsmul_mem (one_mem _) _
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
n : ℕ
⊢ ↑(x ^ n) = ↑x ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
⊢ ↑(x ^ Nat.zero) = ↑x ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ Nat.succ n) = ↑x ^ Nat.succ n
[PROOFSTEP]
simp [pow_succ, ih]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
p q : Subsemiring R
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
q : Subsemiring R
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } =
    (fun s => s.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s => s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubmonoid
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s => s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s
[PROOFSTEP]
simpa only [← hm] using sm.mul_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 1 ∈ { carrier := s, mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) }.carrier
[PROOFSTEP]
exact hm ▸ sm.one_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈
      { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) },
            one_mem' :=
              (_ :
                1 ∈
                  { carrier := s,
                      mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) }.carrier) }.toSubsemigroup.carrier →
    y ∈
        { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) },
              one_mem' :=
                (_ :
                  1 ∈
                    { carrier := s,
                        mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) }.carrier) }.toSubsemigroup.carrier →
      x + y ∈
        { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) },
              one_mem' :=
                (_ :
                  1 ∈
                    { carrier := s,
                        mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) }.carrier) }.toSubsemigroup.carrier
[PROOFSTEP]
simpa only [← ha] using sa.add_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈
    { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := s,
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) }.carrier) }.toSubsemigroup.carrier
[PROOFSTEP]
exact ha ▸ sa.zero_mem
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
s✝ : Subsemiring R✝
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : { x // x ∈ s }
n : ℕ
⊢ ↑(x ^ n) = ↑x ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
s✝ : Subsemiring R✝
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : { x // x ∈ s }
⊢ ↑(x ^ Nat.zero) = ↑x ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
s✝ : Subsemiring R✝
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : { x // x ∈ s }
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ Nat.succ n) = ↑x ^ Nat.succ n
[PROOFSTEP]
simp [pow_succ, ih]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s✝ : Subsemiring R
f : R →+* S
s : Subsemiring R
y : S
⊢ y ∈ map f s ↔ ∃ x, x ∈ s ∧ ↑f x = y
[PROOFSTEP]
convert Set.mem_image_iff_bex (f := f) (s := s.carrier) (y := y) using 1
[GOAL]
case h.e'_2.a
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s✝ : Subsemiring R
f : R →+* S
s : Subsemiring R
y : S
⊢ (∃ x, x ∈ s ∧ ↑f x = y) ↔ ∃ x x_1, ↑f x = y
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f✝ f : R →+* S
⊢ rangeS f = Subsemiring.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ rangeS f ↔ x✝ ∈ Subsemiring.map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g (rangeS f) = rangeS (comp g f)
[PROOFSTEP]
simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set (Subsemiring R)
⊢ ↑(⨅ (t : Subsemiring R) (_ : t ∈ s), t.toSubmonoid) = ⋂ (t : Subsemiring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set (Subsemiring R)
⊢ ↑(⨅ (t : Subsemiring R) (_ : t ∈ s), toAddSubmonoid t) = ⋂ (t : Subsemiring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f : R ≃+* S
K : Subsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ ↑(RingEquiv.symm f) x ∈ K
[PROOFSTEP]
convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x using 1
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
⊢ subsemiringClosure M = Subsemiring.closure ↑M
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
⊢ x✝ ∈ subsemiringClosure M ↔ x✝ ∈ Subsemiring.closure ↑M
[PROOFSTEP]
refine' ⟨fun hx => _, fun hx => (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => _⟩
[GOAL]
case h.refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ subsemiringClosure M
⊢ x✝ ∈ Subsemiring.closure ↑M
[PROOFSTEP]
rintro - ⟨H1, rfl⟩
[GOAL]
case h.refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑(subsemiringClosure M)
[PROOFSTEP]
rintro - ⟨H1, rfl⟩
[GOAL]
case h.refine'_1.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ subsemiringClosure M
H1 : Subsemiring R
⊢ x✝ ∈ (fun t => ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
[PROOFSTEP]
rintro - ⟨H2, rfl⟩
[GOAL]
case h.refine'_2.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t => ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
[PROOFSTEP]
rintro - ⟨H2, rfl⟩
[GOAL]
case h.refine'_1.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ subsemiringClosure M
H1 : Subsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2
[PROOFSTEP]
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
[GOAL]
case h.refine'_2.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2
[PROOFSTEP]
exact H2 sM
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))
[PROOFSTEP]
simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
[PROOFSTEP]
refine' ⟨fun hx => _, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
[PROOFSTEP]
rintro - ⟨H, rfl⟩
[GOAL]
case h.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
[PROOFSTEP]
rintro - ⟨J, rfl⟩
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J
[PROOFSTEP]
refine' (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => _
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑(toAddSubmonoid H)
[PROOFSTEP]
refine' (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => _
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid
[PROOFSTEP]
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ p a ha
[PROOFSTEP]
refine' Exists.elim _ fun (ha : a ∈ closure s) (hc : p a ha) => hc
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∃ x, p a x
[PROOFSTEP]
refine' closure_induction ha (fun m hm => ⟨subset_closure hm, Hs m hm⟩) ⟨zero_mem _, H0⟩ ⟨one_mem _, H1⟩ ?_ ?_
[GOAL]
case refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x + y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨add_mem hx' hy', Hadd _ _ _ _ hx hy⟩)
[GOAL]
case refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x * y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨mul_mem hx' hy', Hmul _ _ _ _ hx hy⟩)
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s ↔ ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
[PROOFSTEP]
intro hx
[GOAL]
case mp
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
[PROOFSTEP]
let p : R → Prop := fun x =>
  ∃ (L : List (List R)), (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ (List.map List.prod L).sum = x
[GOAL]
case mp
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
p : R → Prop := fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
⊢ ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
[PROOFSTEP]
exact
  AddSubmonoid.closure_induction (p := p) (mem_closure_iff.1 hx)
    (fun x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by rw [List.map_singleton, List.sum_singleton, ht2]⟩
      Submonoid.closure_induction hx (fun x hx => ⟨[x], List.forall_mem_singleton.2 hx, one_mul x⟩)
        ⟨[], List.forall_mem_nil _, rfl⟩ fun x y ⟨t, ht1, ht2⟩ ⟨u, hu1, hu2⟩ =>
        ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩)
    ⟨[], List.forall_mem_nil _, rfl⟩ fun x y ⟨L, HL1, HL2⟩ ⟨M, HM1, HM2⟩ =>
    ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by rw [List.map_append, List.sum_append, HL2, HM2]⟩
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝³ : R
hx✝ : x✝³ ∈ closure s
p : R → Prop := fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
x✝² : R
hx : x✝² ∈ ↑(Submonoid.closure s)
x y : R
x✝¹ : ∃ t, (∀ (y : R), y ∈ t → y ∈ s) ∧ List.prod t = x
x✝ : ∃ t, (∀ (y : R), y ∈ t → y ∈ s) ∧ List.prod t = y
t : List R
ht1 : ∀ (y : R), y ∈ t → y ∈ s
ht2 : List.prod t = x
u : List R
hu1 : ∀ (y : R), y ∈ u → y ∈ s
hu2 : List.prod u = y
⊢ List.prod (t ++ u) = x * y
[PROOFSTEP]
rw [List.prod_append, ht2, hu2]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ : R
hx✝ : x✝ ∈ closure s
p : R → Prop := fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
x : R
hx : x ∈ ↑(Submonoid.closure s)
this : ∃ t, (∀ (y : R), y ∈ t → y ∈ s) ∧ List.prod t = x
t : List R
ht1 : ∀ (y : R), y ∈ t → y ∈ s
ht2 : List.prod t = x
⊢ List.sum (List.map List.prod [t]) = x
[PROOFSTEP]
rw [List.map_singleton, List.sum_singleton, ht2]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M✝ : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝² : R
hx : x✝² ∈ closure s
p : R → Prop := fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x
x y : R
x✝¹ : p x
x✝ : p y
L : List (List R)
HL1 : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s
HL2 : List.sum (List.map List.prod L) = x
M : List (List R)
HM1 : ∀ (t : List R), t ∈ M → ∀ (y : R), y ∈ t → y ∈ s
HM2 : List.sum (List.map List.prod M) = y
⊢ List.sum (List.map List.prod (L ++ M)) = x + y
[PROOFSTEP]
rw [List.map_append, List.sum_append, HL2, HM2]
[GOAL]
case mpr
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s) ∧ List.sum (List.map List.prod L) = x) → x ∈ closure s
[PROOFSTEP]
rintro ⟨L, HL1, HL2⟩
[GOAL]
case mpr.intro.intro
R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
L : List (List R)
HL1 : ∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s
HL2 : List.sum (List.map List.prod L) = x
⊢ x ∈ closure s
[PROOFSTEP]
exact
  HL2 ▸
    list_sum_mem fun r hr =>
      let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
      ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Subsemiring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (RingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Subsemiring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (RingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : Subsemiring R :=
  Subsemiring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid)
    (Submonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id) (⨆ i, (S i).toAddSubmonoid)
    (AddSubmonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
      -- Porting note: gave the hypothesis an explicit name because `@this` doesn't work
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid) (⨆ (i : ι), toAddSubmonoid (S i))
    (_ : ↑(⨆ (i : ι), toAddSubmonoid (S i)) = ⋃ (i : ι), ↑(toAddSubmonoid (S i)))
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices h : ⨆ i, S i ≤ U by simpa using @h x
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid) (⨆ (i : ι), toAddSubmonoid (S i))
    (_ : ↑(⨆ (i : ι), toAddSubmonoid (S i)) = ⋃ (i : ι), ↑(toAddSubmonoid (S i)))
h : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa using @h x
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid) (⨆ (i : ι), toAddSubmonoid (S i))
    (_ : ↑(⨆ (i : ι), toAddSubmonoid (S i)) = ⋃ (i : ι), ↑(toAddSubmonoid (S i)))
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
S : Set (Subsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
S : Set (Subsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S✝
inst✝ : NonAssocSemiring T
S : Set (Subsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subsemiring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝⁷ : NonAssocSemiring R
M : Submonoid R
inst✝⁶ : NonAssocSemiring S
inst✝⁵ inst✝⁴ : NonAssocSemiring T
s : Subsemiring R
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
f : R →+* S
⊢ ↑(rangeS f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_rangeS, coe_top]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ↑f
src✝ : R →+* { x // x ∈ RingHom.rangeS f } := RingHom.rangeSRestrict f
x : { x // x ∈ RingHom.rangeS f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [Subsemiring.coe_mul]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x y : { x // x ∈ closure s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
refine'
  closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [zero_mul, mul_zero])
    (fun x => by simp only [zero_mul, mul_zero]) (fun x => by simp only [one_mul, mul_one])
    (fun x => by simp only [one_mul, mul_one]) (fun x y z h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x y z h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x y z h₁ h₂ => by rw [mul_assoc, h₂, ← mul_assoc, h₁, mul_assoc]) fun x y z h₁ h₂ => by
    rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y : { x // x ∈ closure s }
x : R'
⊢ 0 * x = x * 0
[PROOFSTEP]
simp only [zero_mul, mul_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y : { x // x ∈ closure s }
x : R'
⊢ x * 0 = 0 * x
[PROOFSTEP]
simp only [zero_mul, mul_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y : { x // x ∈ closure s }
x : R'
⊢ 1 * x = x * 1
[PROOFSTEP]
simp only [one_mul, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y : { x // x ∈ closure s }
x : R'
⊢ x * 1 = 1 * x
[PROOFSTEP]
simp only [one_mul, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y z : R'
h₁ : x * z = z * x
h₂ : y * z = z * y
⊢ (x + y) * z = z * (x + y)
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y z : R'
h₁ : x * y = y * x
h₂ : x * z = z * x
⊢ x * (y + z) = (y + z) * x
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y z : R'
h₁ : x * z = z * x
h₂ : y * z = z * y
⊢ x * y * z = z * (x * y)
[PROOFSTEP]
rw [mul_assoc, h₂, ← mul_assoc, h₁, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R
M : Submonoid R
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Semiring R'
s : Set R'
hcomm : ∀ (a : R'), a ∈ s → ∀ (b : R'), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ closure s } := toSemiring (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y z : R'
h₁ : x * y = y * x
h₂ : x * z = z * x
⊢ x * (y * z) = y * z * x
[PROOFSTEP]
rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]