Theorem: DividedPowerAlgebra.ext_iff (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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 [DFunLike.ext'_iff]
  apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
  dsimp only
  rw [← AlgHom.coe_comp, ← AlgHom.coe_comp, ← DFunLike.ext'_iff]
  exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
State after:
no goals

State before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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

State before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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
Tactic:
rw [DFunLike.ext'_iff]
State after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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

State before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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
Tactic:
apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
State after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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)
⊢ (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑f = (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑g

State before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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)
⊢ (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑f = (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑g
Tactic:
dsimp only
State after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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 ∘ ⇑(mkAlgHom R (Rel R M)) = ⇑g ∘ ⇑(mkAlgHom R (Rel R M))

State before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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 ∘ ⇑(mkAlgHom R (Rel R M)) = ⇑g ∘ ⇑(mkAlgHom R (Rel R M))
Tactic:
rw [← AlgHom.coe_comp, ← AlgHom.coe_comp, ← DFunLike.ext'_iff]
State after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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.comp (mkAlgHom R (Rel R M)) = g.comp (mkAlgHom R (Rel R M))

State before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring 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.comp (mkAlgHom R (Rel R M)) = g.comp (mkAlgHom R (Rel R M))
Tactic:
exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
State after:
no goals