Theorem: DividedPowerAlgebra.ext_iff (unused_files/Init_copy.lean)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
constructor
State after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g

State before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h n m
  rw [h]
State after:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g

State before:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h
  rw [FunLike.ext'_iff]
  apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
  simp only [← AlgHom.coe_comp, ← FunLike.ext'_iff]
  exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
State after:
no goals

State before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
intro h n m
State after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)

State before:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)
Tactic:
rw [h]
State after:
no goals

State before:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
intro h
State after:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f = g