Theorem: DividedPowerAlgebra.roby_prop_8 (DividedPowers/DPAlgebra/Dpow.lean)

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

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