awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
h :
  Eq (α :=
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u) →ₗ[k]
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
    (Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))) ((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s)
⊢ ∃ (a : G), (equivHom k G : (a : G) → Aut (forget k G)) a = η

Tactic:
⟨s, toRightFDRepComp_injective (InducedCategory.hom_ext (hom_ext h.symm))⟩

Premises used: CategoryTheory.InducedCategory.hom_ext, Exists.intro, ModuleCat.hom_ext, Eq.symm, TannakaDuality.FiniteGroup.toRightFDRepComp_injective
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
h :
  Eq (α :=
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u) →ₗ[k]
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
    (Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))) ((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s)
⊢ ∃ (a : G), (equivHom k G : (a : G) → Aut (forget k G)) a = η

Tactic:
exact ⟨s, toRightFDRepComp_injective (InducedCategory.hom_ext (hom_ext h.symm))⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
x : R
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤)
        ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : (a : R) → R ⧸ I ^ n • ⊤) x) :
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) : (a : R) → R ⧸ I ^ m • ⊤) x :
      R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) 1) 1

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
x : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤
y : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤
⊢ (transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) (x * y) =
    HMul.hMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (β :=
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
      ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) x : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
      ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) y : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)

Tactic:
Quotient.inductionOn₂' x y (fun _ _ ↦ rfl)

Premises used: Quotient.inductionOn₂'
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n a : ℕ
hmn : m ≤ n
x : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤
⊢ (transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) (x ^ a) =
    HPow.hPow (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
      ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) x : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
      a

Tactic:
Quotient.inductionOn' x (fun _ ↦ rfl)

Premises used: Quotient.inductionOn'
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
m n : ℕ
h : m ≤ n
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((transitionMap I R h : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) (1 n)) (1 m)

Tactic:
simp [transitionMap_map_one I]

Premises used: AdicCompletion.transitionMap_map_one
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x y : (n : ℕ) → R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤
hx : Membership.mem (γ := Submodule R ((n : ℕ) → R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤)) (submodule I R) x
hy : Membership.mem (γ := Submodule R ((n : ℕ) → R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤)) (submodule I R) y
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) ((x * y) n) = (x * y) m

Tactic:
simp [hx hmn, hy hmn, transitionMap_map_mul I hmn]

Premises used: AdicCompletion.transitionMap_map_mul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x y : AdicCompletion I R
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤)
      (((↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) * (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤)) n) =
    ((↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) * (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤)) m

Tactic:
simp [x.property, y.property, transitionMap_map_mul I hmn]

Premises used: AdicCompletion.transitionMap_map_mul, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n),
    Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
      ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤) (1 n)) (1 m)

Tactic:
simp [transitionMap_map_one I]

Premises used: AdicCompletion.transitionMap_map_one
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x : AdicCompletion I R
n m n_1 : ℕ
hmn : m ≤ n_1
⊢ (transitionMap I R hmn : (a : R ⧸ I ^ n_1 • ⊤) → R ⧸ I ^ m • ⊤) (((↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) ^ n) n_1) =
    ((↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) ^ n) m

Tactic:
simp [x.property, transitionMap_map_pow I hmn]

Premises used: AdicCompletion.transitionMap_map_pow, Subtype.property
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Algebra S R
r : S
m n : ℕ
hmn : m ≤ n
simp :
  Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((factor ⋯ : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤)
        ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : (a : R) → R ⧸ I ^ n • ⊤)
          ((algebraMap S R : (a : S) → R) r)) :
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) : (a : R) → R ⧸ I ^ m • ⊤)
        ((algebraMap S R : (a : S) → R) r) :
      R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((transitionMap I R hmn : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤)
        ((algebraMap S ((n : ℕ) → R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : (a : S) → (n : ℕ) → R ⧸ I ^ n • ⊤) r n) :
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((algebraMap S ((n : ℕ) → R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : (a : S) → (n : ℕ) → R ⧸ I ^ n • ⊤) r m :
      R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)

Tactic:
simp only [Pi.algebraMap_apply,
        IsScalarTower.algebraMap_apply S R (R ⧸ (I ^ _ • ⊤ : Ideal R)),
        Ideal.Quotient.algebraMap_eq, mapQ_eq_factor]

Premises used: Pi.algebraMap_apply, Ideal.Quotient.algebraMap_eq, Submodule.mapQ_eq_factor, HasQuotient.Quotient, HPow.hPow, HSMul.hSMul, Top.top, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Algebra S R
r : S
m n : ℕ
hmn : m ≤ n
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((factor ⋯ : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ m • ⊤)
        ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : (a : R) → R ⧸ I ^ n • ⊤)
          ((algebraMap S R : (a : S) → R) r)) :
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) : (a : R) → R ⧸ I ^ m • ⊤)
        ((algebraMap S R : (a : S) → R) r) :
      R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : Algebra S R
s : S
⊢ Eq.{u_1 + 1} (α := AdicCompletion I R)
    ((algebraMap S (AdicCompletion I R) : (a : S) → AdicCompletion I R) s : AdicCompletion I R)
    ((of I R : (a : R) → AdicCompletion I R) ((algebraMap S R : (a : S) → R) s) : AdicCompletion I R)

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) ((↑1 : (n : ℕ) → R ⧸ I ^ n • ⊤) n) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x y : AdicCompletion I R
⊢ (↑(x * y) : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n * (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
n : ℕ
h : ∀ (x : R), x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n
⊢ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
n : ℕ
x : R
⊢ x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : AdicCompletion I R
h : I ^ n ≤ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤
⊢ Eq (α := R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤)
    ((Ideal.Quotient.factor h : (a : R ⧸ I ^ n) → R ⧸ I ^ n • ⊤)
        ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x) :
      R ⧸ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤)
    ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤) x : R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)

Tactic:
simp [evalₐ]

Premises used: AdicCompletion.evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : AdicCompletion I R
h : HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ≤ I ^ n
⊢ Eq (α := R ⧸ I ^ n)
    ((factor h : (a : R ⧸ I ^ n • ⊤) → R ⧸ I ^ n) ((eval I R n : (a : AdicCompletion I R) → R ⧸ I ^ n • ⊤) x) :
      R ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)

Tactic:
simp [evalₐ]

Premises used: AdicCompletion.evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R
⊢ Eq (α := R ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) ((of I R : (a : R) → AdicCompletion I R) x) : R ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : R) → R ⧸ I ^ n) x : R ⧸ I ^ n)

Tactic:
simp [evalₐ]

Premises used: AdicCompletion.evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
simp :
  Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n)
    (Function.comp (β := R ⧸ I ^ n * ⊤) (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)
      (⇑(AlgHom.ofLinearMap (eval I R n) ⋯ ⋯) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤))
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n) (⇑(evalₐ I n) : (a : AdicCompletion I R) → R ⧸ I ^ n)

Tactic:
simp only [evalₐ, smul_eq_mul, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ,
    AlgHom.coe_comp]

Premises used: Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, AdicCompletion.evalₐ, AlgHom.coe_comp, smul_eq_mul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
hg :
  Function.Surjective (α := R ⧸ I ^ n * ⊤) (β := R ⧸ I ^ n)
    (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)
hf :
  Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n * ⊤)
    (⇑(AlgHom.ofLinearMap (eval I R n) ⋯ ⋯) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤)
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n)
    (Function.comp (β := R ⧸ I ^ n * ⊤) (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)
      (⇑(AlgHom.ofLinearMap (eval I R n) ⋯ ⋯) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤))

Tactic:
apply Function.Surjective.comp

Premises used: Function.Surjective.comp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective (α := R ⧸ I ^ n * ⊤) (β := R ⧸ I ^ n)
    (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)

Tactic:
factor_surjective Ideal.mul_le_right

Premises used: Submodule.Quotient.mk, Submodule.factor_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective (α := R ⧸ I ^ n * ⊤) (β := R ⧸ I ^ n)
    (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)

Tactic:
exact factor_surjective Ideal.mul_le_right

Premises used: Submodule.factor_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n * ⊤)
    (⇑(AlgHom.ofLinearMap (eval I R n) ⋯ ⋯) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤)

Tactic:
eval_surjective I R n

Premises used: Set.Mem, AdicCompletion.eval_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n * ⊤)
    (⇑(AlgHom.ofLinearMap (eval I R n) ⋯ ⋯) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤)

Tactic:
exact eval_surjective I R n

Premises used: AdicCompletion.eval_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : AdicCauchySequence I R
⊢ Eq (α := R ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n)
        ((mk I R : (a : AdicCauchySequence I R) → AdicCompletion I R) x) :
      R ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : R) → R ⧸ I ^ n) ((↑x : ℕ → R) n) : R ⧸ I ^ n)

Tactic:
simp [evalₐ]

Premises used: AdicCompletion.evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
h : ∀ (n : ℕ), (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n
⊢ x = y

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
n : ℕ
h : ∀ (x : R), x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n
⊢ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x_1 y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x_1 : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
n : ℕ
x : R
⊢ x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
n : ℕ
⊢ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n

Tactic:
have h : (I ^ n • ⊤ : Ideal R) = I ^ n := by ext x; simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
n : ℕ
h : HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n
⊢ (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n

Tactic:
(Ideal.quotientEquivAlgOfEq R h).injective (H n)

Premises used: Ideal.quotientEquivAlgOfEq, Set.Mem, AlgEquiv.injective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x y : AdicCompletion I R
H :
  ∀ (n : ℕ),
    Eq (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) x : R ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) y : R ⧸ I ^ n)
n : ℕ
h : HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n
⊢ (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n

Tactic:
exact (Ideal.quotientEquivAlgOfEq R h).injective (H n)

Premises used: Ideal.quotientEquivAlgOfEq, AlgEquiv.injective
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ HPow.hPow (β := ℕ) I 1 ≤ I

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : R
⊢ Eq (α := R ⧸ I) ((evalOneₐ I : (a : AdicCompletion I R) → R ⧸ I) ((of I R : (a : R) → AdicCompletion I R) x) : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x : AdicCompletion I R
⊢ HPow.hPow (β := ℕ) I 1 ≤ I

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : AdicCompletion I R
⊢ Eq (α := R ⧸ I)
    ((Ideal.Quotient.factor ⋯ : (a : R ⧸ I ^ 1) → R ⧸ I) ((evalₐ I 1 : (a : AdicCompletion I R) → R ⧸ I ^ 1) x) : R ⧸ I)
    ((evalOneₐ I : (a : AdicCompletion I R) → R ⧸ I) x : R ⧸ I)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, npowRec, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ HPow.hPow (β := ℕ) I 1 ≤ I

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I)
    (Function.comp (β := R ⧸ HPow.hPow (β := ℕ) I 1) (⇑(Ideal.Quotient.factorₐ R ⋯) : (a : R ⧸ I ^ 1) → R ⧸ I)
      (⇑(evalₐ I 1) : (a : AdicCompletion I R) → R ⧸ I ^ 1))

Tactic:
exact (Ideal.Quotient.factor_surjective (show I ^ 1 ≤ I by simp)).comp
    (AdicCompletion.surjective_evalₐ I 1)

Premises used: Ideal.Quotient.factor_surjective, AdicCompletion.surjective_evalₐ, Function.Surjective.comp, OfNat.ofNat
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
m n : ℕ
h : m ≤ n
⊢ SModEq.{u_1, u_1} (R := R) (M := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (1 m) (1 n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x y : ℕ → R
hx : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) x
hy : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) y
m n : ℕ
hmn : m ≤ n
simp : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (x m * y m) (x n * y n)
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) ((x * y) m) ((x * y) n)

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x y : ℕ → R
hx : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) x
hy : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) y
m n : ℕ
hmn : m ≤ n
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (x m * y m) (x n * y n)

Tactic:
SModEq.mul (hx hmn) (hy hmn)

Premises used: SModEq.mul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x y : ℕ → R
hx : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) x
hy : Membership.mem (γ := Submodule R (ℕ → R)) (submodule I R : Submodule R (ℕ → R)) y
m n : ℕ
hmn : m ≤ n
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (x m * y m) (x n * y n)

Tactic:
exact SModEq.mul (hx hmn) (hy hmn)

Premises used: SModEq.mul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((↑1 : ℕ → R) n) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
f g : AdicCauchySequence I R
⊢ (↑(f * g) : ℕ → R) n = (↑f : ℕ → R) n * (↑g : ℕ → R) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : AdicCauchySequence I R
⊢ Eq (α := R ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n)
        ((mkₐ I : (a : AdicCauchySequence I R) → AdicCompletion I R) x) :
      R ⧸ I ^ n)
    ((Ideal.Quotient.mk (I ^ n) : (a : R) → R ⧸ I ^ n) ((↑x : ℕ → R) n) : R ⧸ I ^ n)

Tactic:
simp [mkₐ]

Premises used: AdicCompletion.mkₐ
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤

Tactic:
have h : I ^ m = I ^ m • ⊤ := by simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤
rw :
  Eq (α := R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) n) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((↑r : ℕ → R) m) : R ⧸ HSMul.hSMul (β := Ideal R) (I ^ m) ⊤)
⊢ Eq (α := R ⧸ I ^ m) ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
    ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) m) : R ⧸ I ^ m)

Tactic:
rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]

Premises used: Ideal.Quotient.mk_eq_mk