awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
a b : AdicCauchySequence I M
n : ℕ
⊢ (↑(Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(a + b) : ℕ → M) n))
            ⋯) :
        ℕ → N)
      n =
    (↑(HAdd.hAdd (α := AdicCauchySequence I N)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n))
              ⋯)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑b : ℕ → M) n))
              ⋯)) :
        ℕ → N)
      n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
h :
  ∀ (n : ℕ),
    (↑(Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(r • a) : ℕ → M) n))
              ⋯) :
          ℕ → N)
        n =
      (↑(HSMul.hSMul (α := R) (β := AdicCauchySequence I N) ((RingHom.id R : (a : R) → R) r : R)
              (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n))
                ⋯)) :
          ℕ → N)
        n
⊢ Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(r • a) : ℕ → M) n)) ⋯ =
    HSMul.hSMul (α := R) (β := AdicCauchySequence I N) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n)) ⋯)

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
n : ℕ
⊢ (↑(Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(r • a) : ℕ → M) n))
            ⋯) :
        ℕ → N)
      n =
    (↑(HSMul.hSMul (α := R) (β := AdicCauchySequence I N) ((RingHom.id R : (a : R) → R) r : R)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n))
              ⋯)) :
        ℕ → N)
      n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_2 + 1} (α := AdicCauchySequence I M →ₗ[R] AdicCauchySequence I M) (map I LinearMap.id) LinearMap.id

Tactic:
rfl

Premises used: AdicCompletion.AdicCauchySequence.map, AdicCompletion.AdicCauchySequence, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ map I g ∘ₗ map I f = map I (g ∘ₗ f)

Tactic:
rfl

Premises used: AdicCompletion.AdicCauchySequence.map, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
a : AdicCauchySequence I M
⊢ Eq.{u_4 + 1} (α := AdicCauchySequence I P)
    ((map I g : (a : AdicCauchySequence I N) → AdicCauchySequence I P)
        ((map I f : (a : AdicCauchySequence I M) → AdicCauchySequence I N) a) :
      AdicCauchySequence I P)
    ((map I (g ∘ₗ f) : (a : AdicCauchySequence I M) → AdicCauchySequence I P) a : AdicCauchySequence I P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCauchySequence I M) (AdicCauchySequence I N)) (map I 0) 0

Tactic:
rfl

Premises used: AdicCompletion.AdicCauchySequence.map, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤)
      ((↑r : (n : ℕ) → R ⧸ I ^ n * ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) =
    HSMul.hSMul (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ((↑r : (n : ℕ) → R ⧸ I ^ n * ⊤) n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (↑(AddHom.toFun
            (toAddHom
              (lift I
                (fun (n : ℕ) ↦
                  (↑R :
                        {S : Type u_1} →
                          {M : Type u_2} →
                            {M₂ : Type u_3} →
                              [inst : Semiring R] →
                                [inst_9 : Semiring S] →
                                  [inst_10 : AddCommMonoid M] →
                                    [inst_11 : AddCommMonoid M₂] →
                                      [inst_12 : Module R M] →
                                        [inst_13 : Module R M₂] →
                                          [inst_14 : Module S M] →
                                            [inst_15 : Module S M₂] →
                                              [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (reduceModIdeal (I ^ n) f) ∘ₗ
                    eval I M n)
                ⋯))
            (r • x)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n =
    (↑(HSMul.hSMul (α := AdicCompletion I R) (β := AdicCompletion I N)
            ((RingHom.id (AdicCompletion I R) : (a : AdicCompletion I R) → AdicCompletion I R) r : AdicCompletion I R)
            (AddHom.toFun
              (toAddHom
                (lift I
                  (fun (n : ℕ) ↦
                    (↑R :
                          {S : Type u_1} →
                            {M : Type u_2} →
                              {M₂ : Type u_3} →
                                [inst : Semiring R] →
                                  [inst_9 : Semiring S] →
                                    [inst_10 : AddCommMonoid M] →
                                      [inst_11 : AddCommMonoid M₂] →
                                        [inst_12 : Module R M] →
                                          [inst_13 : Module R M₂] →
                                            [inst_14 : Module S M] →
                                              [inst_15 : Module S M₂] →
                                                [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        (reduceModIdeal (I ^ n) f) ∘ₗ
                      eval I M n)
                  ⋯))
              x)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n

Tactic:
dsimp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤)
      (HSMul.hSMul (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n)
        ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n)) =
    HSMul.hSMul (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ((↑r : (n : ℕ) → R ⧸ I ^ n * ⊤) n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h₁ :
  (reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤)
      (HSMul.hSMul (α := R ⧸ I ^ n) ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n)
        ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n)) =
    HSMul.hSMul (α := R ⧸ I ^ n) (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h₂ h₃ :
  HSMul.hSMul (α := R ⧸ I ^ n) (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) =
    HSMul.hSMul (α := R ⧸ I ^ n) (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((evalₐ I n : (a : AdicCompletion I R) → R ⧸ I ^ n) r : R ⧸ I ^ n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤)
      ((↑r : (n : ℕ) → R ⧸ I ^ n * ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) =
    HSMul.hSMul (β := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) ((↑r : (n : ℕ) → R ⧸ I ^ n * ⊤) n)
      ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
rw [val_smul_eq_evalₐ_smul, val_smul_eq_evalₐ_smul, map_smul]

Premises used: AdicCompletion.val_smul_eq_evalₐ_smul, map_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
n : ℕ
x : AdicCompletion I M
⊢ Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((↑((map I f : (a : AdicCompletion I M) → AdicCompletion I N) x) : (n : ℕ) → N ⧸ I ^ n • ⊤) n :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((reduceModIdeal (I ^ n) f : (a : M ⧸ I ^ n • ⊤) → N ⧸ I ^ n • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h :
  ∀ (a : AdicCauchySequence I M),
    f ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) =
      g ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)
h₁ : ∀ (x : AdicCompletion I M), f x = g x
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h :
  ∀ (a : AdicCauchySequence I M),
    f ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) =
      g ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)
x : AdicCompletion I M
⊢ f x = g x

Tactic:
apply induction_on I M x h

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type u_5
inst_3 : AddCommGroup T
inst_4 : Module.{u_1, u_5} (AdicCompletion I R) T
f g : LinearMap.{u_1, u_1, u_2, u_5} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) T
h :
  ∀ (a : AdicCauchySequence I M),
    Eq.{u_5 + 1} (α := T)
      ((f : (a : AdicCompletion I M) → T)
          ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M) :
        T)
      ((g : (a : AdicCompletion I M) → T)
          ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M) :
        T)
h₁ :
  ∀ (x : AdicCompletion I M),
    Eq.{u_5 + 1} (α := T) ((f : (a : AdicCompletion I M) → T) x : T) ((g : (a : AdicCompletion I M) → T) x : T)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type u_5
inst_3 : AddCommGroup T
inst_4 : Module.{u_1, u_5} (AdicCompletion I R) T
f g : LinearMap.{u_1, u_1, u_2, u_5} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) T
h :
  ∀ (a : AdicCauchySequence I M),
    Eq.{u_5 + 1} (α := T)
      ((f : (a : AdicCompletion I M) → T)
          ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M) :
        T)
      ((g : (a : AdicCompletion I M) → T)
          ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M) :
        T)
x : AdicCompletion I M
⊢ Eq.{u_5 + 1} (α := T) ((f : (a : AdicCompletion I M) → T) x : T) ((g : (a : AdicCompletion I M) → T) x : T)

Tactic:
apply induction_on I M x h

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f g : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
h₁ :
  ∀ (x : AdicCompletion I M),
    Eq.{u_3 + 1} (α := N) ((f : (a : AdicCompletion I M) → N) x : N) ((g : (a : AdicCompletion I M) → N) x : N)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f g : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
x : AdicCompletion I M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : AdicCompletion I M) → N) x : N) ((g : (a : AdicCompletion I M) → N) x : N)

Tactic:
apply induction_on I M x (fun a ↦ LinearMap.ext_iff.mp h a)

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ (a : AdicCauchySequence I M) (n : ℕ),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((↑((map I LinearMap.id : (a : AdicCompletion I M) → AdicCompletion I M)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        n)
      ((↑((LinearMap.id : (a : AdicCompletion I M) → AdicCompletion I M)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        n)
⊢ Eq.{u_2 + 1} (α :=
    LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M)
      (AdicCompletion I M))
    (map I LinearMap.id) LinearMap.id

Tactic:
ext a n
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a : AdicCauchySequence I M
n : ℕ
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((map I LinearMap.id : (a : AdicCompletion I M) → AdicCompletion I M)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      n)
    ((↑((LinearMap.id : (a : AdicCompletion I M) → AdicCompletion I M)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h :
  ∀ (a : AdicCauchySequence I M) (n : ℕ),
    Eq.{u_4 + 1} (α := P ⧸ HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤)
      ((↑((map I g ∘ₗ map I f : (a : AdicCompletion I M) → AdicCompletion I P)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → P ⧸ I ^ n • ⊤)
        n)
      ((↑((map I (g ∘ₗ f) : (a : AdicCompletion I M) → AdicCompletion I P)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → P ⧸ I ^ n • ⊤)
        n)
⊢ map I g ∘ₗ map I f = map I (g ∘ₗ f)

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
a : AdicCauchySequence I M
n : ℕ
⊢ Eq.{u_4 + 1} (α := P ⧸ HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤)
    ((↑((map I g ∘ₗ map I f : (a : AdicCompletion I M) → AdicCompletion I P)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → P ⧸ I ^ n • ⊤)
      n)
    ((↑((map I (g ∘ₗ f) : (a : AdicCompletion I M) → AdicCompletion I P)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → P ⧸ I ^ n • ⊤)
      n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
rw rw₁ :
  Eq.{u_4 + 1} (α := AdicCompletion I P)
    ((map I (g ∘ₗ f) : (a : AdicCompletion I M) → AdicCompletion I P) x : AdicCompletion I P)
    ((map I (g ∘ₗ f) : (a : AdicCompletion I M) → AdicCompletion I P) x : AdicCompletion I P)
⊢ Eq.{u_4 + 1} (α := AdicCompletion I P)
    ((map I g ∘ₗ map I f : (a : AdicCompletion I M) → AdicCompletion I P) x : AdicCompletion I P)
    ((map I (g ∘ₗ f) : (a : AdicCompletion I M) → AdicCompletion I P) x : AdicCompletion I P)

Tactic:
rw [map_comp]

Premises used: AdicCompletion.map_comp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
a : AdicCauchySequence I M
⊢ Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N)
        ((AdicCauchySequence.map I f : (a : AdicCauchySequence I M) → AdicCauchySequence I N) a) :
      AdicCompletion I N)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
h :
  ∀ (a : AdicCauchySequence I M) (n : ℕ),
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((↑((map I 0 : (a : AdicCompletion I M) → AdicCompletion I N)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n)
      ((↑(((0 :
                  LinearMap.{u_1, u_1, u_2, u_3} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
                    (AdicCompletion I M) (AdicCompletion I N)) :
                (a : AdicCompletion I M) → AdicCompletion I N)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n)
⊢ Eq (α :=
    LinearMap.{u_1, u_1, u_2, u_3} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M)
      (AdicCompletion I N))
    (map I 0) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
a : AdicCauchySequence I M
n : ℕ
⊢ Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((↑((map I 0 : (a : AdicCompletion I M) → AdicCompletion I N)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)
    ((↑(((0 :
                LinearMap.{u_1, u_1, u_2, u_3} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
                  (AdicCompletion I M) (AdicCompletion I N)) :
              (a : AdicCompletion I M) → AdicCompletion I N)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
x : M
⊢ Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) ((of I M : (a : M) → AdicCompletion I M) x) :
      AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) ((f : (a : M) → N) x) : AdicCompletion I N)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M ≃ₗ[R] N
⊢ map I (↑f : M →ₗ[R] N) ∘ₗ map I (↑f.symm : N →ₗ[R] M) = LinearMap.id

Tactic:
simp [map_comp]

Premises used: AdicCompletion.map_comp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M ≃ₗ[R] N
⊢ map I (↑f.symm : N →ₗ[R] M) ∘ₗ map I (↑f : M →ₗ[R] N) = LinearMap.id

Tactic:
simp [map_comp]

Premises used: AdicCompletion.map_comp
-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M ≃ₗ[R] N
x : AdicCompletion I M
⊢ Eq.{u_3 + 1} (α := AdicCompletion I N)
    ((congr I f : (a : AdicCompletion I M) → AdicCompletion I N) x : AdicCompletion I N)
    ((map I (↑f : M →ₗ[R] N) : (a : AdicCompletion I M) → AdicCompletion I N) x : AdicCompletion I N)

Tactic:
rfl

Premises used: rfl