awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : AlgHom.{u, v, u_1} R A (B ⧸ I)
e :
  AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)) g' =
    (↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g
h₃ :
  ∀ (g' : A →ₐ[R] B)
    (e :
      AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
          (AlgHom.comp (Ideal.Quotient.mkₐ R I) g') =
        (↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g),
    ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g

Tactic:
obtain ⟨g', rfl⟩ := h₁ g'

Premises used: rfl
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) g') =
    (↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g
⊢ (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      ((↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g)

Tactic:
replace e := congr_arg this.toAlgHom.comp e
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      ((↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g)
rw : g
| (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
    ((↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g)

Tactic:
rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]

Premises used: AlgHom.comp_assoc, AlgHom.id_comp, AlgEquiv.comp_symm
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      ((↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g)
⊢ (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    g

Tactic:
conv_rhs at e =>
      rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]

Premises used: AlgHom.comp_assoc, AlgHom.id_comp, AlgEquiv.comp_symm
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    g
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g

Tactic:
⟨g', e⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    g
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g

Tactic:
exact ⟨g', e⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : AlgHom.{u, v, u_1} R A (B ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (lift I hI g) = g

Tactic:
(FormallySmooth.exists_lift I hI g).choose_spec

Premises used: Exists.choose_spec, Algebra.FormallySmooth.exists_lift, Algebra.FormallySmooth.lift
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : AlgHom.{u, v, u_1} R A (B ⧸ I)
x : A
⊢ Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((lift I hI g : (a : A) → B) x) : B ⧸ I)
    ((g : (a : A) → B ⧸ I) x : B ⧸ I)

Tactic:
AlgHom.congr_fun (FormallySmooth.comp_lift I hI g :) x

Premises used: Submodule.Quotient.mk, Algebra.FormallySmooth.comp_lift, AlgHom.congr_fun
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
a :
  Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B) : C)
    ((f : (a : A) → C) x : C)

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective

Premises used: AlgEquiv.symm, AlgEquiv.injective, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
rw :
  ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
      ((lift (RingHom.ker g) hg'
            ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
          (a : A) → B)
        x) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
| (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))

Tactic:
rw [← AlgEquiv.coe_algHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']

Premises used: AlgHom.comp_apply, Algebra.FormallySmooth.mk_lift, AlgEquiv.coe_algHom
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
a :
  Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
        ((lift (RingHom.ker g) hg'
              ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
            (a : A) → B)
          x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))

Tactic:
conv_rhs => rw [← AlgEquiv.coe_algHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']

Premises used: AlgHom.comp_apply, Algebra.FormallySmooth.mk_lift, AlgEquiv.coe_algHom
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
a :
  Eq.{u_4 + 1} (α := C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
            ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
            ((lift (RingHom.ker g) hg'
                  ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
                (a : A) → B)
              x) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
        ((lift (RingHom.ker g) hg'
              ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
            (a : A) → B)
          x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective

Premises used: AlgEquiv.injective, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
a :
  Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B) : C)
    ((RingHom.kerLift (↑g : B →+* C) : (a : B ⧸ RingHom.ker (↑g : B →+* C)) → C)
        ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
            ((lift (RingHom.ker g) hg'
                  ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
                (a : A) → B)
              x) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
⊢ Eq.{u_4 + 1} (α := C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
            ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
            ((lift (RingHom.ker g) hg'
                  ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
                (a : A) → B)
              x) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)

Tactic:
rw [AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_apply]

Premises used: AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_apply
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B) : C)
    ((RingHom.kerLift (↑g : B →+* C) : (a : B ⧸ RingHom.ker (↑g : B →+* C)) → C)
        ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
            ((lift (RingHom.ker g) hg'
                  ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
                (a : A) → B)
              x) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)

Tactic:
simp only [liftOfSurjective, ← RingHom.ker_coe_toRingHom g, RingHom.kerLift_mk, RingHom.coe_coe]

Premises used: RingHom.coe_coe, RingHom.ker_coe_toRingHom, Algebra.FormallySmooth.liftOfSurjective, RingHom.kerLift_mk
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker (F := B →+* C) (↑g : B →+* C))
⊢ g.comp (liftOfSurjective f g hg hg') = f

Tactic:
AlgHom.ext (FormallySmooth.liftOfSurjective_apply f g hg hg')

Premises used: AlgHom.ext, Algebra.FormallySmooth.liftOfSurjective_apply
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C_1
inst_6 : Algebra R C_1
inst_7 : CommRing P
inst_8 : Algebra R P
C : Type u_4
inst_9 : CommRing C
inst_10 : Algebra R C
inst_11 : EssFiniteType R A
inst_12 : FormallySmooth R A
⊢ Module.FinitePresentation A Ω[A⁄R]

Tactic:
Module.finitePresentation_of_projective A Ω[A⁄R]

Premises used: KaehlerDifferential, Module.finitePresentation_of_projective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
rw : HPow.hPow (β := ℕ) P₂.ker.cotangentIdeal 2 = ⊥
⊢ HPow.hPow (β := ℕ) P₂.infinitesimal.ker 2 = ⊥

Tactic:
rw [ker_infinitesimal]

Premises used: Algebra.Extension.ker_infinitesimal
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
⊢ HPow.hPow (β := ℕ) P₂.ker.cotangentIdeal 2 = ⊥

Tactic:
Ideal.cotangentIdeal_square _

Premises used: Set.Mem, npowRec, Ideal.cotangentIdeal_square
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
⊢ HPow.hPow (β := ℕ) P₂.ker.cotangentIdeal 2 = ⊥

Tactic:
exact Ideal.cotangentIdeal_square _

Premises used: Ideal.cotangentIdeal_square