-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem maximalIdeal_eq_span_X : IsLocalRing.maximalIdeal (k⟦X⟧) = Ideal.span {X}

Proof state:
case left
k : Type u_2
inst✝ : Field k
⊢ ¬X ∣ 1

Tactic:
exact Prime.not_dvd_one X_prime

Result:
no goals

Proof state:
case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
intro I f hI hfX hfI

Result:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
⊢ 1 ∈ I

Proof state:
k : Type u_2
inst✝ : Field k
⊢ (Ideal.span {X}).IsMaximal

Tactic:
rw [Ideal.isMaximal_iff]

Result:
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Proof state:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ (C k) (f 0) ∈ I

Tactic:
rw [this]

Result:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (f - (C k) (f 0)) ∈ I

Proof state:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (C k) (f 0) ∈ I

Tactic:
apply hI

Result:
case a
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (C k) (f 0) ∈ Ideal.span {X}

Proof state:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
⊢ (C k) (f 0) = f - (f - (C k) (f 0))

Tactic:
rw [sub_sub_cancel]

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
constructor

Result:
case left
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X}

case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Proof state:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (f - (C k) (f 0)) ∈ I

Tactic:
apply Ideal.sub_mem I hfI

Result:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (C k) (f 0) ∈ I

Proof state:
k : Type u_2
inst✝ : Field k
hX : (Ideal.span {X}).IsMaximal
⊢ IsLocalRing.maximalIdeal k⟦X⟧ = Ideal.span {X}

Tactic:
rw [IsLocalRing.eq_maximalIdeal hX]

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
⊢ (C k) (f 0) ∈ I

Tactic:
have : C k (f 0) = f - (f - C k (f 0)) := by rw [sub_sub_cancel]

Result:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ (C k) (f 0) ∈ I

Proof state:
case left
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X}

Tactic:
rw [Ideal.mem_span_singleton]

Result:
case left
k : Type u_2
inst✝ : Field k
⊢ ¬X ∣ 1

Proof state:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
hfI0 : (C k) (f 0) ∈ I
⊢ I = ⊤

Tactic:
apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map (C k) (Ne.isUnit hfX))

Result:
no goals

Proof state:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
hfI0 : (C k) (f 0) ∈ I
⊢ 1 ∈ I

Tactic:
rw [← Ideal.eq_top_iff_one]

Result:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
hfI0 : (C k) (f 0) ∈ I
⊢ I = ⊤

Proof state:
case a
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ f - (C k) (f 0) ∈ Ideal.span {X}

Tactic:
rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
  coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]

Result:
case a
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ (constantCoeff k) f = f 0

Proof state:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
⊢ 1 ∈ I

Tactic:
have hfI0 : C k (f 0) ∈ I := by
  have : C k (f 0) = f - (f - C k (f 0)) := by rw [sub_sub_cancel]
  rw [this]
  apply Ideal.sub_mem I hfI
  apply hI
  rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
    coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
  rfl

Result:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
hfI0 : (C k) (f 0) ∈ I
⊢ 1 ∈ I

Proof state:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
⊢ 1 ∈ I

Tactic:
rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX

Result:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
⊢ 1 ∈ I

Proof state:
case a
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬(constantCoeff k) f = 0
hfI : f ∈ I
this : (C k) (f 0) = f - (f - (C k) (f 0))
⊢ (constantCoeff k) f = f 0

Tactic:
rfl

Result:
no goals