Theorem: DividedPowers.dp_uniqueness_self (DividedPowers/DPMorphism.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
⊢ hI' = hI
Tactic:
ext n a
State after:
case dpow.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
⊢ hI'.dpow n a = hI.dpow n a

State before:
case dpow.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
⊢ hI'.dpow n a = hI.dpow n a
Tactic:
by_cases ha : a ∈ I
State after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a

State before:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a
Tactic:
. refine' hI.dp_uniqueness hI' (RingHom.id A) hS _ _ n a ha
  . intro s hs
    simp only [RingHom.id_apply, hS]
    exact Ideal.subset_span hs
  . simpa only [RingHom.id_apply] using hdp
State after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a

State before:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a
Tactic:
refine' hI.dp_uniqueness hI' (RingHom.id A) hS _ _ n a ha
State after:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ s ∈ S, (RingHom.id A) s ∈ I

case pos.refine'_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)

State before:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ s ∈ S, (RingHom.id A) s ∈ I

case pos.refine'_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)
Tactic:
. intro s hs
  simp only [RingHom.id_apply, hS]
  exact Ideal.subset_span hs
State after:
case pos.refine'_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)

State before:
case pos.refine'_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)
Tactic:
. simpa only [RingHom.id_apply] using hdp
State after:
no goals

State before:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ s ∈ S, (RingHom.id A) s ∈ I
Tactic:
intro s hs
State after:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
s : A
hs : s ∈ S
⊢ (RingHom.id A) s ∈ I

State before:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
s : A
hs : s ∈ S
⊢ (RingHom.id A) s ∈ I
Tactic:
simp only [RingHom.id_apply, hS]
State after:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
s : A
hs : s ∈ S
⊢ s ∈ Ideal.span S

State before:
case pos.refine'_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
s : A
hs : s ∈ S
⊢ s ∈ Ideal.span S
Tactic:
exact Ideal.subset_span hs
State after:
no goals

State before:
case pos.refine'_2
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)
Tactic:
simpa only [RingHom.id_apply] using hdp
State after:
no goals

State before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = Ideal.span S
hdp : ∀ (n : ℕ), ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a
Tactic:
rw [hI.dpow_null ha, hI'.dpow_null ha]
State after:
no goals