Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv (DividedPowers/IdealAdd.lean)

State before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Ring.inverse (C a) = C (Ring.inverse a)
Tactic:
simp only [Ring.inverse]
State after:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)

State before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
by_cases ha : IsUnit a
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)

case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
simp only [dif_pos ha]
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Tactic:
have hCa : IsUnit (C a) := by
  rw [← IsUnit.unit_spec ha]
  exact RingHom.isUnit_map C ha
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C ↑ha.unit⁻¹
Tactic:
rw [dif_pos hCa]
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ = C ↑ha.unit⁻¹

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ = C ↑ha.unit⁻¹
Tactic:
apply IsUnit.mul_right_cancel hCa
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C ↑ha.unit⁻¹ * C a

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C ↑ha.unit⁻¹ * C a
Tactic:
rw [← map_mul]
State after:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C (↑ha.unit⁻¹ * a)

State before:
case pos
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
hCa : IsUnit (C a)
⊢ ↑hCa.unit⁻¹ * C a = C (↑ha.unit⁻¹ * a)
Tactic:
simp only [IsUnit.val_inv_mul, map_one]
State after:
no goals

State before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C a)
Tactic:
rw [← IsUnit.unit_spec ha]
State after:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C ↑ha.unit)

State before:
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : IsUnit a
⊢ IsUnit (C ↑ha.unit)
Tactic:
exact RingHom.isUnit_map C ha
State after:
no goals

State before:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = C (if h : IsUnit a then ↑h.unit⁻¹ else 0)
Tactic:
simp only [Ring.inverse, dif_neg ha, map_zero]
State after:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = 0

State before:
case neg
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ (if h : IsUnit (C a) then ↑h.unit⁻¹ else 0) = 0
Tactic:
rw [dif_neg]
State after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ ¬IsUnit (C a)

State before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
⊢ ¬IsUnit (C a)
Tactic:
intro hCa
State after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ False

State before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ False
Tactic:
apply ha
State after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ IsUnit a

State before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : IsUnit (C a)
⊢ IsUnit a
Tactic:
rw [isUnit_iff_exists_inv] at hCa ⊢
State after:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : ∃ b, C a * b = 1
⊢ ∃ b, a * b = 1

State before:
case neg.hnc
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
hCa : ∃ b, C a * b = 1
⊢ ∃ b, a * b = 1
Tactic:
obtain ⟨b, hb⟩ := hCa
State after:
case neg.hnc.intro
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ∃ b, a * b = 1

State before:
case neg.hnc.intro
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ∃ b, a * b = 1
Tactic:
use b.coeff 0
State after:
case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = 1

State before:
case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = 1
Tactic:
convert congr_arg₂ coeff hb rfl
State after:
case h.e'_2
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = (C a * b).coeff ?h

case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 ?h

case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ℕ

State before:
case h.e'_2
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = (C a * b).coeff ?h

case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 ?h

case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ℕ
Tactic:
rw [Polynomial.coeff_C_mul]
State after:
case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 0

State before:
case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 0
Tactic:
simp only [coeff_one_zero]
State after:
no goals