-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma of_mvPolynomial_int_ext {R} {f g : ℤ[n] ⟶ R} (h : ∀ i, f (.X i) = g (.X i)) : f = g

Proof state:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
⊢ f = g

Tactic:
ext x

Result:
case hf.hC.a
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ULift.{u_1, 0} ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) x = ((CommRingCat.Hom.hom g).comp C) x

case hf.hX
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : n
⊢ (CommRingCat.Hom.hom f) (X x) = (CommRingCat.Hom.hom g) (X x)

Proof state:
case hC
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C

Tactic:
exact RingHom.ext_int _ _

Result:
no goals

Proof state:
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom

Tactic:
ext1

Result:
case hC
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C

case hX
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
i✝ : n
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝) =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝)

Proof state:
case hf.hC.a
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ULift.{u_1, 0} ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) x = ((CommRingCat.Hom.hom g).comp C) x

Tactic:
obtain ⟨x⟩ := x

Result:
case hf.hC.a.up
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) { down := x } = ((CommRingCat.Hom.hom g).comp C) { down := x }

Proof state:
case hX
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
i✝ : n
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝) =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝)

Tactic:
simpa using h _

Result:
no goals

Proof state:
case hf.hX
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : n
⊢ (CommRingCat.Hom.hom f) (X x) = (CommRingCat.Hom.hom g) (X x)

Tactic:
simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (X x)

Result:
no goals

Proof state:
case hf.hC.a.up
n : Type v
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) { down := x } = ((CommRingCat.Hom.hom g).comp C) { down := x }

Tactic:
simpa [-map_intCast, -eq_intCast] using DFunLike.congr_fun this (C x)

Result:
no goals