awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
rw : y * (a * 1) = y * a
rw₁ rw₂ : y * a = y * a
⊢ y * (a * (x * y)) = y * a

Tactic:
rw [hy, mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : Ring A
inst_1 : IsSimpleRing A
x : A
hx1_1 : Membership.mem (γ := Subring A) (Subring.center A) x
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun (x_1 : A) ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
calc : a * y = x * y * a * y
calc₁ : x * y * a * y = y * x * a * y
calc₂ : y * x * a * y = y * (x * a) * y
calc₃ : y * (x * a) * y = y * (a * x) * y
calc₄ : y * (a * x) * y = y * (a * x * y)
calc₅ : y * (a * x * y) = y * (a * (x * y))
calc₆ : y * (a * (x * y)) = y * a
⊢ a * y = y * a

Tactic:
calc a * y
      _ = (x * y) * a * y := by rw [hy, one_mul]
      _ = (y * x) * a * y := by rw [hx1]
      _ = y * (x * a) * y := by rw [mul_assoc y x a]
      _ = y * (a * x) * y := by rw [hx1]
      _ = y * ((a * x) * y) := by rw [mul_assoc]
      _ = y * (a * (x * y)) := by rw [mul_assoc a x y]
      _ = y * a := by rw [hy, mul_one]

Premises used: HMul.hMul
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : CommRing A
h : IsSimpleRing A
rw : IsField.{u_1} ↥(Subring.center A)
⊢ IsField.{u_1} ↥⊤

Tactic:
rw [← Subring.center_eq_top A]

Premises used: Subring.center_eq_top
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : CommRing A
h : IsSimpleRing A
⊢ IsField.{u_1} ↥(Subring.center A)

Tactic:
IsSimpleRing.isField_center A

Premises used: Set.Mem, IsSimpleRing.isField_center
-- Module: Mathlib.RingTheory.SimpleRing.Field
Goal:
A : Type u_1
inst : CommRing A
h : IsSimpleRing A
⊢ IsField.{u_1} ↥(Subring.center A)

Tactic:
exact IsSimpleRing.isField_center A

Premises used: IsSimpleRing.isField_center
-- Module: Mathlib.RingTheory.SimpleRing.Principal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsSimpleRing R
⊢ IsSimpleOrder.{u_1} (Ideal R)

Tactic:
TwoSidedIdeal.orderIsoIdeal.symm.isSimpleOrder

Premises used: TwoSidedIdeal.orderIsoIdeal, OrderIso.symm, OrderIso.isSimpleOrder
-- Module: Mathlib.RingTheory.SimpleRing.Principal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsSimpleRing R
⊢ IsPrincipalIdealRing R

Tactic:
((isSimpleRing_iff_isField _).mp ‹_›).isPrincipalIdealRing

Premises used: IsField.isPrincipalIdealRing, isSimpleRing_iff_isField, Iff.mp
-- Module: Mathlib.RingTheory.SimpleRing.Principal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsSimpleRing R
⊢ IsDomain R

Tactic:
((isSimpleRing_iff_isField _).mp ‹_›).isDomain

Premises used: isSimpleRing_iff_isField, Iff.mp, IsField.isDomain
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
⊢ Subsingleton.{u_3 + 1} (S ⧸ HPow.hPow (β := ℕ) I 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
⊢ I = HPow.hPow (β := ℕ) I 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : AlgHom.{u_1, u_2, u_3} R A (T ⧸ J) :=
  AlgHom.comp
    (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
      S ⧸ I ^ (m + 1) →ₐ[R] (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
    (liftAdicCompletionAux (m + 1))
rw :
  Eq (α := Ideal T)
    (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1)))
      (I ^ ((m + 1) * (m + 1 + 1))))
    ⊥
⊢ J ^ (m + 1 + 1) = 0

Tactic:
rw [← Ideal.map_pow, Submodule.zero_eq_bot, ← pow_mul]

Premises used: pow_mul, Submodule.zero_eq_bot, Ideal.map_pow
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : AlgHom.{u_1, u_2, u_3} R A (T ⧸ J) :=
  AlgHom.comp
    (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
      S ⧸ I ^ (m + 1) →ₐ[R] (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
    (liftAdicCompletionAux (m + 1))
⊢ m + 1 + 1 ≤ (m + 1) * (m + 1 + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : AlgHom.{u_1, u_2, u_3} R A (T ⧸ J) :=
  AlgHom.comp
    (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
      S ⧸ I ^ (m + 1) →ₐ[R] (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
    (liftAdicCompletionAux (m + 1))
⊢ Eq (α := Ideal T)
    (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1)))
      (I ^ ((m + 1) * (m + 1 + 1))))
    ⊥

Tactic:
exact eq_bot_mono (Ideal.map_mono <| Ideal.pow_le_pow_right (by simp))
        (Ideal.map_quotient_self _)

Premises used: Ideal.map_quotient_self, Ideal.pow_le_pow_right, eq_bot_mono, Ideal.map_mono
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
zero :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := S ⧸ HPow.hPow (β := ℕ) I 0)
      (((AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (HAdd.hAdd (α := ℕ) 0 1)) :
              AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0)) :
            (a : A) → S ⧸ I ^ 0)
          x :
        S ⧸ HPow.hPow (β := ℕ) I 0)
      (((liftAdicCompletionAux I f 0 : AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0)) : (a : A) → S ⧸ I ^ 0)
          x :
        S ⧸ HPow.hPow (β := ℕ) I 0)
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0))
    (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (HAdd.hAdd (α := ℕ) 0 1)))
    (liftAdicCompletionAux I f 0)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
x : A
zero : Eq.{u_3 + 1} (α := S ⧸ HPow.hPow (β := ℕ) I 0) 0 1
⊢ Eq.{u_3 + 1} (α := S ⧸ HPow.hPow (β := ℕ) I 0)
    (((AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (HAdd.hAdd (α := ℕ) 0 1)) :
            AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0)) :
          (a : A) → S ⧸ I ^ 0)
        x :
      S ⧸ HPow.hPow (β := ℕ) I 0)
    (((liftAdicCompletionAux I f 0 : AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0)) : (a : A) → S ⧸ I ^ 0) x :
      S ⧸ HPow.hPow (β := ℕ) I 0)

Tactic:
apply eq_of_zero_eq_one

Premises used: eq_of_zero_eq_one
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
x : A
⊢ Eq.{u_3 + 1} (α := S ⧸ HPow.hPow (β := ℕ) I 0) 0 1

Tactic:
simp [subsingleton_iff_zero_eq_one]

Premises used: subsingleton_iff_zero_eq_one
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
succ :
  AlgHom.comp
      (AlgHom.comp
        (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯) :
          (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)) →ₐ[R]
            S ⧸ I ^ (m + 1))
        (Ideal.Quotient.mkₐ R
          (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1).succ) (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))))
      (lift (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
        (AlgHom.comp
          (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
            S ⧸ I ^ (m + 1) →ₐ[R]
              (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
          (liftAdicCompletionAux I f (m + 1)))) =
    liftAdicCompletionAux I f (m + 1)
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (S ⧸ I ^ (m + 1)))
    (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (m + 1 + 1)))
    (liftAdicCompletionAux I f (m + 1))

Tactic:
rw [liftAdicCompletionAux, ← DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ]

Premises used: _private.0.Algebra.FormallySmooth.liftAdicCompletionAux, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
succ :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := S ⧸ I ^ (m + 1))
      ((AlgHom.comp
              (AlgHom.comp
                (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯) :
                  (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)) →ₐ[R]
                    S ⧸ I ^ (m + 1))
                (Ideal.Quotient.mkₐ R
                  (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1).succ) (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ))
                    (I ^ (m + 1)))))
              (lift
                (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
                (AlgHom.comp
                  (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
                    S ⧸ I ^ (m + 1) →ₐ[R]
                      (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
                  (liftAdicCompletionAux I f (m + 1)))) :
            (a : A) → S ⧸ I ^ (m + 1))
          x :
        S ⧸ I ^ (m + 1))
      (((liftAdicCompletionAux I f (m + 1) : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I ^ (m + 1))) : (a : A) → S ⧸ I ^ (m + 1))
          x :
        S ⧸ I ^ (m + 1))
⊢ AlgHom.comp
      (AlgHom.comp
        (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯) :
          (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)) →ₐ[R]
            S ⧸ I ^ (m + 1))
        (Ideal.Quotient.mkₐ R
          (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1).succ) (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))))
      (lift (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
        (AlgHom.comp
          (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
            S ⧸ I ^ (m + 1) →ₐ[R]
              (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
          (liftAdicCompletionAux I f (m + 1)))) =
    liftAdicCompletionAux I f (m + 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
x : A
⊢ Eq.{u_3 + 1} (α := S ⧸ I ^ (m + 1))
    ((AlgHom.comp
            (AlgHom.comp
              (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯) :
                (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)) →ₐ[R]
                  S ⧸ I ^ (m + 1))
              (Ideal.Quotient.mkₐ R
                (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1).succ) (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ))
                  (I ^ (m + 1)))))
            (lift (Ideal.map (F := S →ₐ[R] S ⧸ I ^ (m + 1 + 1)) (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1)))
              ⋯
              (AlgHom.comp
                (↑(AlgEquiv.symm (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)) :
                  S ⧸ I ^ (m + 1) →ₐ[R]
                    (S ⧸ I ^ (m + 1).succ) ⧸ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1)))
                (liftAdicCompletionAux I f (m + 1)))) :
          (a : A) → S ⧸ I ^ (m + 1))
        x :
      S ⧸ I ^ (m + 1))
    (((liftAdicCompletionAux I f (m + 1) : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I ^ (m + 1))) : (a : A) → S ⧸ I ^ (m + 1))
        x :
      S ⧸ I ^ (m + 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m : ℕ
zero :
  Eq (α := AlgHom.{u_1, u_2, u_3} R A (S ⧸ HPow.hPow (β := ℕ) I 0))
    (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (HAdd.hAdd (α := ℕ) 0 1)))
    (liftAdicCompletionAux I f 0)
succ :
  ∀ (m : ℕ),
    Eq (α := AlgHom.{u_1, u_2, u_3} R A (S ⧸ I ^ (m + 1)))
      (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (m + 1 + 1)))
      (liftAdicCompletionAux I f (m + 1))
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (m + 1)) = liftAdicCompletionAux I f m

Tactic:
cases m with
  | zero =>
    ext
    apply eq_of_zero_eq_one
    simp [subsingleton_iff_zero_eq_one]
  | succ m =>
    rw [liftAdicCompletionAux, ← DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ]
    ext
    simp

Premises used: _private.0.Algebra.FormallySmooth.liftAdicCompletionAux, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, subsingleton_iff_zero_eq_one, eq_of_zero_eq_one
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n : ℕ
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f m) = liftAdicCompletionAux I f m

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n_1 n : ℕ
hmn : m ≤ n
ih : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
succ :
  AlgHom.comp (Ideal.Quotient.factorₐ R ⋯)
      (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (n + 1))) =
    liftAdicCompletionAux I f m
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (n + 1)) = liftAdicCompletionAux I f m

Tactic:
rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]

Premises used: AlgHom.comp_assoc, Nat.le_succ, Ideal.pow_le_pow_right, Ideal.Quotient.factorₐ_comp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n_1 n : ℕ
hmn : m ≤ n
ih : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯)
      (AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (n + 1))) =
    liftAdicCompletionAux I f m

Tactic:
simpa
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
inst_5 : FormallySmooth R A
m n : ℕ
hn : m ≤ n
base : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f m) = liftAdicCompletionAux I f m
succ :
  ∀ (n : ℕ) (hmn : m ≤ n)
    (ih : AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m),
    AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f (n + 1)) = liftAdicCompletionAux I f m
⊢ AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m

Tactic:
induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih =>
    rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
    simpa

Premises used: AlgHom.comp_assoc
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)),
    AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f

Tactic:
⟨AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f)
    (factorₐ_comp_liftAdicCompletionAux_of_le I f), ?_⟩

Premises used: _private.0.Algebra.FormallySmooth.liftAdicCompletionAux, AdicCompletion.liftAlgHom, Exists.intro, _private.0.Algebra.FormallySmooth.factorₐ_comp_liftAdicCompletionAux_of_le
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
refine :
  AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
      (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) =
    f
⊢ ∃ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)),
    AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f

Tactic:
refine ⟨AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f)
    (factorₐ_comp_liftAdicCompletionAux_of_le I f), ?_⟩
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
H :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := S ⧸ I)
      (((AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
                (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) :
              AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)) :
            (a : A) → S ⧸ I)
          x :
        S ⧸ I)
      ((f : (a : A) → S ⧸ I) x : S ⧸ I)
⊢ AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
      (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) =
    f

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
x : A
⊢ Eq.{u_3 + 1} (α := S ⧸ I)
    (((AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I))
              (AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f) ⋯) :
            AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)) :
          (a : A) → S ⧸ I)
        x :
      S ⧸ I)
    ((f : (a : A) → S ⧸ I) x : S ⧸ I)

Tactic:
simp [liftAdicCompletionAux]

Premises used: _private.0.Algebra.FormallySmooth.liftAdicCompletionAux
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
obtain :
  ∀ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S))
    (hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f),
    ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f
⊢ ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f

Tactic:
obtain ⟨g, hg⟩ := exists_adicCompletionEvalOneₐ_comp_eq f

Premises used: Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)
hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
⊢ ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f

Tactic:
⟨AlgHom.comp ((AdicCompletion.ofAlgEquiv I).symm.toAlgHom.restrictScalars R) g, ?_⟩

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgHom.restrictScalars, AdicCompletion.ofAlgEquiv, Exists.intro, AlgHom.comp
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)
hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
refine :
  AlgHom.comp (Ideal.Quotient.mkₐ R I)
      (AlgHom.comp (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S)) g) =
    f
⊢ ∃ (g : A →ₐ[R] S), AlgHom.comp (Ideal.Quotient.mkₐ R I) g = f

Tactic:
refine ⟨AlgHom.comp ((AdicCompletion.ofAlgEquiv I).symm.toAlgHom.restrictScalars R) g, ?_⟩
-- Module: Mathlib.RingTheory.Smooth.AdicCompletion
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FormallySmooth R A
I : Ideal S
inst_6 : IsAdicComplete I S
f : AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)
g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion I S)
hg : AlgHom.comp (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)) g = f
H :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := S ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I)
                (AlgHom.comp
                  (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S)) g) :
              AlgHom.{u_1, u_2, u_3} R A (S ⧸ I)) :
            (a : A) → S ⧸ I)
          x :
        S ⧸ I)
      ((f : (a : A) → S ⧸ I) x : S ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I)
      (AlgHom.comp (AlgHom.restrictScalars R (↑(AdicCompletion.ofAlgEquiv I).symm : AdicCompletion I S →ₐ[S] S)) g) =
    f

Tactic:
ext x