internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.roby_theorem_2
Proof state before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ (dividedPowers' R M).isDPMorphism hI ↑(lift hI φ hφ)
Tactic:
apply cond_D_uniqueness
Proof state after:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ∀ (n : ℕ) (x : M), (dividedPowers' R M).dpow n ((ι R M) x) = dp R n x
Theorem: DividedPowerAlgebra.roby_theorem_2
Proof state before:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ∀ (n : ℕ) (x : M), (dividedPowers' R M).dpow n ((ι R M) x) = dp R n x
Tactic:
intro m n
Proof state after:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : ℕ
n : M
⊢ (dividedPowers' R M).dpow m ((ι R M) n) = dp R m n
Theorem: DividedPowerAlgebra.roby_theorem_2
Proof state before:
case hh
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : ℕ
n : M
⊢ (dividedPowers' R M).dpow m ((ι R M) n) = dp R m n
Tactic:
rw [dpow_ι]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
have hφ : ∀ m, ((ι S N).restrictScalars R).comp f m ∈ augIdeal S N := by
  intro m
  simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply, ι_mem_augIdeal S N (f m)]
Proof state after:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
use hφ
Proof state after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
apply DividedPowerAlgebra.ext
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∀ (n : ℕ) (m : M), (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∀ (n : ℕ) (m : M), (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Tactic:
intro n m
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Tactic:
simp only [liftAlgHom_apply_dp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply]
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Tactic:
simp only [LinearMap.liftAlgHom_dp]
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Tactic:
simp only [ι, LinearMap.coe_mk, AddHom.coe_mk]
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n (dp S 1 (f m))
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n (dp S 1 (f m))
Tactic:
rw [dp_comp _ _ _ _ Nat.one_ne_zero]
Proof state after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = ↑(mchoose n 1) * dp S (n * 1) (f m)
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = ↑(mchoose n 1) * dp S (n * 1) (f m)
Tactic:
simp only [mchoose_one', Nat.cast_one, mul_one, one_mul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
⊢ ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
Tactic:
intro m
Proof state after:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
m : M
⊢ (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
Theorem: DividedPowerAlgebra.lift'_eq_dp_lift
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
m : M
⊢ (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, ι_mem_augIdeal S N (f m)]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby_prop_8
Proof state before:
R : Type u
inst✝¹⁰ : DecidableEq R
inst✝⁹ : CommRing R
M : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type u
inst✝⁶ : DecidableEq S
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
⊢ (dividedPowers' R M).isDPMorphism (dividedPowers' S N) ↑(LinearMap.lift R S f)
Tactic:
obtain ⟨hφ, phφ'⟩ := lift'_eq_dp_lift R S f
Proof state after:
case intro
R : Type u
inst✝¹⁰ : DecidableEq R
inst✝⁹ : CommRing R
M : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type u
inst✝⁶ : DecidableEq S
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
phφ' : LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
⊢ (dividedPowers' R M).isDPMorphism (dividedPowers' S N) ↑(LinearMap.lift R S f)
Theorem: DividedPowerAlgebra.roby_prop_8
Proof state before:
case intro
R : Type u
inst✝¹⁰ : DecidableEq R
inst✝⁹ : CommRing R
M : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type u
inst✝⁶ : DecidableEq S
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
phφ' : LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
⊢ (dividedPowers' R M).isDPMorphism (dividedPowers' S N) ↑(LinearMap.lift R S f)
Tactic:
convert roby_theorem_2 R M (dividedPowers' S N) hφ
Proof state after:
no goals
Theorem: DividedPowers.add_dpowExp
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ hI.dpowExp (a + b) = hI.dpowExp a * hI.dpowExp b
Tactic:
ext n
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
n : ℕ
⊢ (PowerSeries.coeff A n) (hI.dpowExp (a + b)) = (PowerSeries.coeff A n) (hI.dpowExp a * hI.dpowExp b)
Theorem: DividedPowers.add_dpowExp
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
a b : A
ha : a ∈ I
hb : b ∈ I
n : ℕ
⊢ (PowerSeries.coeff A n) (hI.dpowExp (a + b)) = (PowerSeries.coeff A n) (hI.dpowExp a * hI.dpowExp b)
Tactic:
simp only [dpowExp, PowerSeries.coeff_mk, PowerSeries.coeff_mul, hI.dpow_add n ha hb,
  Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
Proof state after:
no goals
Theorem: DividedPowers.eq_of_eq_on_ideal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'
Tactic:
ext n x
Proof state after:
case dpow.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
⊢ hI.dpow n x = hI'.dpow n x
Theorem: DividedPowers.eq_of_eq_on_ideal
Proof state before:
case dpow.h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
by_cases hx : x ∈ I
Proof state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
hx : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
hx : x ∉ I
⊢ hI.dpow n x = hI'.dpow n x
Theorem: DividedPowers.eq_of_eq_on_ideal
Proof state before:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
hx : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
exact h_eq n hx
Proof state after:
no goals
Theorem: DividedPowers.eq_of_eq_on_ideal
Proof state before:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
n : ℕ
x : A
hx : x ∉ I
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
rw [hI.dpow_null hx, hI'.dpow_null hx]
Proof state after:
no goals
Theorem: DividedPowers.dpow_smul'
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
a x : A
hx : x ∈ I
⊢ hI.dpow n (a • x) = a ^ n • hI.dpow n x
Tactic:
simp only [smul_eq_mul, hI.dpow_smul, hx]
Proof state after:
no goals
Theorem: DividedPowers.dpow_mul_right
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
a : A
ha : a ∈ I
x : A
⊢ hI.dpow n (a * x) = hI.dpow n a * x ^ n
Tactic:
rw [mul_comm, hI.dpow_smul n ha, mul_comm]
Proof state after:
no goals
Theorem: DividedPowers.dpow_smul_right
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
a : A
ha : a ∈ I
x : A
⊢ hI.dpow n (a • x) = hI.dpow n a • x ^ n
Tactic:
rw [smul_eq_mul, hI.dpow_mul_right n ha, smul_eq_mul]
Proof state after:
no goals
Theorem: DividedPowers.factorial_mul_dpow_eq_pow
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
x : A
hx : x ∈ I
⊢ ↑n.factorial * hI.dpow n x = x ^ n
Tactic:
induction n with
| zero => rw [Nat.factorial_zero, Nat.cast_one, one_mul, pow_zero, hI.dpow_zero hx]
| add_one n ih =>
  rw [Nat.factorial_succ, mul_comm (n + 1)]
  nth_rewrite 1 [← (n + 1).choose_one_right]
  rw [← Nat.choose_symm_add, Nat.cast_mul, mul_assoc,
    ← hI.dpow_mul n 1 hx, ← mul_assoc, ih, hI.dpow_one hx, pow_succ', mul_comm]
Proof state after:
no goals
Theorem: DividedPowers.factorial_mul_dpow_eq_pow
Proof state before:
case zero
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
⊢ ↑(Nat.factorial 0) * hI.dpow 0 x = x ^ 0
Tactic:
rw [Nat.factorial_zero, Nat.cast_one, one_mul, pow_zero, hI.dpow_zero hx]
Proof state after:
no goals
Theorem: DividedPowers.factorial_mul_dpow_eq_pow
Proof state before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n + 1).factorial * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
rw [Nat.factorial_succ, mul_comm (n + 1)]
Proof state after:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1)) * hI.dpow (n + 1) x = x ^ (n + 1)
Theorem: DividedPowers.factorial_mul_dpow_eq_pow
Proof state before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1)) * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
nth_rewrite 1 [← (n + 1).choose_one_right]
Proof state after:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1).choose 1) * hI.dpow (n + 1) x = x ^ (n + 1)
Theorem: DividedPowers.factorial_mul_dpow_eq_pow
Proof state before:
case add_one
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x : A
hx : x ∈ I
n : ℕ
ih : ↑n.factorial * hI.dpow n x = x ^ n
⊢ ↑(n.factorial * (n + 1).choose 1) * hI.dpow (n + 1) x = x ^ (n + 1)
Tactic:
rw [← Nat.choose_symm_add, Nat.cast_mul, mul_assoc,
  ← hI.dpow_mul n 1 hx, ← mul_assoc, ih, hI.dpow_one hx, pow_succ', mul_comm]
Proof state after:
no goals
Theorem: DividedPowers.dpow_eval_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Tactic:
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_smul n I.zero_mem,
  zero_pow hn, zero_mul, zero_mul]
Proof state after:
no goals
Theorem: DividedPowers.nilpotent_of_mem_dpIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
have h_fac : (n.factorial : A) * hI.dpow n x =
  n • ((n - 1).factorial : A) * hI.dpow n x := by
  rw [nsmul_eq_mul, ← Nat.cast_mul, Nat.mul_factorial_pred (Nat.pos_of_ne_zero hn)]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ x ^ n = 0
Theorem: DividedPowers.nilpotent_of_mem_dpIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ x ^ n = 0
Tactic:
rw [← factorial_mul_dpow_eq_pow hI _ _ hx, h_fac, smul_mul_assoc]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ n • (↑(n - 1).factorial * hI.dpow n x) = 0
Theorem: DividedPowers.nilpotent_of_mem_dpIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ n • (↑(n - 1).factorial * hI.dpow n x) = 0
Tactic:
exact hnI (I.mul_mem_left ((n - 1).factorial : A) (hI.dpow_mem hn hx))
Proof state after:
no goals
Theorem: DividedPowers.nilpotent_of_mem_dpIdeal
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
⊢ ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
Tactic:
rw [nsmul_eq_mul, ← Nat.cast_mul, Nat.mul_factorial_pred (Nat.pos_of_ne_zero hn)]
Proof state after:
no goals
Theorem: DividedPowers.coincide_on_smul
Proof 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']
Proof state after:
no goals
Theorem: DividedPowers.coincide_on_smul
Proof 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]
Proof 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
Theorem: DividedPowers.coincide_on_smul
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.coincide_on_smul
Proof 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)]
Proof 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