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

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
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

Tactic:
have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
  simp [RingHom.mem_ker]

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
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

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:
show Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _

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 (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)

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 (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) = 1

Tactic:
rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
  Ideal.Quotient.eq_zero_iff_mem]

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
⊢ Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2

Proof state:
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

Tactic:
simp [pow_two, sub_mul, mul_sub, ← Pi.single_mul]

Result:
no goals