awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
R : Type u_1
inst : CommRing R
A : Type u
B : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra A B
n : ℕ
inst_5 : IsStandardSmoothOfRelativeDimension n A B
ι σ : Type
w : Finite σ
w_1 : Finite ι
P : SubmersivePresentation A B ι σ
hP : P.dimension = n
A₀ : Subalgebra R A := adjoin R P.coeffs
this : P.HasCoeffs ↥A₀
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
exact ⟨A₀, (P.ModelOfHasCoeffs A₀:), inferInstance, inferInstance,
    ⟨P.finite_coeffs.toFinset, by simp [A₀]⟩, ⟨_, _, _, inferInstance,
      P.ofHasCoeffs A₀, hP⟩, ⟨(P.tensorModelOfHasCoeffsEquiv A₀).symm⟩⟩
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
R : Type u_1
inst : CommRing R
A : Type u
B : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : Etale A B
simp :
  IsStandardSmoothOfRelativeDimension 0 A B →
    ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
      A₀.FG ∧ IsStandardSmoothOfRelativeDimension 0 (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
simp only [Etale.iff_isStandardSmoothOfRelativeDimension_zero] at *

Premises used: Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
R : Type u_1
inst : CommRing R
A : Type u
B : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : IsStandardSmoothOfRelativeDimension 0 A B
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension 0 (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg ..

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
R : Type u_1
inst : CommRing R
A : Type u
B : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra A B
inst_5 : IsStandardSmoothOfRelativeDimension 0 A B
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension 0 (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
exact IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg ..

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  A i →ₐ[R]
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ FormallySmooth.{u_1, u_3} R (A i)

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

Premises used: Pi.evalAlgHom, Algebra.FormallySmooth.of_split
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  Eq (α :=
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((AlgHom.toLinearMap
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
          LinearMap.single R A i :
        (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      1)
    1
g₁ :
  ∀ (x y : A i),
    (AlgHom.toLinearMap
              (Ideal.Quotient.mkₐ R
                (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                  (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
            LinearMap.single R A i :
          (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
        (x * y) =
      HMul.hMul (α :=
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
        (β :=
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
        ((AlgHom.toLinearMap
                  (Ideal.Quotient.mkₐ R
                    (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
                LinearMap.single R A i :
              (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
            x :
          ((i : I) → A i) ⧸
            HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
        ((AlgHom.toLinearMap
                  (Ideal.Quotient.mkₐ R
                    (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
                LinearMap.single R A i :
              (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
            y :
          ((i : I) → A i) ⧸
            HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
⊢ A i →ₐ[R]
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2

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

Premises used: AlgHom.toLinearMap, AlgHom.ofLinearMap, LinearMap.comp, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  Eq (α :=
    ((j : I) → A j) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((Ideal.Quotient.mk
            (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
          (a : (j : I) → A j) → ((j : I) → A j) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
        (Pi.single (M := A) i 1) :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    (1 :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
⊢ Eq (α :=
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((AlgHom.toLinearMap
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
          LinearMap.single R A i :
        (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      1)
    1

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

Premises used: Ideal.Quotient.mk, Pi.single, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 ∈
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
⊢ Eq (α :=
    ((j : I) → A j) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((Ideal.Quotient.mk
            (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
          (a : (j : I) → A j) → ((j : I) → A j) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
        (Pi.single (M := A) i 1) :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    (1 :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)

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

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.mk, RingHom.map_one, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)

Tactic:
simp [RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)

Tactic:
have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
        simp [RingHom.mem_ker]
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
this :
  Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)
⊢ -HPow.hPow (β := ℕ) (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1) 2 ∈
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2

Tactic:
neg_mem (Ideal.pow_mem_pow this 2)

Premises used: Ideal.pow_mem_pow, OfNat.ofNat, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
this :
  Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)
h :
  HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 =
    -HPow.hPow (β := ℕ) (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1) 2
⊢ HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 ∈
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2

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

Premises used: Ideal.pow_mem_pow, OfNat.ofNat, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
this :
  Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)
⊢ HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 =
    -HPow.hPow (β := ℕ) (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1) 2

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

Premises used: pow_two, mul_sub, sub_mul, Pi.single_mul
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
x y : A i
⊢ (Ideal.Quotient.mk
          (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
        (a : (i : I) → A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      (((LinearMap.single R A i : A i →ₗ[R] (i : I) → A i) : (a : A i) → (i : I) → A i) (x * y)) =
    HMul.hMul (α :=
      ((i : I) → A i) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      (β :=
      ((i : I) → A i) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      ((Ideal.Quotient.mk
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
            (a : (i : I) → A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
          (((LinearMap.single R A i : A i →ₗ[R] (i : I) → A i) : (a : A i) → (i : I) → A i) x) :
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      ((Ideal.Quotient.mk
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
            (a : (i : I) → A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
          (((LinearMap.single R A i : A i →ₗ[R] (i : I) → A i) : (a : A i) → (i : I) → A i) y) :
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)

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

Premises used: map_mul, LinearMap.coe_single, AlgHom.toRingHom_eq_coe, Pi.single_mul
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
x : A i
h : Pi.single (M := A) i x i = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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

Premises used: Pi.single
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ Pi.single (M := A) i x i = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : Finite I
inst_4 : ∀ (i : I), FormallySmooth.{u_1, u_3} R (A i)
⊢ FormallySmooth R ((i : I) → A i)

Tactic:
(pi_iff _).mpr ‹_›

Premises used: Iff.mpr, Algebra.FormallySmooth.pi_iff
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R' S'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
surjRS : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
eqmap :
  Eq (α := Ideal S) (RingHom.ker (F := S →+* S') (algebraMap S S'))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker (F := R →+* R') (algebraMap R R')))
rw :
  Eq (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) (RingHom.ker (F := S →+* S') (algebraMap S S')))
    (RingHom.ker (F := R →+* R') (algebraMap R R') ⊔ RingHom.ker (F := R →+* S) (algebraMap R S))
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') (RingHom.ker (F := R' →+* S') (algebraMap R' S')))
    (RingHom.ker (F := R →+* R') (algebraMap R R') ⊔ RingHom.ker (F := R →+* S) (algebraMap R S))

Tactic:
rw [RingHom.comap_ker, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ S,
      ← RingHom.comap_ker]

Premises used: RingHom.comap_ker, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R' S'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
surjRS : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
eqmap :
  Eq (α := Ideal S) (RingHom.ker (F := S →+* S') (algebraMap S S'))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker (F := R →+* R') (algebraMap R R')))
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) (RingHom.ker (F := S →+* S') (algebraMap S S')))
    (RingHom.ker (F := R →+* R') (algebraMap R R') ⊔ RingHom.ker (F := R →+* S) (algebraMap R S))

Tactic:
simp [eqmap, Ideal.comap_map_of_surjective' _ surjRS]

Premises used: Ideal.comap_map_of_surjective'
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : HPow.hPow (β := ℕ) I 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
rw :
  ∀ (sq : I * I = ⊥) (f : J.Cotangent →ₗ[R] J.Cotangent)
    (le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))),
    Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
rw [pow_two] at sq

Premises used: pow_two
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
mem_mul_mem :
  ∀ (w : ↥J) (hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J))
    (eqz :
      Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
        ((f : (a : J.Cotangent) → J.Cotangent)
            ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
          J.Cotangent)),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)

Tactic:
rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩

Premises used: Submodule.mem_map, LinearMap.mem_range_self, Subtype.mk, Iff.mp, Ideal.toCotangent, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
⊢ HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) ∈ I * (I * J)

Tactic:
have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) ∈ I * (I * J)
⊢ HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0

Tactic:
simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot

Premises used: Submodule.mem_bot, mul_assoc, Submodule.bot_mul
-- Module: Mathlib.RingTheory.Smooth.Quotient
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
⊢ y • w = 0

Tactic:
have eq0 : y • w = 0 := SetCoe.ext mem_bot