awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u t : G
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹) ≫
      η.hom.hom.app rightFDRep)
    (η.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹))
⊢ Eq (α := k)
    ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
        ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
            (single (M := fun (a : G) ↦ k) u 1) :
          G → k) :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
have pos : u = t * s →
  Eq (α := k)
    ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
        ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
            (single (M := fun (a : G) ↦ k) u 1) :
          G → k) :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
Tactic: by_cases u = t * s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u t : G
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹) ≫
      η.hom.hom.app rightFDRep)
    (η.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹))
pos :
  u = t * s →
    Eq (α := k)
      ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
          ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
              (single (M := fun (a : G) ↦ k) u 1) :
            G → k) :
        k)
      ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) t :
        k)
⊢ Eq (α := k)
    ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
        ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
            (single (M := fun (a : G) ↦ k) u 1) :
          G → k) :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
have neg : ¬u = t * s →
  Eq (α := k)
    ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
        ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
            (single (M := fun (a : G) ↦ k) u 1) :
          G → k) :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
Tactic: by_cases u = t * s
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u t : G
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹) ≫
      η.hom.hom.app rightFDRep)
    (η.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹))
⊢ Eq (α := k)
    (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
            (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
          (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
have _ : Eq (α := k)
  (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
          (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
        (a : G → k) → G → k)
      ((basisFun k G : (a : G) → G → k) u : G → k) t :
    k)
  ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC := carrier)
              (X :=
              ObjectProperty.FullSubcategory.obj (P := isFG k)
                (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
              (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)) :
            (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
          (single (M := fun (a : G) ↦ k) u 1) :
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
          Type u))
      1 :
    k)
Tactic: calc
    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all [single_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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),
    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)
have obtain : ∀ (s : G)
  (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s),
  ∃ (s : G),
    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)
Tactic: classical
  obtain ⟨s, hs⟩ := ((evalAlgHom _ _ 1).comp (algHomOfRightFDRepComp η)).eq_piEvalAlgHom
  refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
  simp only [rightFDRep, forget_obj]
  ext t
  have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)
  calc
    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all [single_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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)
⊢ ∃ (a : G), (equivHom k G : (a : G) → Aut (forget k G)) a = η
have obtain : ∀ (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: obtain ⟨s, h⟩ := toRightFDRepComp_in_rightRegular η
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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) ⊤)
    ((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) ⊤)
have simp : Eq (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤)
  ((factor sorry : (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: simp only [Pi.algebraMap_apply,
        IsScalarTower.algebraMap_apply S R (R ⧸ (I ^ _ • ⊤ : Ideal R)),
        Ideal.Quotient.algebraMap_eq, mapQ_eq_factor]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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 : ℕ
⊢ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n
have h : ∀ (x : R), x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n) (⇑(evalₐ I n) : (a : AdicCompletion I R) → R ⧸ I ^ n)
have simp : Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n)
  (Function.comp (β := R ⧸ I ^ n * ⊤) (⇑(Ideal.Quotient.factorₐ R sorry) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)
    (⇑(AlgHom.ofLinearMap (eval I R n) sorry sorry) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤))
Tactic: simp only [evalₐ, smul_eq_mul, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ,
    AlgHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
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 * ⊤))
have hg : Function.Surjective (α := R ⧸ I ^ n * ⊤) (β := R ⧸ I ^ n)
  (⇑(Ideal.Quotient.factorₐ R sorry) : (a : R ⧸ I ^ n * ⊤) → R ⧸ I ^ n)
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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)
⊢ 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 * ⊤))
have hf : Function.Surjective (α := AdicCompletion I R) (β := R ⧸ I ^ n * ⊤)
  (⇑(AlgHom.ofLinearMap (eval I R n) sorry sorry) : (a : AdicCompletion I R) → R ⧸ I ^ n * ⊤)
Tactic: apply Function.Surjective.comp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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)
⊢ x = y
have h : ∀ (n : ℕ), (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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
have h : ∀ (x : R), x ∈ HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ ↔ x ∈ I ^ n
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (hypothesis)
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 : ℕ
⊢ (↑x : (n : ℕ) → R ⧸ I ^ n • ⊤) n = (↑y : (n : ℕ) → R ⧸ I ^ n • ⊤) n
have h : HSMul.hSMul (β := Ideal R) (I ^ n) ⊤ = I ^ n
Tactic: have h : (I ^ n • ⊤ : Ideal R) = I ^ n := by ext x; simp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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 * y) m) ((x * y) n)
have simp : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (x m * y m) (x n * y n)
Tactic: simp only [Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ 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)
have h : I ^ m = HSMul.hSMul (β := Ideal R) (I ^ m) ⊤
Tactic: have h : I ^ m = I ^ m • ⊤ := by simp
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
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) ⊤
⊢ 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)
have 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) ⊤)
Tactic: rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw : Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
rw :
  Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw₁ : HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
rw :
  Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₁ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw₂ : HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Algebra (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
rw :
  Submodule.Quotient.mk ((↑r : ℕ → R) n • (↑x : ℕ → M) n) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₁ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
rw₂ :
  HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
      ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) n) : R ⧸ I ^ m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
⊢ HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) n)
      (Submodule.Quotient.mk ((↑x : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
      (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
have rw₃ : HSMul.hSMul (α := R ⧸ I ^ m) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((Ideal.Quotient.mk (I ^ m) : (a : R) → R ⧸ I ^ m) ((↑r : ℕ → R) m) : R ⧸ I ^ m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ((↑r : ℕ → R) m)
    (Submodule.Quotient.mk ((↑x : ℕ → M) m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
Tactic: rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]