[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
[PROOFSTEP]
rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
[GOAL]
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
[PROOFSTEP]
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
[GOAL]
case intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
[PROOFSTEP]
refine' fg_def.2 ⟨p * q, hp.mul hq, le_antisymm _ _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ span R (p * q) ≤ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))
[PROOFSTEP]
rw [span_le]
[GOAL]
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ p * q ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
[PROOFSTEP]
change x * y ∈ adjoin R (s ∪ t)
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x * y ∈ adjoin R (s ∪ t)
[PROOFSTEP]
refine' Subalgebra.mul_mem _ _ _
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)
[PROOFSTEP]
have : x ∈ Subalgebra.toSubmodule (adjoin R s) := by
  rw [← hp']
  exact subset_span hx
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
[PROOFSTEP]
rw [← hp']
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ span R p
[PROOFSTEP]
exact subset_span hx
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ x ∈ adjoin R (s ∪ t)
[PROOFSTEP]
exact adjoin_mono (Set.subset_union_left _ _) this
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ adjoin R (s ∪ t)
[PROOFSTEP]
have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) :=
  by
  rw [← hq']
  exact subset_span hy
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
[PROOFSTEP]
rw [← hq']
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ span { x // x ∈ adjoin R s } q
[PROOFSTEP]
exact subset_span hy
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
[PROOFSTEP]
change y ∈ adjoin R (s ∪ t)
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
[PROOFSTEP]
rwa [adjoin_union_eq_adjoin_adjoin]
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)
[PROOFSTEP]
intro r hr
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))
⊢ r ∈ span R (p * q)
[PROOFSTEP]
change r ∈ adjoin R (s ∪ t) at hr
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ adjoin R (s ∪ t)
⊢ r ∈ span R (p * q)
[PROOFSTEP]
rw [adjoin_union_eq_adjoin_adjoin] at hr
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ Subalgebra.restrictScalars R (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
[PROOFSTEP]
change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
[PROOFSTEP]
rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_total (adjoin R s)] at hr
[GOAL]
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr :
  ∃ l,
    l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q ∧
      ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l = r
⊢ r ∈ span R (p * q)
[PROOFSTEP]
rcases hr with ⟨l, hlq, rfl⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
[PROOFSTEP]
have := @Finsupp.total_apply A A (adjoin R s)
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
[PROOFSTEP]
rw [this, Finsupp.sum]
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finset.sum l.support fun a => ↑l a • _root_.id a) ∈ span R (p * q)
[PROOFSTEP]
refine' sum_mem _
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l.support → ↑l c • _root_.id c ∈ span R (p * q)
[PROOFSTEP]
intro z hz
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑l z • _root_.id z ∈ span R (p * q)
[PROOFSTEP]
change (l z).1 * _ ∈ _
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ↑(↑l z) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_total R] at this
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ∃ l_1, l_1 ∈ Finsupp.supported R R p ∧ ↑(Finsupp.total A A R _root_.id) l_1 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
rcases this with ⟨l2, hlp, hl⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
have := @Finsupp.total_apply A A R
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
rw [this] at hl
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
rw [← hl, Finsupp.sum_mul]
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finsupp.sum l2 fun a c => c • _root_.id a * _root_.id z) ∈ span R (p * q)
[PROOFSTEP]
refine' sum_mem _
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l2.support → (fun a c => c • _root_.id a * _root_.id z) c (↑l2 c) ∈ span R (p * q)
[PROOFSTEP]
intro t ht
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ (fun a c => c • _root_.id a * _root_.id z) t (↑l2 t) ∈ span R (p * q)
[PROOFSTEP]
change _ * _ ∈ _
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • _root_.id t * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
rw [smul_mul_assoc]
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • (_root_.id t * _root_.id z) ∈ span R (p * q)
[PROOFSTEP]
refine' smul_mem _ _ _
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ _root_.id t * _root_.id z ∈ span R (p * q)
[PROOFSTEP]
exact subset_span ⟨t, z, hlp ht, hlq hz, rfl⟩
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
x✝ : Submodule.FG (↑toSubmodule S)
t : Finset A
ht : span R ↑t = ↑toSubmodule S
x : A
hx : x ∈ ↑toSubmodule S
⊢ x ∈ span R ↑t
[PROOFSTEP]
rw [ht]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
x✝ : Submodule.FG (↑toSubmodule S)
t : Finset A
ht : span R ↑t = ↑toSubmodule S
x : A
hx : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S
[PROOFSTEP]
exact hx
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Submodule.FG ⊤
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑toSubmodule (Algebra.adjoin R ↑s) = ↑toSubmodule ⊤
[PROOFSTEP]
rw [Algebra.top_toSubmodule, eq_top_iff, ← hs, span_le]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Submodule.FG ⊤
s : Finset A
hs : span R ↑s = ⊤
⊢ ↑s ⊆ ↑(↑toSubmodule (Algebra.adjoin R ↑s))
[PROOFSTEP]
exact Algebra.subset_adjoin
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : FG S
hT : FG T
⊢ FG (Subalgebra.prod S T)
[PROOFSTEP]
obtain ⟨s, hs⟩ := fg_def.1 hS
[GOAL]
case intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : FG S
hT : FG T
s : Set A
hs : Set.Finite s ∧ Algebra.adjoin R s = S
⊢ FG (Subalgebra.prod S T)
[PROOFSTEP]
obtain ⟨t, ht⟩ := fg_def.1 hT
[GOAL]
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : FG S
hT : FG T
s : Set A
hs : Set.Finite s ∧ Algebra.adjoin R s = S
t : Set B
ht : Set.Finite t ∧ Algebra.adjoin R t = T
⊢ FG (Subalgebra.prod S T)
[PROOFSTEP]
rw [← hs.2, ← ht.2]
[GOAL]
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : FG S
hT : FG T
s : Set A
hs : Set.Finite s ∧ Algebra.adjoin R s = S
t : Set B
ht : Set.Finite t ∧ Algebra.adjoin R t = T
⊢ FG (Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t))
[PROOFSTEP]
exact
  fg_def.2
    ⟨LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}),
      Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
        (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
      Algebra.adjoin_inl_union_inr_eq_prod R s t⟩
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : FG S
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R ↑(Finset.image (↑f) s) = Subalgebra.map f S
[PROOFSTEP]
rw [Finset.coe_image, Algebra.adjoin_image, hs]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f
      (Algebra.adjoin R
        ↑(Finset.preimage s ↑f
            (_ : ∀ (x : A), x ∈ ↑f ⁻¹' ↑s → ∀ (x_2 : A), x_2 ∈ ↑f ⁻¹' ↑s → ↑f x = ↑f x_2 → x = x_2))) =
    map f S
[PROOFSTEP]
rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ↑f
[PROOFSTEP]
rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ↑f
hs✝ : FG (map f S)
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
[PROOFSTEP]
exact map_mono le_top
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
h : FG ⊤
⊢ FG S
[PROOFSTEP]
rw [← S.range_val, ← Algebra.map_top]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
h : FG ⊤
⊢ FG (map (val S) ⊤)
[PROOFSTEP]
exact FG.map _ h
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
h : FG S
⊢ FG (map (val S) ⊤)
[PROOFSTEP]
rw [Algebra.map_top, range_val]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
h : FG S
⊢ FG S
[PROOFSTEP]
exact h
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
S : Subalgebra R A
⊢ P S
[PROOFSTEP]
classical
obtain ⟨t, rfl⟩ := S.fg_of_noetherian
refine' Finset.induction_on t _ _
· simpa using base
intro x t _ h
rw [Finset.coe_insert]
simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
S : Subalgebra R A
⊢ P S
[PROOFSTEP]
obtain ⟨t, rfl⟩ := S.fg_of_noetherian
[GOAL]
case intro
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑t)
[PROOFSTEP]
refine' Finset.induction_on t _ _
[GOAL]
case intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑∅)
[PROOFSTEP]
simpa using base
[GOAL]
case intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ ∀ ⦃a : A⦄ {s : Finset A}, ¬a ∈ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert a s))
[PROOFSTEP]
intro x t _ h
[GOAL]
case intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : ¬x ∈ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R ↑(insert x t))
[PROOFSTEP]
rw [Finset.coe_insert]
[GOAL]
case intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : ¬x ∈ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R (insert x ↑t))
[PROOFSTEP]
simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h


[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
x y : TruncatedWittVector p n R
h : x = y
i : Fin n
⊢ coeff i x = coeff i y
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
⊢ (mk p fun i => coeff i x) = x
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i (mk p fun i => coeff i x) = coeff i x
[PROOFSTEP]
rw [coeff_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ WittVector.coeff (out x) ↑i = coeff i x
[PROOFSTEP]
rw [out]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ WittVector.coeff { coeff := fun i => if h : i < n then coeff { val := i, isLt := h } x else 0 } ↑i = coeff i x
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ (if h : ↑i < n then coeff { val := ↑i, isLt := h } x else 0) = coeff i x
[PROOFSTEP]
rw [dif_pos i.is_lt, Fin.eta]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ Injective out
[PROOFSTEP]
intro x y h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : out x = out y
⊢ x = y
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : out x = out y
i : Fin n
⊢ coeff i x = coeff i y
[PROOFSTEP]
rw [WittVector.ext_iff] at h
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : ∀ (n_1 : ℕ), WittVector.coeff (out x) n_1 = WittVector.coeff (out y) n_1
i : Fin n
⊢ coeff i x = coeff i y
[PROOFSTEP]
simpa only [coeff_out] using h ↑i
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff i (truncateFun n x) = coeff x ↑i
[PROOFSTEP]
rw [truncateFun, TruncatedWittVector.coeff_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ TruncatedWittVector.out (truncateFun n x) = init n x
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ coeff (TruncatedWittVector.out (truncateFun n x)) i = coeff (init n x) i
[PROOFSTEP]
dsimp [TruncatedWittVector.out, init, select, coeff_mk]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ (if h : i < n then TruncatedWittVector.coeff { val := i, isLt := h } (truncateFun n x) else 0) =
    if i < n then coeff x i else 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff { val := i, isLt := hi } (truncateFun n x) = coeff x i
case neg p : ℕ hp : Fact (Nat.Prime p) n : ℕ R : Type u_1 inst✝ : CommRing R x : 𝕎 R i : ℕ hi : ¬i < n ⊢ 0 = 0
[PROOFSTEP]
swap
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff { val := i, isLt := hi } (truncateFun n x) = coeff x i
[PROOFSTEP]
rw [coeff_truncateFun, Fin.val_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
⊢ WittVector.truncateFun n (out x) = x
[PROOFSTEP]
simp only [WittVector.truncateFun, coeff_out, mk_coeff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
i : Fin n
⊢ coeff i 0 = 0
[PROOFSTEP]
show coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
i : Fin n
⊢ coeff i (truncateFun n 0) = 0
[PROOFSTEP]
rw [coeff_truncateFun, WittVector.zero_coeff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ truncateFun n (-x) = -truncateFun n x
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
m : ℕ
⊢ truncateFun n (m • x) = m • truncateFun n x
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
m : ℤ
⊢ truncateFun n (m • x) = m • truncateFun n x
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
m : ℕ
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m
[PROOFSTEP]
witt_truncateFun_tac
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ x ∈ RingHom.ker (truncate n) ↔ ∀ (i : ℕ), i < n → coeff x i = 0
[PROOFSTEP]
simp only [RingHom.mem_ker, truncate, truncateFun, RingHom.coe_mk, TruncatedWittVector.ext_iff,
  TruncatedWittVector.coeff_mk, coeff_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (∀ (i : Fin n),
      TruncatedWittVector.coeff i
          (↑{ toOneHom := { toFun := truncateFun n, map_one' := (_ : truncateFun n 1 = 1) },
                map_mul' := (_ : ∀ (x y : 𝕎 R), truncateFun n (x * y) = truncateFun n x * truncateFun n y) }
            x) =
        0) ↔
    ∀ (i : ℕ), i < n → coeff x i = 0
[PROOFSTEP]
exact Fin.forall_iff
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
f : ℕ → R
⊢ ↑(truncate n) { coeff := f } = TruncatedWittVector.mk p fun k => f ↑k
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
f : ℕ → R
i : Fin n
⊢ TruncatedWittVector.coeff i (↑(truncate n) { coeff := f }) =
    TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun k => f ↑k)
[PROOFSTEP]
simp only [coeff_truncate, TruncatedWittVector.coeff_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
⊢ RingHom.ker (WittVector.truncate m) ≤ RingHom.ker (WittVector.truncate n)
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ x ∈ RingHom.ker (WittVector.truncate m) → x ∈ RingHom.ker (WittVector.truncate n)
[PROOFSTEP]
simp only [WittVector.mem_ker_truncate]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ (∀ (i : ℕ), i < m → WittVector.coeff x i = 0) → ∀ (i : ℕ), i < n → WittVector.coeff x i = 0
[PROOFSTEP]
intro h i hi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : 𝕎 R
h : ∀ (i : ℕ), i < m → WittVector.coeff x i = 0
i : ℕ
hi : i < n
⊢ WittVector.coeff x i = 0
[PROOFSTEP]
exact h i (lt_of_lt_of_le hi hm)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ ↑(truncate h1) (↑(truncate h2) x) = ↑(truncate (_ : n₁ ≤ n₃)) x
[PROOFSTEP]
obtain ⟨x, rfl⟩ := @WittVector.truncate_surjective p _ n₃ R _ x
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : 𝕎 R
⊢ ↑(truncate h1) (↑(truncate h2) (↑(WittVector.truncate n₃) x)) =
    ↑(truncate (_ : n₁ ≤ n₃)) (↑(WittVector.truncate n₃) x)
[PROOFSTEP]
simp only [truncate_wittVector_truncate]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
⊢ RingHom.comp (truncate h1) (truncate h2) = truncate (_ : n₁ ≤ n₃)
[PROOFSTEP]
ext1 x
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ ↑(RingHom.comp (truncate h1) (truncate h2)) x = ↑(truncate (_ : n₁ ≤ n₃)) x
[PROOFSTEP]
simp only [truncate_truncate, Function.comp_apply, RingHom.coe_comp]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
⊢ Surjective ↑(truncate hm)
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p n R
⊢ ∃ a, ↑(truncate hm) a = x
[PROOFSTEP]
obtain ⟨x, rfl⟩ := @WittVector.truncate_surjective p _ _ R _ x
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ ∃ a, ↑(truncate hm) a = ↑(WittVector.truncate n) x
[PROOFSTEP]
exact ⟨WittVector.truncate _ x, truncate_wittVector_truncate _ _⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
i : Fin n
x : TruncatedWittVector p m R
⊢ coeff i (↑(truncate hm) x) = coeff (Fin.castLE hm i) x
[PROOFSTEP]
obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
hm : n ≤ m
i : Fin n
y : 𝕎 R
⊢ coeff i (↑(truncate hm) (↑(WittVector.truncate m) y)) = coeff (Fin.castLE hm i) (↑(WittVector.truncate m) y)
[PROOFSTEP]
simp only [truncate_wittVector_truncate, WittVector.coeff_truncate, Fin.coe_castLE]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_2
inst✝ : Fintype R
⊢ Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n
[PROOFSTEP]
simp only [TruncatedWittVector, Fintype.card_fin, Fintype.card_fun]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ ⨅ (i : ℕ), RingHom.ker (WittVector.truncate i) = ⊥
[PROOFSTEP]
rw [Submodule.eq_bot_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (x : 𝕎 R), x ∈ ⨅ (i : ℕ), RingHom.ker (WittVector.truncate i) → x = 0
[PROOFSTEP]
intro x hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
hx : x ∈ ⨅ (i : ℕ), RingHom.ker (WittVector.truncate i)
⊢ x = 0
[PROOFSTEP]
ext
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
hx : x ∈ ⨅ (i : ℕ), RingHom.ker (WittVector.truncate i)
n✝ : ℕ
⊢ WittVector.coeff x n✝ = WittVector.coeff 0 n✝
[PROOFSTEP]
simp only [WittVector.mem_ker_truncate, Ideal.mem_iInf, WittVector.zero_coeff] at hx ⊢
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n✝ : ℕ
hx : ∀ (i i_1 : ℕ), i_1 < i → WittVector.coeff x i_1 = 0
⊢ WittVector.coeff x n✝ = 0
[PROOFSTEP]
exact hx _ _ (Nat.lt_succ_self _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
⊢ ↑(truncate n) (liftFun f s) = ↑(f n) s
[PROOFSTEP]
ext i
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff i (↑(truncate n) (liftFun f s)) = TruncatedWittVector.coeff i (↑(f n) s)
[PROOFSTEP]
simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.last ↑i) (↑(f (↑i + 1)) s) = TruncatedWittVector.coeff i (↑(f n) s)
[PROOFSTEP]
rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
i : Fin n
⊢ TruncatedWittVector.coeff (Fin.castLE (_ : ↑i < n) (Fin.last ↑i)) (↑(f n) s) = TruncatedWittVector.coeff i (↑(f n) s)
[PROOFSTEP]
congr 1 with _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ S →+* 𝕎 R
[PROOFSTEP]
refine'
  { toFun := liftFun f
    map_zero' := _
    map_one' := _
    map_add' := _
    map_mul' := _ }
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 1 = 1
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 1 = 1
[PROOFSTEP]
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ ∀ (i : ℕ), liftFun f 1 - 1 ∈ RingHom.ker (truncate i)
[PROOFSTEP]
simp [RingHom.mem_ker, f_compat]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ ∀ (x y : S),
    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
        OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x✝ *
      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y✝
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ * y✝) = liftFun f x✝ * liftFun f y✝
[PROOFSTEP]
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ ∀ (i : ℕ), liftFun f (x✝ * y✝) - liftFun f x✝ * liftFun f y✝ ∈ RingHom.ker (truncate i)
[PROOFSTEP]
simp [RingHom.mem_ker, f_compat]
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : S),
                OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
      0 =
    0
[PROOFSTEP]
intros
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : S),
                OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
      0 =
    0
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 0 = 0
[PROOFSTEP]
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
[GOAL]
case refine'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ ∀ (i : ℕ), liftFun f 0 - 0 ∈ RingHom.ker (truncate i)
[PROOFSTEP]
simp [RingHom.mem_ker, f_compat]
[GOAL]
case refine'_4
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ ∀ (x y : S),
    OneHom.toFun
        (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : S),
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                        OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : S),
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                        OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
          y
[PROOFSTEP]
intros
[GOAL]
case refine'_4
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : S),
                OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
      (x✝ + y✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
        x✝ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } (x * y) =
                    OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } x *
                      OneHom.toFun { toFun := liftFun f, map_one' := (_ : liftFun f 1 = 1) } y) })
        y✝
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_4
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ + y✝) = liftFun f x✝ + liftFun f y✝
[PROOFSTEP]
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
[GOAL]
case refine'_4
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ y✝ : S
⊢ ∀ (i : ℕ), liftFun f (x✝ + y✝) - (liftFun f x✝ + liftFun f y✝) ∈ RingHom.ker (truncate i)
[PROOFSTEP]
simp [RingHom.mem_ker, f_compat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ RingHom.comp (truncate n) (lift (fun k₂ => f k₂) f_compat) = f n
[PROOFSTEP]
ext1
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x✝ : S
⊢ ↑(RingHom.comp (truncate n) (lift (fun k₂ => f k₂) f_compat)) x✝ = ↑(f n) x✝
[PROOFSTEP]
rw [RingHom.comp_apply, truncate_lift]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
⊢ lift (fun k₂ => f k₂) f_compat = g
[PROOFSTEP]
ext1 x
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
⊢ ↑(lift (fun k₂ => f k₂) f_compat) x = ↑g x
[PROOFSTEP]
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
⊢ ∀ (i : ℕ), ↑(lift (fun k₂ => f k₂) f_compat) x - ↑g x ∈ RingHom.ker (truncate i)
[PROOFSTEP]
intro i
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
i : ℕ
⊢ ↑(lift (fun k₂ => f k₂) f_compat) x - ↑g x ∈ RingHom.ker (truncate i)
[PROOFSTEP]
simp only [RingHom.mem_ker, g_compat, ← RingHom.comp_apply, truncate_comp_lift, RingHom.map_sub, sub_self]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
⊢ ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
    RingHom.comp (TruncatedWittVector.truncate hk) ((fun k => RingHom.comp (truncate k) g) k₂) =
      (fun k => RingHom.comp (truncate k) g) k₁
[PROOFSTEP]
intro _ _ h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
g : S →+* 𝕎 R
k₁✝ k₂✝ : ℕ
h : k₁✝ ≤ k₂✝
⊢ RingHom.comp (TruncatedWittVector.truncate h) ((fun k => RingHom.comp (truncate k) g) k₂✝) =
    (fun k => RingHom.comp (truncate k) g) k₁✝
[PROOFSTEP]
simp only [← RingHom.comp_assoc, truncate_comp_wittVector_truncate]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ Function.LeftInverse
    (fun g =>
      { val := fun k => RingHom.comp (truncate k) g,
        property :=
          (_ :
            ∀ (k₁ k₂ : ℕ) (h : k₁ ≤ k₂),
              RingHom.comp (RingHom.comp (TruncatedWittVector.truncate h) (truncate k₂)) g =
                RingHom.comp (truncate k₁) g) })
    fun f => lift ↑f (_ : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (↑f k₂) = ↑f k₁)
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case mk
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : Semiring S
f✝ : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f✝ k₂) = f✝ k₁
f : (k : ℕ) → S →+* TruncatedWittVector p k R
hf : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ (fun g =>
        { val := fun k => RingHom.comp (truncate k) g,
          property :=
            (_ :
              ∀ (k₁ k₂ : ℕ) (h : k₁ ≤ k₂),
                RingHom.comp (RingHom.comp (TruncatedWittVector.truncate h) (truncate k₂)) g =
                  RingHom.comp (truncate k₁) g) })
      ((fun f =>
          lift ↑f (_ : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (↑f k₂) = ↑f k₁))
        { val := f, property := hf }) =
    { val := f, property := hf }
[PROOFSTEP]
simp only [truncate_comp_lift]