Theorem: DividedPowerAlgebra.lift'_eq_dp_lift (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
have hφ : ∀ m, ((ι S N).restrictScalars R).comp f m ∈ augIdeal S N := by
  intro m
  simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply, ι_mem_augIdeal S N (f m)]
State after:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∃ (hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N),
    LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
use hφ
State after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ

State before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ LinearMap.lift R S f = lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ
Tactic:
apply DividedPowerAlgebra.ext
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∀ (n : ℕ) (m : M), (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
⊢ ∀ (n : ℕ) (m : M), (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Tactic:
intro n m
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (lift (dividedPowers' S N) (↑R (ι S N) ∘ₗ f) hφ) (dp R n m)
Tactic:
simp only [liftAlgHom_apply_dp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply]
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (dividedPowers' S N).dpow n ((ι S N) (f m))

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ (LinearMap.lift R S f) (dp R n m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Tactic:
simp only [LinearMap.liftAlgHom_dp]
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n ((ι S N) (f m))

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n ((ι S N) (f m))
Tactic:
simp only [ι, LinearMap.coe_mk, AddHom.coe_mk]
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n (dp S 1 (f m))

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = (dividedPowers' S N).dpow n (dp S 1 (f m))
Tactic:
rw [dp_comp _ _ _ _ Nat.one_ne_zero]
State after:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = ↑(mchoose n 1) * dp S (n * 1) (f m)

State before:
case h.h
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hφ : ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
n : ℕ
m : M
⊢ dp S n (f m) = ↑(mchoose n 1) * dp S (n * 1) (f m)
Tactic:
simp only [mchoose_one', Nat.cast_one, mul_one, one_mul]
State after:
no goals

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
⊢ ∀ (m : M), (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
Tactic:
intro m
State after:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
m : M
⊢ (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type v
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
S : Type w
inst✝⁶ : CommRing S
inst✝⁵ : DecidableEq S
inst✝⁴ : Algebra R S
N : Type w
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
m : M
⊢ (↑R (ι S N) ∘ₗ f) m ∈ augIdeal S N
Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, ι_mem_augIdeal S N (f m)]
State after:
no goals