-- Mathlib/RingTheory/Smooth/Pi.lean
theorem of_pi [FormallySmooth R (Π i, A i)] (i) :
    FormallySmooth R (A i)

Proof state:
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ FormallySmooth R (A i)

Tactic:
fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)

Result:
case g
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ A i →ₐ[R] ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

case hg
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ (Pi.evalAlgHom R A i).kerSquareLift.comp ?g = AlgHom.id R (A i)

Proof state:
case hg
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ (Pi.evalAlgHom R A i).kerSquareLift.comp
      (AlgHom.ofLinearMap
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        ⋯ ⋯) =
    AlgHom.id R (A i)

Tactic:
ext x

Result:
case hg.H
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ ((Pi.evalAlgHom R A i).kerSquareLift.comp
        (AlgHom.ofLinearMap
          ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ
            LinearMap.single R A i)
          ⋯ ⋯))
      x =
    (AlgHom.id R (A i)) x

Proof state:
case g.map_mul
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ∀ (x y : A i),
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        (x * y) =
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          x *
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          y

Tactic:
intro x y

Result:
case g.map_mul
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x y : A i
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
      (x * y) =
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) x *
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) y

Proof state:
case g
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ A i →ₐ[R] ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

Tactic:
apply AlgHom.ofLinearMap
  ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))

Result:
case g.map_one
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

case g.map_mul
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ∀ (x y : A i),
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        (x * y) =
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          x *
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          y

Proof state:
case hg.H
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ ((Pi.evalAlgHom R A i).kerSquareLift.comp
        (AlgHom.ofLinearMap
          ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ
            LinearMap.single R A i)
          ⋯ ⋯))
      x =
    (AlgHom.id R (A i)) x

Tactic:
show (Pi.single i x) i = x

Result:
case hg.H
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ Pi.single i x i = x

Proof state:
case g.map_one
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

Tactic:
show Ideal.Quotient.mk _ (Pi.single i 1) = 1

Result:
case g.map_one
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) = 1

Proof state:
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom

Tactic:
simp [RingHom.mem_ker]

Result:
no goals

Proof state:
case g.map_one
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
this : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

Tactic:
convert neg_mem (Ideal.pow_mem_pow this 2) using 1

Result:
case h.e'_5
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
this : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom
⊢ Pi.single i 1 - 1 = -(Pi.single i 1 - 1) ^ 2

Proof state:
case g.map_mul
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x y : A i
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) (x * y)) =
    (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) x) *
      (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) y)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]

Result:
no goals

Proof state:
case hg.H
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ Pi.single i x i = x

Tactic:
simp

Result:
no goals