Theorem: DividedPowers.coincide_on_smul (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
a : A
ha : a ∈ I • J
⊢ hI.dpow n a = hJ.dpow n a
Tactic:
induction ha using Submodule.smul_induction_on' generalizing n with
| smul a ha b hb =>
  rw [Algebra.id.smul_eq_mul, hJ.dpow_smul n hb, mul_comm a b, hI.dpow_smul n ha, ←
    hJ.factorial_mul_dpow_eq_pow n b hb, ← hI.factorial_mul_dpow_eq_pow n a ha]
  ring
| add x hx y hy hx' hy' =>
  rw [hI.dpow_add n (Ideal.mul_le_right hx) (Ideal.mul_le_right hy),
    hJ.dpow_add n (Ideal.mul_le_left hx) (Ideal.mul_le_left hy)]
  apply Finset.sum_congr rfl
  intro k _
  rw [hx', hy']
State after:
no goals

State before:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a✝ a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ hI.dpow n (a • b) = hJ.dpow n (a • b)
Tactic:
rw [Algebra.id.smul_eq_mul, hJ.dpow_smul n hb, mul_comm a b, hI.dpow_smul n ha, ←
  hJ.factorial_mul_dpow_eq_pow n b hb, ← hI.factorial_mul_dpow_eq_pow n a ha]
State after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a✝ a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ ↑n.factorial * hJ.dpow n b * hI.dpow n a = ↑n.factorial * hI.dpow n a * hJ.dpow n b

State before:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a✝ a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ ↑n.factorial * hJ.dpow n b * hI.dpow n a = ↑n.factorial * hI.dpow n a * hJ.dpow n b
Tactic:
ring
State after:
no goals

State before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ hI.dpow n (x + y) = hJ.dpow n (x + y)
Tactic:
rw [hI.dpow_add n (Ideal.mul_le_right hx) (Ideal.mul_le_right hy),
  hJ.dpow_add n (Ideal.mul_le_left hx) (Ideal.mul_le_left hy)]
State after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 x * hJ.dpow k.2 y

State before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic:
apply Finset.sum_congr rfl
State after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y

State before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
Tactic:
intro k _
State after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ Finset.antidiagonal n
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y

State before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ Finset.antidiagonal n
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic:
rw [hx', hy']
State after:
no goals