-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[ext 1100]
lemma hom_ext {f g : X ⟶ 𝔸(n; S)}
    (h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S)
    (h₂ : ∀ i, f.appTop (coord S i) = g.appTop (coord S i)) : f = g

Proof state:
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])) =
    g ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))

Tactic:
show f ≫ toSpecMvPoly _ _ = g ≫ toSpecMvPoly _ _

Result:
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f ≫ toSpecMvPoly n S = g ≫ toSpecMvPoly n S

Proof state:
case a.h
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop f)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) =
    (ConcreteCategory.hom (Scheme.Hom.appTop g)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i)

Tactic:
exact h₂ i

Result:
no goals

Proof state:
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f ≫ toSpecMvPoly n S = g ≫ toSpecMvPoly n S

Tactic:
apply (toSpecMvPolyIntEquiv n).injective

Result:
case a
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S)

Proof state:
case a
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S)

Tactic:
ext i

Result:
case a.h
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) i = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S) i

Proof state:
case a.h
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (toSpecMvPolyIntEquiv n) (f ≫ toSpecMvPoly n S) i = (toSpecMvPolyIntEquiv n) (g ≫ toSpecMvPoly n S) i

Tactic:
rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]

Result:
case a.h
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop f)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i) =
    (ConcreteCategory.hom (Scheme.Hom.appTop g)) ((toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i)

Proof state:
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f = g

Tactic:
apply pullback.hom_ext h₁

Result:
n : Type v
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n])) =
    g ≫ pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))