case zero
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ comap f K ^ Nat.zero ≤ comap f (K ^ Nat.zero)

case succ
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ Nat.succ n ≤ comap f (K ^ Nat.succ n)
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
n : ℕ
⊢ comap f K ^ n ≤ comap f (K ^ n)
induction' n with n n_ih
case zero
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ ⊤ ≤ comap f ⊤
case zero
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ comap f K ^ Nat.zero ≤ comap f (K ^ Nat.zero)
rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
no goals
case zero
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
⊢ ⊤ ≤ comap f ⊤
exact rfl.le
case succ
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K * comap f K ^ n ≤ comap f (K * K ^ n)
case succ
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ Nat.succ n ≤ comap f (K ^ Nat.succ n)
rw [pow_succ, pow_succ]
no goals
case succ
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K * comap f K ^ n ≤ comap f (K * K ^ n)
exact (Ideal.mul_mono_right n_ih).trans (Ideal.le_comap_mul f)