awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
n : ℕ
x : R
⊢ Eq (α := S ⧸ I ^ n)
    ((factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
          ((liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x)) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp [liftRingHom, eval]

Premises used: AdicCompletion.liftRingHom, AdicCompletion.eval
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
n : ℕ
a :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := S ⧸ I ^ n)
      (((RingHom.comp (↑(evalₐ I n) : AdicCompletion I S →+* S ⧸ I ^ n) (liftRingHom I f ⋯) :
              RingHom.{u_4, u_5} R (S ⧸ I ^ n)) :
            (a : R) → S ⧸ I ^ n)
          x :
        S ⧸ I ^ n)
      ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ RingHom.comp (↑(evalₐ I n) : AdicCompletion I S →+* S ⧸ I ^ n) (liftRingHom I f ⋯) = f n

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
n : ℕ
x : R
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ n)
    (((RingHom.comp (↑(evalₐ I n) : AdicCompletion I S →+* S ⧸ I ^ n) (liftRingHom I f ⋯) :
            RingHom.{u_4, u_5} R (S ⧸ I ^ n)) :
          (a : R) → S ⧸ I ^ n)
        x :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
m n : ℕ
hle : m ≤ n
a :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := S ⧸ I ^ m)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
                ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
              RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
            (a : A) → S ⧸ I ^ m)
          x :
        S ⧸ I ^ m)
      ((((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)
⊢ Eq (α := RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
        ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
      RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    ((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m))

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
m n : ℕ
hle : m ≤ n
x : A
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
              ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)

Tactic:
congr($(hf hle) x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
m n : ℕ
hle : m ≤ n
x : A
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
              ((fun (n : ℕ) ↦ (f n).toRingHom) n : RingHom.{u_7, u_5} A (S ⧸ I ^ n)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((fun (n : ℕ) ↦ (f n).toRingHom) m : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)

Tactic:
exact congr($(hf hle) x)
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
r : R
n m n_1 : ℕ
hle : m ≤ n_1
a :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := S ⧸ I ^ m)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
                ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
              RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
            (a : A) → S ⧸ I ^ m)
          x :
        S ⧸ I ^ m)
      ((((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x :
        S ⧸ I ^ m)
⊢ Eq (α := RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
        ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
      RingHom.{u_7, u_5} A (S ⧸ I ^ m))
    ((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m))

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
r : R
n m n_1 : ℕ
hle : m ≤ n_1
x : A
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
              ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x :
      S ⧸ I ^ m)

Tactic:
congr($(hf hle) x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
r : R
n m n_1 : ℕ
hle : m ≤ n_1
x : A
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factorPow I hle : S ⧸ I ^ n_1 →+* S ⧸ I ^ m)
              ((↑(f n_1) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) : RingHom.{u_7, u_5} A (S ⧸ I ^ n_1)) :
            RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((↑(f m) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) : (a : A) → S ⧸ I ^ m) x :
      S ⧸ I ^ m)

Tactic:
exact congr($(hf hle) x)
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
r : R
n : ℕ
⊢ Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        (OneHom.toFun.{u_7, u_5} (M := A)
          ((↑(↑(liftRingHom I (fun (n : ℕ) ↦ (f n).toRingHom) ⋯) : A →* AdicCompletion I S) :
              OneHom.{u_7, u_5} A (AdicCompletion I S)) :
            OneHom.{u_7, u_5} A (AdicCompletion I S))
          ((algebraMap R A : (a : R) → A) r : A)) :
      S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        ((algebraMap R (AdicCompletion I S) : (a : R) → AdicCompletion I S) r) :
      S ⧸ I ^ n)

Tactic:
simp [evalₐ_liftRingHom _ _ <| fun hle ↦ by ext x; exact congr($(hf hle) x)]

Premises used: AdicCompletion.evalₐ_liftRingHom
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst_1 : CommRing R
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
n : ℕ
x : A
m n_1 : ℕ
hle : m ≤ n_1
a :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := S ⧸ I ^ m)
      (((RingHom.comp (Ideal.Quotient.factorPow I hle) (f n_1).toRingHom : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
            (a : A) → S ⧸ I ^ m)
          x :
        S ⧸ I ^ m)
      (((f m).toRingHom : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)
⊢ RingHom.comp (Ideal.Quotient.factorPow I hle) (f n_1).toRingHom = (f m).toRingHom

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst_1 : CommRing R
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
n : ℕ
x_1 : A
m n_1 : ℕ
hle : m ≤ n_1
x : A
⊢ Eq.{u_5 + 1} (α := S ⧸ I ^ m)
    (((RingHom.comp (Ideal.Quotient.factorPow I hle) (f n_1).toRingHom : RingHom.{u_7, u_5} A (S ⧸ I ^ m)) :
          (a : A) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    (((f m).toRingHom : (a : A) → S ⧸ I ^ m) x : S ⧸ I ^ m)

Tactic:
congr($(hf hle) x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R_2 : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R_2
inst_5 : CommRing S
I : Ideal S
f_1 : (n : ℕ) → RingHom.{u_4, u_5} R_2 (S ⧸ I ^ n)
hf_1 : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f_1 n) = f_1 m
R : Type u_6
A : Type u_7
inst_6 : CommRing R
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
x : A
⊢ HPow.hPow (β := ℕ) I 1 ≤ I

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst_1 : CommRing R
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : (n : ℕ) → AlgHom.{u_6, u_7, u_5} R A (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), AlgHom.comp (Ideal.Quotient.factorₐ R ⋯) (f n) = f m
x : A
⊢ Eq (α := S ⧸ I)
    ((evalOneₐ I : (a : AdicCompletion I S) → S ⧸ I) ((liftAlgHom I f ⋯ : (a : A) → AdicCompletion I S) x) : S ⧸ I)
    ((Ideal.Quotient.factorₐ R ⋯ : (a : S ⧸ I ^ 1) → S ⧸ I) ((f 1 : (a : A) → S ⧸ I ^ 1) x) : S ⧸ I)

Tactic:
simp [evalOneₐ]

Premises used: AdicCompletion.evalOneₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
inst_6 : IsAdicComplete I S
x x_1 : S
h :
  ∀ (n : ℕ),
    (↑(AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) (x * x_1)) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n =
      (↑(HMul.hMul (α := AdicCompletion I S)
              (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x)
              (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x_1)) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n
⊢ AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) (x * x_1) =
    HMul.hMul (α := AdicCompletion I S)
      (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x)
      (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x_1)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
inst_6 : IsAdicComplete I S
x x_1 : S
n : ℕ
⊢ (↑(AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) (x * x_1)) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n =
    (↑(HMul.hMul (α := AdicCompletion I S)
            (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x)
            (AddHom.toFun (LinearMap.toAddHom (↑(ofLinearEquiv I S) : S →ₗ[S] AdicCompletion I S)) x_1)) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
x : S
⊢ Eq (α := AdicCompletion I S) ((ofAlgEquiv I : (a : S) → AdicCompletion I S) x : AdicCompletion I S)
    ((of I S : (a : S) → AdicCompletion I S) x : AdicCompletion I S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
x : AdicCompletion I S
⊢ (of I S : (a : S) → AdicCompletion I S) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) = x

Tactic:
simp [ofAlgEquiv]

Premises used: AdicCompletion.ofAlgEquiv
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
x : S
⊢ ((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S)
      ((of I S : (a : S) → AdicCompletion I S) x : AdicCompletion I S) =
    x

Tactic:
simp [ofAlgEquiv]

Premises used: AdicCompletion.ofAlgEquiv
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
nth_rw :
  Eq (α := S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
        ((of I S : (a : S) → AdicCompletion I S) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
⊢ Eq (α := S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)

Tactic:
nth_rw 2 [← of_ofAlgEquiv_symm I x]

Premises used: AdicCompletion.of_ofAlgEquiv_symm
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ Eq (α := S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
        (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ HSMul.hSMul (β := Ideal S) (I ^ n) ⊤)
    ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
        ((of I S : (a : S) → AdicCompletion I S) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)

Tactic:
simp [-of_ofAlgEquiv_symm, eval]

Premises used: AdicCompletion.of_ofAlgEquiv_symm, AdicCompletion.eval
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
simp :
  Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    (((↑(Ideal.quotientEquivAlgOfEq S ⋯) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x) :
      S ⧸ I ^ n)
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp only [evalₐ, AlgHom.coe_comp, Function.comp_apply, AlgHom.ofLinearMap_apply]

Premises used: AlgHom.ofLinearMap_apply, AdicCompletion.evalₐ, AlgHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
rw :
  Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    (((↑(Ideal.quotientEquivAlgOfEq S ⋯) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
          (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
      S ⧸ I ^ n)
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    (((↑(Ideal.quotientEquivAlgOfEq S ⋯) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤) x) :
      S ⧸ I ^ n)

Tactic:
rw [← mk_smul_top_ofAlgEquiv_symm I n x]

Premises used: AdicCompletion.mk_smul_top_ofAlgEquiv_symm
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ Eq (α := S ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : S) → S ⧸ I ^ n) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) :
      S ⧸ I ^ n)
    (((↑(Ideal.quotientEquivAlgOfEq S ⋯) : S ⧸ I ^ n • ⊤ →ₐ[S] S ⧸ I ^ n) : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal S) (I ^ n) ⊤) : (a : S) → S ⧸ I ^ n • ⊤)
          (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x)) :
      S ⧸ I ^ n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
S : Type u_5
inst : CommRing S
I : Ideal S
inst_1 : IsAdicComplete I S
x : AdicCompletion I S
⊢ Eq (α := S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((ofAlgEquiv I).symm : (a : AdicCompletion I S) → S) x) : S ⧸ I)
    ((evalOneₐ I : (a : AdicCompletion I S) → S ⧸ I) x : S ⧸ I)

Tactic:
simp [evalOneₐ, ← mk_ofAlgEquiv_symm]

Premises used: AdicCompletion.mk_ofAlgEquiv_symm, AdicCompletion.evalOneₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
A : Type u_4
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
x : S
⊢ Eq.{u_4 + 1} (α := A)
    ((kerProj hf : (a : AdicCompletion (RingHom.ker f) S) → A)
        ((of (RingHom.ker f) S : (a : S) → AdicCompletion (RingHom.ker f) S) x : AdicCompletion (RingHom.ker f) S) :
      A)
    ((f : (a : S) → A) x : A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
A : Type u_4
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
dsimp :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
    (Function.comp (β := HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))
      (⇑(Ideal.quotientKerAlgEquivOfSurjective hf) : (a : S ⧸ RingHom.ker f) → A)
      (⇑(evalOneₐ (RingHom.ker f)) : (a : AdicCompletion (RingHom.ker f) S) → S ⧸ RingHom.ker f))
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := AdicCompletion (RingHom.ker f) S) (β := A)
    (⇑(kerProj hf) : (a : AdicCompletion (RingHom.ker f) S) → A)

Tactic:
dsimp [kerProj]

Premises used: AdicCompletion.kerProj