Theorem: DividedPowers.isDPMorphism.of_comp (DividedPowers/DPMorphism.lean)

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
⊢ hI.isDPMorphism hJ f → hI.isDPMorphism hK h → hJ.isDPMorphism hK g
Tactic:
intro hf hh
State after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ hJ.isDPMorphism hK g

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ hJ.isDPMorphism hK g
Tactic:
apply isDPMorphism_on_span
State after:
case hS
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ J = Ideal.span ?S

case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ?S, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ?S, g (hJ.dpow n a) = hK.dpow n (g a)

case S
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ Set B

State before:
case hS
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ J = Ideal.span ?S

case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ?S, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ?S, g (hJ.dpow n a) = hK.dpow n (g a)

case S
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ Set B
Tactic:
exact sf
State after:
case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ⇑f '' ↑I, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ⇑f '' ↑I, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rintro b ⟨a, ha, rfl⟩
State after:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ g (f a) ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ g (f a) ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rw [← RingHom.comp_apply]
State after:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ (g.comp f) a ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ (g.comp f) a ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rw [hcomp]
State after:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ h a ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ h a ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
apply hh.1
State after:
case hS'.intro.intro.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ h a ∈ Ideal.map h I

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'.intro.intro.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ h a ∈ Ideal.map h I

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
apply Ideal.mem_map_of_mem
State after:
case hS'.intro.intro.a.h
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ a ∈ I

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hS'.intro.intro.a.h
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ a ∈ I

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
exact ha
State after:
case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)

State before:
case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rintro n b ⟨a, ha, rfl⟩
State after:
case hdp.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = hK.dpow n (g (f a))

State before:
case hdp.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = hK.dpow n (g (f a))
Tactic:
rw [← RingHom.comp_apply, hcomp, hh.2 n a ha, ← hcomp, RingHom.comp_apply]
State after:
case hdp.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = g (f (hI.dpow n a))

State before:
case hdp.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = g (f (hI.dpow n a))
Tactic:
rw [hf.2 n a ha]
State after:
no goals