internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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]
Proof 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)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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
Proof 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)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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
Proof 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)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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
Proof 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)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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⟩
Proof 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))
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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]
Proof 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))
Theorem: DividedPowers.isDPMorphism.of_comp
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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)
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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)
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof 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
Theorem: DividedPowers.dp_uniqueness_self
Proof 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]
Proof 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
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.dp_uniqueness_self
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.dp_uniqueness_self
Proof 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]
Proof state after:
no goals
Theorem: Polynomial.coeff_baseChange_apply
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ ((baseChange φ) f).coeff p = φ (f.coeff p)
Tactic:
rw [baseChange, AlgHom.coe_mk, coe_eval₂RingHom]
Proof state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)
Theorem: Polynomial.coeff_baseChange_apply
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : S[X]
p : ℕ
⊢ (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)
Tactic:
induction f using Polynomial.induction_on with
| h_C r =>
  simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C,
    apply_ite φ, map_zero]
| h_add f g hf hg => simp only [eval₂_add, coeff_add, hf, hg, map_add]
| h_monomial n r _ =>
  simp only [eval₂_mul, eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
    eval₂_X_pow, coeff_C_mul, _root_.map_mul, coeff_X_pow, apply_ite φ, _root_.map_one, map_zero]
Proof state after:
no goals
Theorem: Polynomial.coeff_baseChange_apply
Proof state before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
r : S
⊢ (eval₂ (C.comp ↑φ) X (C r)).coeff p = φ ((C r).coeff p)
Tactic:
simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C,
  apply_ite φ, map_zero]
Proof state after:
no goals
Theorem: Polynomial.coeff_baseChange_apply
Proof state before:
case h_add
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f g : S[X]
hf : (eval₂ (C.comp ↑φ) X f).coeff p = φ (f.coeff p)
hg : (eval₂ (C.comp ↑φ) X g).coeff p = φ (g.coeff p)
⊢ (eval₂ (C.comp ↑φ) X (f + g)).coeff p = φ ((f + g).coeff p)
Tactic:
simp only [eval₂_add, coeff_add, hf, hg, map_add]
Proof state after:
no goals
Theorem: Polynomial.coeff_baseChange_apply
Proof state before:
case h_monomial
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p n : ℕ
r : S
a✝ : (eval₂ (C.comp ↑φ) X (C r * X ^ n)).coeff p = φ ((C r * X ^ n).coeff p)
⊢ (eval₂ (C.comp ↑φ) X (C r * X ^ (n + 1))).coeff p = φ ((C r * X ^ (n + 1)).coeff p)
Tactic:
simp only [eval₂_mul, eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
  eval₂_X_pow, coeff_C_mul, _root_.map_mul, coeff_X_pow, apply_ite φ, _root_.map_one, map_zero]
Proof state after:
no goals
Theorem: Polynomial.lcoeff_comp_baseChange_eq
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
⊢ φ.toLinearMap ∘ₗ ↑R (lcoeff S p) = ↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap
Tactic:
ext f
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f : S[X]
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S p)) f = (↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap) f
Theorem: Polynomial.lcoeff_comp_baseChange_eq
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
p : ℕ
f : S[X]
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S p)) f = (↑R (lcoeff S' p) ∘ₗ (baseChange φ).toLinearMap) f
Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, lcoeff_apply,
  AlgHom.toLinearMap_apply, coeff_baseChange_apply]
Proof state after:
no goals
Theorem: Polynomial.baseChange_monomial
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
a : S
⊢ (baseChange φ) ((monomial n) a) = (monomial n) (φ a)
Tactic:
simp only [baseChange, AlgHom.coe_mk, coe_eval₂RingHom, eval₂_monomial, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply, C_mul_X_pow_eq_monomial]
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
μ : S ⊗[R] M
⊢ ∃ m, μ = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
classical
induction μ using TensorProduct.induction_on with
| zero => use 0; simp
| tmul s m => use single s m; simp
| add x y hx hy =>
  obtain ⟨sx, rfl⟩ := hx
  obtain ⟨sy, rfl⟩ := hy
  use sx + sy
  rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
μ : S ⊗[R] M
⊢ ∃ m, μ = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
induction μ using TensorProduct.induction_on with
| zero => use 0; simp
| tmul s m => use single s m; simp
| add x y hx hy =>
  obtain ⟨sx, rfl⟩ := hx
  obtain ⟨sy, rfl⟩ := hy
  use sx + sy
  rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ ∃ m, 0 = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
use 0
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ 0 = sum 0 fun s x => s ⊗ₜ[R] x
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ 0 = sum 0 fun s x => s ⊗ₜ[R] x
Tactic:
simp
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case tmul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ ∃ m_1, s ⊗ₜ[R] m = m_1.sum fun s x => s ⊗ₜ[R] x
Tactic:
use single s m
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ s ⊗ₜ[R] m = (Finsupp.single s m).sum fun s x => s ⊗ₜ[R] x
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : S
m : M
⊢ s ⊗ₜ[R] m = (Finsupp.single s m).sum fun s x => s ⊗ₜ[R] x
Tactic:
simp
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∃ m, x = m.sum fun s x => s ⊗ₜ[R] x
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
⊢ ∃ m, x + y = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
obtain ⟨sx, rfl⟩ := hx
Proof state after:
case add.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
y : S ⊗[R] M
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
sx : S →₀ M
⊢ ∃ m, (sx.sum fun s x => s ⊗ₜ[R] x) + y = m.sum fun s x => s ⊗ₜ[R] x