[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
⊢ coeSubmodule S ⊥ = ⊥
[PROOFSTEP]
rw [coeSubmodule, Submodule.map_bot]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
⊢ coeSubmodule S ⊤ = 1
[PROOFSTEP]
rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (↑(algebraMap R S) '' s)
[PROOFSTEP]
rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
s : Set R
⊢ Submodule.span R (↑(Algebra.linearMap R S) '' s) = Submodule.span R (↑(algebraMap R S) '' s)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
x : R
⊢ coeSubmodule S (Ideal.span {x}) = Submodule.span R {↑(algebraMap R S) x}
[PROOFSTEP]
rw [coeSubmodule_span, Set.image_singleton]
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
h : IsNoetherianRing R
⊢ IsNoetherianRing S
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_wellFounded] at h ⊢
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
h : WellFounded fun x x_1 => x > x_1
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal (coeSubmodule S I) ↔ Submodule.IsPrincipal I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal (coeSubmodule S I) → Submodule.IsPrincipal I
[PROOFSTEP]
rintro ⟨⟨x, hx⟩⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ Submodule.IsPrincipal I → Submodule.IsPrincipal (coeSubmodule S I)
[PROOFSTEP]
rintro ⟨⟨x, hx⟩⟩
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = Submodule.span R {x}
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = Submodule.span R {x}
x_mem : x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
[GOAL]
case mp.mk.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
x_mem : ↑(algebraMap R S) x ∈ coeSubmodule S I
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
refine' ⟨⟨x, coeSubmodule_injective S h _⟩⟩
[GOAL]
case mp.mk.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left✝ : x ∈ I
hx : coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
x_mem : ↑(algebraMap R S) x ∈ coeSubmodule S I
⊢ coeSubmodule S I = coeSubmodule S (Submodule.span R {x})
[PROOFSTEP]
rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
[GOAL]
case mpr.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = Submodule.span R {x}
⊢ Submodule.IsPrincipal (coeSubmodule S I)
[PROOFSTEP]
refine' ⟨⟨algebraMap R S x, _⟩⟩
[GOAL]
case mpr.mk.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = Submodule.span R {x}
⊢ coeSubmodule S I = Submodule.span R {↑(algebraMap R S) x}
[PROOFSTEP]
rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a ↔ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
case mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → x ∈ Submodule.span S a
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
refine' Submodule.span_induction h _ _ _ _
[GOAL]
case mp.refine'_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (x : N), x ∈ a → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
rintro x hx
[GOAL]
case mp.refine'_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ x = mk' S 1 1 • x
[PROOFSTEP]
rw [mk'_one, _root_.map_one, one_smul]
[GOAL]
case mp.refine'_2
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∃ y, y ∈ Submodule.span R a ∧ ∃ z, 0 = mk' S 1 z • y
[PROOFSTEP]
exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ 0 = mk' S 1 1 • 0
[PROOFSTEP]
rw [mk'_one, _root_.map_one, one_smul]
[GOAL]
case mp.refine'_3
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (x y : N),
    (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) →
      (∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z, y = mk' S 1 z • y_1) →
        ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z, x + y = mk' S 1 z • y_1
[PROOFSTEP]
rintro _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z_1, mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1
[PROOFSTEP]
refine'
  ⟨(z' : R) • y + (z : R) • y', Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', _⟩
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • (↑z' • y + ↑z • y')
[PROOFSTEP]
rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ← IsScalarTower.algebraMap_smul S (z' : R), smul_smul,
  smul_smul]
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z') • y + (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z) • y'
[PROOFSTEP]
congr 1
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro.e_a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z • y = (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z') • y
[PROOFSTEP]
rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, _root_.map_one, mul_one, mul_one]
[GOAL]
case mp.refine'_3.intro.intro.intro.intro.intro.intro.e_a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : N
hy' : y' ∈ Submodule.span R a
z' : { x // x ∈ M }
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * ↑(algebraMap R S) ↑z) • y'
[PROOFSTEP]
rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, _root_.map_one, mul_one, one_mul]
[GOAL]
case mp.refine'_4
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (a_1 : S) (x : N),
    (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → ∃ y, y ∈ Submodule.span R a ∧ ∃ z, a_1 • x = mk' S 1 z • y
[PROOFSTEP]
rintro a _ ⟨y, hy, z, rfl⟩
[GOAL]
case mp.refine'_4.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a✝ : Set N
h : x ∈ Submodule.span S a✝
a : S
y : N
hy : y ∈ Submodule.span R a✝
z : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a✝ ∧ ∃ z_1, a • mk' S 1 z • y = mk' S 1 z_1 • y_1
[PROOFSTEP]
obtain ⟨y', z', rfl⟩ := mk'_surjective M a
[GOAL]
case mp.refine'_4.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : R
z' : { x // x ∈ M }
⊢ ∃ y_1, y_1 ∈ Submodule.span R a ∧ ∃ z_1, mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1
[PROOFSTEP]
refine' ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, _⟩
[GOAL]
case mp.refine'_4.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
y' : R
z' : { x // x ∈ M }
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul, mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]
[GOAL]
case mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ (∃ y, y ∈ Submodule.span R a ∧ ∃ z, x = mk' S 1 z • y) → x ∈ Submodule.span S a
[PROOFSTEP]
rintro ⟨y, hy, z, rfl⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝⁷ : CommRing Q
inst✝⁶ : Algebra P Q
inst✝⁵ : IsLocalization T Q
inst✝⁴ : IsLocalization M S
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
a : Set N
y : N
hy : y ∈ Submodule.span R a
z : { x // x ∈ M }
⊢ mk' S 1 z • y ∈ Submodule.span S a
[PROOFSTEP]
exact Submodule.smul_mem _ _ (Submodule.span_subset_span R S _ hy)
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ x ∈ Ideal.span (↑(algebraMap R S) '' a) ↔ ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
refine' (mem_span_iff M).trans _
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y) ↔
    ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y) →
    ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
rw [← coeSubmodule_span]
[GOAL]
case mp
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ coeSubmodule S (Ideal.span a) ∧ ∃ z, x = mk' S 1 z • y) → ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : { x // x ∈ M }
hz : x = mk' S 1 z • ↑(Algebra.linearMap R S) y
⊢ ∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z
[PROOFSTEP]
refine' ⟨y, hy, z, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : { x // x ∈ M }
hz : x = mk' S 1 z • ↑(Algebra.linearMap R S) y
⊢ x = mk' S y z
[PROOFSTEP]
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
[GOAL]
case mpr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y, y ∈ Ideal.span a ∧ ∃ z, x = mk' S y z) →
    ∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
rintro ⟨y, hy, z, hz⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : { x // x ∈ M }
hz : x = mk' S y z
⊢ ∃ y, y ∈ Submodule.span R (↑(algebraMap R S) '' a) ∧ ∃ z, x = mk' S 1 z • y
[PROOFSTEP]
refine' ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, _⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
g : R →+* P
T : Submonoid P
hy✝ : M ≤ Submonoid.comap g T
Q : Type u_4
inst✝³ : CommRing Q
inst✝² : Algebra P Q
inst✝¹ : IsLocalization T Q
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : { x // x ∈ M }
hz : x = mk' S y z
⊢ x = mk' S 1 z • ↑(algebraMap R S) y
[PROOFSTEP]
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]


[GOAL]
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ #L ≤ #R
[PROOFSTEP]
classical
cases fintypeOrInfinite R
· exact Cardinal.mk_le_of_surjective (IsArtinianRing.localization_surjective S _)
erw [← Cardinal.mul_eq_self <| Cardinal.aleph0_le_mk R]
set f : R × R → L := fun aa => IsLocalization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1)
refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
use(x, y)
dsimp
rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]
[GOAL]
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ #L ≤ #R
[PROOFSTEP]
cases fintypeOrInfinite R
[GOAL]
case inl
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Fintype R
⊢ #L ≤ #R
[PROOFSTEP]
exact Cardinal.mk_le_of_surjective (IsArtinianRing.localization_surjective S _)
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
⊢ #L ≤ #R
[PROOFSTEP]
erw [← Cardinal.mul_eq_self <| Cardinal.aleph0_le_mk R]
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
⊢ #L ≤ #R * #R
[PROOFSTEP]
set f : R × R → L := fun aa => IsLocalization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1)
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
⊢ #L ≤ #R * #R
[PROOFSTEP]
refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
⊢ ∃ a_1, f a_1 = a
[PROOFSTEP]
obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
[GOAL]
case inr.intro.intro
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ ∃ a_1, f a_1 = a
[PROOFSTEP]
use(x, y)
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ f (x, ↑y) = a
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ mk' L x (if h : ↑y ∈ S then { val := ↑y, property := h } else 1) = a
[PROOFSTEP]
rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]


[GOAL]
n : ℕ
⊢ hermite (n + 1) = X * hermite n - ↑derivative (hermite n)
[PROOFSTEP]
rw [hermite]
[GOAL]
n : ℕ
⊢ hermite n = (fun p => X * p - ↑derivative p)^[n] 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ hermite Nat.zero = (fun p => X * p - ↑derivative p)^[Nat.zero] 1
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
ih : hermite n = (fun p => X * p - ↑derivative p)^[n] 1
⊢ hermite (Nat.succ n) = (fun p => X * p - ↑derivative p)^[Nat.succ n] 1
[PROOFSTEP]
rw [Function.iterate_succ_apply', ← ih, hermite_succ]
[GOAL]
⊢ hermite 1 = X
[PROOFSTEP]
rw [hermite_succ, hermite_zero]
[GOAL]
⊢ X * ↑C 1 - ↑derivative (↑C 1) = X
[PROOFSTEP]
simp only [map_one, mul_one, derivative_one, sub_zero]
[GOAL]
n : ℕ
⊢ coeff (hermite (n + 1)) 0 = -coeff (hermite n) 1
[PROOFSTEP]
simp [coeff_derivative]
[GOAL]
n k : ℕ
⊢ coeff (hermite (n + 1)) (k + 1) = coeff (hermite n) k - (↑k + 2) * coeff (hermite n) (k + 2)
[PROOFSTEP]
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]
[GOAL]
n k : ℕ
⊢ coeff (hermite n) k - (↑(k + 1) + 1) * coeff (hermite n) (k + 1 + 1) =
    coeff (hermite n) k - (↑k + 2) * coeff (hermite n) (k + 2)
[PROOFSTEP]
norm_cast
[GOAL]
n k : ℕ
hnk : n < k
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk
[GOAL]
case intro
n k : ℕ
hnk : n < n + k + 1
⊢ coeff (hermite n) (n + k + 1) = 0
[PROOFSTEP]
clear hnk
[GOAL]
case intro
n k : ℕ
⊢ coeff (hermite n) (n + k + 1) = 0
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case intro.zero
k✝ k : ℕ
⊢ coeff (hermite Nat.zero) (Nat.zero + k + 1) = 0
[PROOFSTEP]
apply coeff_C
[GOAL]
case intro.succ
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n + k + 1) = 0
[PROOFSTEP]
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
[GOAL]
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
⊢ n + k + 1 + 2 = n + (k + 2) + 1
[PROOFSTEP]
ring
[GOAL]
case intro.succ
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n + k + 1) = 0
[PROOFSTEP]
rw [Nat.succ_eq_add_one, coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
[GOAL]
n : ℕ
⊢ coeff (hermite n) n = 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ coeff (hermite Nat.zero) Nat.zero = 1
[PROOFSTEP]
apply coeff_C
[GOAL]
case succ
n : ℕ
ih : coeff (hermite n) n = 1
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n) = 1
[PROOFSTEP]
rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
[GOAL]
case succ
n : ℕ
ih : coeff (hermite n) n = 1
⊢ n < n + 2
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ degree (hermite n) = ↑n
[PROOFSTEP]
rw [degree_eq_of_le_of_coeff_ne_zero]
[GOAL]
case pn
n : ℕ
⊢ degree (hermite n) ≤ ↑n
case p1 n : ℕ ⊢ coeff (hermite n) n ≠ 0
[PROOFSTEP]
simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
[GOAL]
case pn
n : ℕ
⊢ ∀ (m : ℕ), n < m → coeff (hermite n) m = 0
[PROOFSTEP]
rintro m hnm
[GOAL]
case pn
n m : ℕ
hnm : n < m
⊢ coeff (hermite n) m = 0
[PROOFSTEP]
exact coeff_hermite_of_lt hnm
[GOAL]
case p1
n : ℕ
⊢ coeff (hermite n) n ≠ 0
[PROOFSTEP]
simp [coeff_hermite_self n]
[GOAL]
n : ℕ
⊢ leadingCoeff (hermite n) = 1
[PROOFSTEP]
rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]
[GOAL]
n k : ℕ
hnk : Odd (n + k)
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case zero
n k✝ : ℕ
hnk✝ : Odd (n + k✝)
k : ℕ
hnk : Odd (Nat.zero + k)
⊢ coeff (hermite Nat.zero) k = 0
[PROOFSTEP]
rw [Nat.zero_eq, zero_add k] at hnk
[GOAL]
case zero
n k✝ : ℕ
hnk✝ : Odd (n + k✝)
k : ℕ
hnk : Odd k
⊢ coeff (hermite Nat.zero) k = 0
[PROOFSTEP]
exact coeff_hermite_of_lt hnk.pos
[GOAL]
case succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + k)
⊢ coeff (hermite (Nat.succ n)) k = 0
[PROOFSTEP]
cases' k with k
[GOAL]
case succ.zero
n✝ k : ℕ
hnk✝ : Odd (n✝ + k)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
hnk : Odd (Nat.succ n + Nat.zero)
⊢ coeff (hermite (Nat.succ n)) Nat.zero = 0
[PROOFSTEP]
rw [Nat.succ_add_eq_succ_add] at hnk
[GOAL]
case succ.zero
n✝ k : ℕ
hnk✝ : Odd (n✝ + k)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
hnk : Odd (n + Nat.succ Nat.zero)
⊢ coeff (hermite (Nat.succ n)) Nat.zero = 0
[PROOFSTEP]
rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ coeff (hermite (Nat.succ n)) (Nat.succ k) = 0
[PROOFSTEP]
rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Odd (n + (k + 2))
[PROOFSTEP]
rwa [Nat.succ_add_eq_succ_add] at hnk
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Odd (n + k)
[PROOFSTEP]
rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
[GOAL]
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Nat.succ n + Nat.succ k = n + k + 2
[PROOFSTEP]
rw [Nat.succ_add, Nat.add_succ]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)
[PROOFSTEP]
exact (Nat.odd_add.mp hnk).mpr even_two
[GOAL]
x✝ : ℕ
⊢ coeff (hermite (2 * 0 + x✝)) x✝ = (-1) ^ 0 * ↑(2 * 0 - 1)‼ * ↑(Nat.choose (2 * 0 + x✝) x✝)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ coeff (hermite (2 * (n + 1) + 0)) 0 = (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + 0) 0)
[PROOFSTEP]
convert coeff_hermite_succ_zero (2 * n + 1) using 1
  -- porting note: ring_nf did not solve the goal on line 165
[GOAL]
case h.e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + 0) 0) = -coeff (hermite (2 * n + 1)) 1
[PROOFSTEP]
rw [coeff_hermite_explicit n 1, (by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1),
  Nat.doubleFactorial_add_one, Nat.choose_zero_right, Nat.choose_one_right, pow_succ]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1
[PROOFSTEP]
rw [Nat.left_distrib, mul_one, Nat.succ_sub_one]
[GOAL]
case h.e'_3
n : ℕ
⊢ -1 * (-1) ^ n * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑1 = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(2 * n + 1))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3
n : ℕ
⊢ -1 * (-1) ^ n * ((2 * ↑n + 1) * ↑(2 * n - 1)‼) * 1 = -((-1) ^ n * ↑(2 * n - 1)‼ * (2 * ↑n + 1))
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
let hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * (2 * n - 1)‼ * Nat.choose (2 * n + k) k
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
have hermite_explicit_recur :
  ∀ n k : ℕ, hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (k + 2) * hermite_explicit n (k + 2) :=
  by
  intro n k
  simp only
    -- Factor out (-1)'s.
  rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
  nth_rw 3 [neg_eq_neg_one_mul]
  simp only [mul_assoc, ← mul_add, pow_succ]
  congr 2
    -- Factor out double factorials.
  norm_cast
    -- porting note: ring_nf did not solve the goal on line 186
  rw [(by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one,
    mul_comm (2 * n + 1)]
  simp only [mul_assoc, ← mul_add]
  congr 1
    -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
  rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1), (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
    (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
  rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel, Int.negSucc_eq]
    -- porting note: ring could not solve the goal so the lines 195, 198-200 were added.
  ring_nf
  simp only [sub_eq_add_neg, ← neg_mul, ← right_distrib _ _ ((-(1 : ℤ)) ^ n), ← neg_add]
  norm_cast
  simp only [← add_assoc, add_comm]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
⊢ ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
intro n k
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
simp only
  -- Factor out (-1)'s.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) -
      (↑k + 2) * ((-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)))
[PROOFSTEP]
rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) +
      -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))
[PROOFSTEP]
nth_rw 3 [neg_eq_neg_one_mul]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) +
      -((-1 * 1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))
[PROOFSTEP]
simp only [mul_assoc, ← mul_add, pow_succ]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k))) +
      -((-1 * 1) ^ n * (↑(2 * n - 1)‼ * (↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))))
[PROOFSTEP]
congr 2
  -- Factor out double factorials.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k))) +
      -((-1 * 1) ^ n * (↑(2 * n - 1)‼ * (↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))))
[PROOFSTEP]
norm_cast
  -- porting note: ring_nf did not solve the goal on line 186
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * (n + 1) - 1)‼ * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * (n + 1) - 1)‼ * Nat.choose (2 * (n + 1) + k) k)) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [(by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one,
  mul_comm (2 * n + 1)]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1
[PROOFSTEP]
rw [Nat.left_distrib, mul_one, Nat.succ_sub_one]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * (2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * (2 * n + 1) * Nat.choose (2 * (n + 1) + k) k)) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
simp only [mul_assoc, ← mul_add]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + k) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
congr 1
  -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + k) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1), (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
  (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) + k = 2 * n + 1 + (k + 1)
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * n + (k + 2) = 2 * n + 1 + (k + 1)
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1) + 1) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1)) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + 1 + (k + 1)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel, Int.negSucc_eq]
  -- porting note: ring could not solve the goal so the lines 195, 198-200 were added.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -(↑0 + 1) *
      ((-(↑0 + 1)) ^ n *
        ↑((2 * n - 1)‼ *
            ((2 * n + 1) * (Nat.choose (2 * n + 1 + (k + 1)) k + Nat.choose (2 * n + 1 + (k + 1)) (k + 1))))) =
    -(↑0 + 1) * ((-(↑0 + 1)) ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1)) k))) +
      -((-(↑0 + 1) * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + 1 + (k + 1)) (k + 1) * (2 * n + 1))))
[PROOFSTEP]
ring_nf
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
        (-1) ^ n) =
    -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k) * (-1) ^ n) -
      ↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
        (-1) ^ n
[PROOFSTEP]
simp only [sub_eq_add_neg, ← neg_mul, ← right_distrib _ _ ((-(1 : ℤ)) ^ n), ← neg_add]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
      (-1) ^ n =
    -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k) +
          ↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k))) *
      (-1) ^ n
[PROOFSTEP]
norm_cast
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
      Int.negSucc 0 ^ n =
    -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k))) *
      Int.negSucc 0 ^ n
[PROOFSTEP]
simp only [← add_assoc, add_comm]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
change _ = hermite_explicit _ _
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) = hermite_explicit (n + 1) (k + 1)
[PROOFSTEP]
rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) k - (↑k + 2) * coeff (hermite (2 * (n + 1) + k)) (k + 2) =
    hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
congr
[GOAL]
case e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) k = hermite_explicit (n + 1) k
[PROOFSTEP]
rw [coeff_hermite_explicit (n + 1) k]
[GOAL]
case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) (k + 2) = hermite_explicit n (k + 2)
[PROOFSTEP]
rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
  -- porting note: Lean 3 worked this out automatically
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ 2 * (n + 1) + k = 2 * n + (k + 2)
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
hnk : Even (n + k)
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
cases' le_or_lt k n with h_le h_lt
[GOAL]
case inl
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
rw [Nat.even_add, ← Nat.even_sub h_le] at hnk
[GOAL]
case inl
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hnk
[GOAL]
case inl.intro
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
rw [(by linarith [by rwa [Nat.sub_eq_iff_eq_add h_le] at hm ] : n = 2 * m + k), Nat.add_sub_cancel,
  Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]
[GOAL]
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k
[PROOFSTEP]
linarith [by rwa [Nat.sub_eq_iff_eq_add h_le] at hm ]
[GOAL]
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ ?m.206711
[PROOFSTEP]
rwa [Nat.sub_eq_iff_eq_add h_le] at hm
[GOAL]
case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]
[GOAL]
n k : ℕ
⊢ coeff (hermite n) k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n k : ℕ
h : Even (n + k)
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
case neg n k : ℕ h : ¬Even (n + k) ⊢ coeff (hermite n) k = 0
[PROOFSTEP]
exact coeff_hermite_of_even_add h
[GOAL]
case neg
n k : ℕ
h : ¬Even (n + k)
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
exact coeff_hermite_of_odd_add (Nat.odd_iff_not_even.mpr h)