awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
simp :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk
        ((LinearEquiv.symm (ofLinearEquiv I N) : (a : AdicCompletion I N) → N)
          ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((lift I f ⋯ : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
simp only [lift, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]

Premises used: LinearMap.coe_comp, IsAdicComplete.lift, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
rw :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((AdicCompletion.eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤)
        ((of I N : (a : N) → AdicCompletion I N)
          ((LinearEquiv.symm (ofLinearEquiv I N) : (a : AdicCompletion I N) → N)
            ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N))) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk
        ((LinearEquiv.symm (ofLinearEquiv I N) : (a : AdicCompletion I N) → N)
          ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
rw [← mkQ_apply, ← eval_of]

Premises used: Submodule.mkQ_apply, AdicCompletion.eval_of
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((AdicCompletion.eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤)
        ((of I N : (a : N) → AdicCompletion I N)
          ((LinearEquiv.symm (ofLinearEquiv I N) : (a : AdicCompletion I N) → N)
            ((AdicCompletion.lift I f ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N))) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
h₁ :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ lift I f ⋯ : (a : M) → N ⧸ I ^ n • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ lift I f ⋯ = f n

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ lift I f ⋯ : (a : M) → N ⧸ I ^ n • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((f n : (a : M) → N ⧸ I ^ n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ F = f n
a :
  Eq (α := (a : M) → N) ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F)
    ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I f ⋯))
⊢ F = lift I f ⋯

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ F = f n
a :
  ∀ (n : ℕ) (m : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F m))
      (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I f ⋯) m))
⊢ Eq (α := (a : M) → N) ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F)
    ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I f ⋯))

Tactic:
apply IsHausdorff.funext I

Premises used: IsHausdorff.funext
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsAdicComplete I N
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ ∘ₗ F = f n
n : ℕ
m : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F m))
    (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I f ⋯) m))

Tactic:
simp [← hF n]
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
h :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((Submodule.factorPow I N ⋯ ∘ₗ f n : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
⊢ Submodule.factorPow I N ⋯ ∘ₗ f n = f m

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
h :
  Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((Submodule.factorPow I N ⋯ ∘ₗ f n : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((Submodule.factorPow I N ⋯ ∘ₗ f n : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)

Tactic:
symm
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((Submodule.factorPow I N ⋯ ∘ₗ f n : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)

Tactic:
Submodule.eq_factor_of_eq_factor_succ ?_ (fun n ↦ f n x) ?_ hle

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.eq_factor_of_eq_factor_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
h : Antitone.{0, u_5} (β := Submodule R N) fun (n : ℕ) ↦ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤
h₁ :
  ∀ (m : ℕ),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((fun (n : ℕ) ↦ ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)) m)
      ((Submodule.factor ⋯ : (a_1 : N ⧸ I ^ a m.succ • ⊤) → N ⧸ I ^ a m • ⊤)
        ((fun (n : ℕ) ↦ ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤))
          (m + 1)))
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
    ((Submodule.factorPow I N ⋯ ∘ₗ f n : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)

Tactic:
refine Submodule.eq_factor_of_eq_factor_succ ?_ (fun n ↦ f n x) ?_ hle

Premises used: Submodule.eq_factor_of_eq_factor_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ Antitone.{0, u_5} (β := Submodule R N) fun (n : ℕ) ↦ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤

Tactic:
fun _ _ le ↦ smul_mono_left (Ideal.pow_le_pow_right (ha.monotone le))

Premises used: StrictMono.monotone, Set.Mem, Ideal.pow_le_pow_right, Antitone, Submodule.smul_mono_left
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ Antitone.{0, u_5} (β := Submodule R N) fun (n : ℕ) ↦ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤

Tactic:
exact fun _ _ le ↦ smul_mono_left (Ideal.pow_le_pow_right (ha.monotone le))

Premises used: StrictMono.monotone, Ideal.pow_le_pow_right, Submodule.smul_mono_left
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
s : ℕ
⊢ ∀ {m : ℕ} (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)

Tactic:
simp only [LinearMap.ext_iff] at hf

Premises used: LinearMap.ext_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
m n : ℕ
hle : m ≤ n
x : M
s : ℕ
hf :
  ∀ {m : ℕ} (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) : (a_1 : M) → N ⧸ I ^ a m • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
      ((f m : (a_1 : M) → N ⧸ I ^ a m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a m) ⊤)
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a s) ⊤)
    ((fun (n : ℕ) ↦ ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)) s)
    ((Submodule.factor ⋯ : (a_1 : N ⧸ I ^ a s.succ • ⊤) → N ⧸ I ^ a s • ⊤)
      ((fun (n : ℕ) ↦ ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤))
        (s + 1)))

Tactic:
simpa using (hf x).symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
n : ℕ
⊢ extend ha f (a n) = f n

Tactic:
factorPow_comp_eq_of_factorPow_comp_succ_eq ha f hf (ha.id_le n)

Premises used: Set.Mem, IsAdicComplete.StrictMono.extend, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq, StrictMono.id_le
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
h :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
      ((Submodule.factorPow I N hle ∘ₗ extend ha f n : (a : M) → N ⧸ I ^ m • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
      ((extend ha f m : (a : M) → N ⧸ I ^ m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
⊢ Submodule.factorPow I N hle ∘ₗ extend ha f n = extend ha f m

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
    ((Submodule.factorPow I N hle ∘ₗ extend ha f n : (a : M) → N ⧸ I ^ m • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
    ((extend ha f m : (a : M) → N ⧸ I ^ m • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)

Tactic:
simp [extend, ← factorPow_comp_eq_of_factorPow_comp_succ_eq ha f hf hle]

Premises used: IsAdicComplete.StrictMono.extend, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
x : M
⊢ Eq (α := AdicCompletion I N)
    ((of I N : (a : N) → AdicCompletion I N) ((lift I ha f ⋯ : (a : M) → N) x) : AdicCompletion I N)
    ((AdicCompletion.lift I (extend ha f) ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)

Tactic:
IsAdicComplete.of_lift I (extend ha f) (factorPow_comp_extend ha f hf) x

Premises used: IsAdicComplete.of_lift, IsAdicComplete.StrictMono.extend, IsAdicComplete.StrictMono.factorPow_comp_extend
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
⊢ of I N ∘ₗ lift I ha f ⋯ = AdicCompletion.lift I (extend ha f) ⋯

Tactic:
IsAdicComplete.of_comp_lift I (extend ha f) (factorPow_comp_extend ha f hf)

Premises used: IsAdicComplete.StrictMono.extend, IsAdicComplete.of_comp_lift, IsAdicComplete.StrictMono.factorPow_comp_extend, IsAdicComplete.StrictMono.lift
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
n : ℕ
x : M
simp :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    (Submodule.Quotient.mk
        ((LinearEquiv.symm (LinearEquiv.ofBijective (of I N) ⋯) : (a : AdicCompletion I N) → N)
          ((AdicCompletion.lift I (extend ha f) ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    (Submodule.Quotient.mk ((lift I ha f ⋯ : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)

Tactic:
simp only [lift, IsAdicComplete.lift, ofLinearEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply]

Premises used: AdicCompletion.ofLinearEquiv, LinearMap.coe_comp, IsAdicComplete.lift, Function.comp_apply, LinearEquiv.coe_coe, IsAdicComplete.StrictMono.lift
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
n : ℕ
x : M
rw :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((AdicCompletion.eval I N (a n) : (a_1 : AdicCompletion I N) → N ⧸ I ^ a n • ⊤)
        ((of I N : (a : N) → AdicCompletion I N)
          ((LinearEquiv.symm (LinearEquiv.ofBijective (of I N) ⋯) : (a : AdicCompletion I N) → N)
            ((AdicCompletion.lift I (extend ha f) ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N))) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    (Submodule.Quotient.mk
        ((LinearEquiv.symm (LinearEquiv.ofBijective (of I N) ⋯) : (a : AdicCompletion I N) → N)
          ((AdicCompletion.lift I (extend ha f) ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N)) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)

Tactic:
rw [← mkQ_apply, ← eval_of]

Premises used: Submodule.mkQ_apply, AdicCompletion.eval_of
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
n : ℕ
x : M
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((AdicCompletion.eval I N (a n) : (a_1 : AdicCompletion I N) → N ⧸ I ^ a n • ⊤)
        ((of I N : (a : N) → AdicCompletion I N)
          ((LinearEquiv.symm (LinearEquiv.ofBijective (of I N) ⋯) : (a : AdicCompletion I N) → N)
            ((AdicCompletion.lift I (extend ha f) ⋯ : (a : M) → AdicCompletion I N) x : AdicCompletion I N))) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)

Tactic:
simp [extend_eq ha f hf]

Premises used: IsAdicComplete.StrictMono.extend_eq