mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
⊢ ∀ (n : ℕ), ↑(a n) ≡ ↑(a (n + 1)) [SMOD I ^ n • ⊤]

Tactic:
refine fun n ↦ SModEq.symm ?_

Goal state after:
case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
n : ℕ
⊢ ↑(a (n + 1)) ≡ ↑(a n) [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
a b : AdicCauchySequence I M
n : ℕ
⊢ ↑⟨fun n ↦ f (↑(a + b) n), ⋯⟩ n = ↑(⟨fun n ↦ f (↑a n), ⋯⟩ + ⟨fun n ↦ f (↑b n), ⋯⟩) n

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
a b : AdicCauchySequence I M
n : ℕ
⊢ ↑⟨fun n ↦ f (↑(a + b) n), ⋯⟩ n = ↑(⟨fun n ↦ f (↑a n), ⋯⟩ + ⟨fun n ↦ f (↑b n), ⋯⟩) n
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
n : ℕ
⊢ ↑⟨fun n ↦ f (↑(r • a) n), ⋯⟩ n = ↑((RingHom.id R) r • ⟨fun n ↦ f (↑a n), ⋯⟩) n

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
n : ℕ
⊢ ↑⟨fun n ↦ f (↑(r • a) n), ⋯⟩ n = ↑((RingHom.id R) r • ⟨fun n ↦ f (↑a n), ⋯⟩) n
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
n : ℕ
⊢ Submodule.Quotient.mk (Eq.recOn ⋯ (↑x n)) = ↑(Eq.recOn ⋯ ((mk I (M j)) x)) n

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
n : ℕ
⊢ Submodule.Quotient.mk (Eq.recOn ⋯ (↑x n)) = ↑(Eq.recOn ⋯ ((mk I (M j)) x)) n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ y : AdicCompletion I R
H : ∀ (n : ℕ), (evalₐ I n) x✝ = (evalₐ I n) y
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ y : AdicCompletion I R
H : ∀ (n : ℕ), (evalₐ I n) x✝ = (evalₐ I n) y
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h✝ : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
h : ∃ x, ∀ (n : ℕ), x n ≡ x (n + 1) [SMOD I ^ n • ⊤] ∧ Submodule.Quotient.mk (f (x n)) = (eval I N n) y
⊢ ∃ a, (map I f) a = y

Tactic:
obtain ⟨x, hx⟩ := h
    use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
    ext n
    simp [hx n]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : M ⧸ I ^ n • ⊤
f✝ : AdicCauchySequence I R
⊢ ↑((mk I R) f✝) n • x = (evalₐ I n) ((mk I R) f✝) • x

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : M ⧸ I ^ n • ⊤
f✝ : AdicCauchySequence I R
⊢ ↑((mk I R) f✝) n • x = (evalₐ I n) ((mk I R) f✝) • x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
n : ℕ
⊢ ↑(r • 0) n = ↑0 n

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
n : ℕ
⊢ ↑(r • 0) n = ↑0 n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
x y : AdicCompletion I M
n : ℕ
⊢ ↑(r • (x + y)) n = ↑(r • x + r • y) n

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
x y : AdicCompletion I M
n : ℕ
⊢ ↑(r • (x + y)) n = ↑(r • x + r • y) n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
⊢ ↑((r + s) • x) n = ↑(r • x + s • x) n

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
⊢ ↑((r + s) • x) n = ↑(r • x + s • x) n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
n : ℕ
⊢ ↑(0 • x) n = ↑0 n

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
n : ℕ
⊢ ↑(0 • x) n = ↑0 n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n✝ : ℕ
⊢ ↑⟨fun n ↦ (factor ⋯) 1, ⋯⟩ n✝ = ↑1 n✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n✝ : ℕ
⊢ ↑⟨fun n ↦ (factor ⋯) 1, ⋯⟩ n✝ = ↑1 n✝
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
x y : R
n✝ : ℕ
⊢ ↑⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) x) * (Ideal.Quotient.factor ⋯) ((f n) y), ⋯⟩ n✝ =
    ↑(⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) x), ⋯⟩ * ⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) y), ⋯⟩) n✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
x y : R
n✝ : ℕ
⊢ ↑⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) x) * (Ideal.Quotient.factor ⋯) ((f n) y), ⋯⟩ n✝ =
    ↑(⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) x), ⋯⟩ * ⟨fun n ↦ (Ideal.Quotient.factor ⋯) ((f n) y), ⋯⟩) n✝
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n✝ : ℕ
⊢ ↑⟨fun n ↦ 0, ⋯⟩ n✝ = ↑0 n✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n✝ : ℕ
⊢ ↑⟨fun n ↦ 0, ⋯⟩ n✝ = ↑0 n✝
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
x y : R
n✝ : ℕ
⊢ ↑⟨fun n ↦ (factor ⋯) ((f n) x) + (factor ⋯) ((f n) y), ⋯⟩ n✝ =
    ↑(⟨fun n ↦ (factor ⋯) ((f n) x), ⋯⟩ + ⟨fun n ↦ (factor ⋯) ((f n) y), ⋯⟩) n✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R✝ M
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
x y : R
n✝ : ℕ
⊢ ↑⟨fun n ↦ (factor ⋯) ((f n) x) + (factor ⋯) ((f n) y), ⋯⟩ n✝ =
    ↑(⟨fun n ↦ (factor ⋯) ((f n) x), ⋯⟩ + ⟨fun n ↦ (factor ⋯) ((f n) y), ⋯⟩) n✝
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x✝ : R
⊢ ((↑(evalₐ I n)).comp (liftRingHom I f ⋯)) x✝ = (f n) x✝

Tactic:
;

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
n : ℕ
x✝ : R
⊢ ((↑(evalₐ I n)).comp (liftRingHom I f ⋯)) x✝ = (f n) x✝
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x

Tactic:
;

Goal state after:
R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : ?m.133
⊢ ((Ideal.Quotient.factorPow ?m.137 hle).comp (?m.138 n✝)) x = (?m.138 m✝) x

Tactic:
;

Goal state after:
R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : ?m.133
⊢ ((Ideal.Quotient.factorPow ?m.137 hle).comp (?m.138 n✝)) x = (?m.138 m✝) x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝⁴ : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
n : ℕ
x✝ : A
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x

Tactic:
;

Goal state after:
S : Type u_5
inst✝⁴ : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
n : ℕ
x✝ : A
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
R : Type u_4
S : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
inst✝ : IsAdicComplete I S
x✝¹ x✝ : S
n✝ : ℕ
⊢ ↑((↑(ofLinearEquiv I S)).toFun (x✝¹ * x✝)) n✝ =
    ↑((↑(ofLinearEquiv I S)).toFun x✝¹ * (↑(ofLinearEquiv I S)).toFun x✝) n✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
I✝ : Ideal R✝
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
R : Type u_4
S : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
inst✝ : IsAdicComplete I S
x✝¹ x✝ : S
n✝ : ℕ
⊢ ↑((↑(ofLinearEquiv I S)).toFun (x✝¹ * x✝)) n✝ =
    ↑((↑(ofLinearEquiv I S)).toFun x✝¹ * (↑(ofLinearEquiv I S)).toFun x✝) n✝
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_1
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
⊢ ∀ (n : ℕ), ↑(a n) ≡ ↑(a (n + 1)) [SMOD I ^ n • ⊤]

Tactic:
refine fun n ↦ SModEq.symm ?_

Goal state after:
case refine_1
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ ↑(a (n + 1)) ≡ ↑(a n) [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f (m + 1)) = liftAdicCompletionAux I f m

Tactic:
cases m with
  | zero =>
    ext
    apply eq_of_zero_eq_one
    simp [subsingleton_iff_zero_eq_one]
  | succ m =>
    rw [liftAdicCompletionAux, ← DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ]
    ext
    simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case e'_4
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
x✝¹ x✝ : σ
⊢ (⇑P.aevalDifferential ∘ ⇑(Pi.basisFun S σ)) x✝¹ x✝ = (aeval P.val) ((pderiv (P.map x✝)) (P.relation x✝¹))

Tactic:
;

Goal state after:
case e'_4
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
x✝¹ x✝ : σ
⊢ (⇑P.aevalDifferential ∘ ⇑(Pi.basisFun S σ)) x✝¹ x✝ = (aeval P.val) ((pderiv (P.map x✝)) (P.relation x✝¹))
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case e'_6
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
x✝¹ x✝ : σ
⊢ (⇑P.aevalDifferential ∘ ⇑(Pi.basisFun S σ)) x✝¹ x✝ = (aeval P.val) ((pderiv (P.map x✝)) (P.relation x✝¹))

Tactic:
;

Goal state after:
case e'_6
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
x✝¹ x✝ : σ
⊢ (⇑P.aevalDifferential ∘ ⇑(Pi.basisFun S σ)) x✝¹ x✝ = (aeval P.val) ((pderiv (P.map x✝)) (P.relation x✝¹))
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) = (rename Sum.inr) (P.jacobiMatrix i j)

Tactic:
by
  rw [jacobiMatrix_apply, jacobiMatrix_apply]
  simp only [comp_map, Sum.elim_inr]
  apply pderiv_rename Sum.inr_injective

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
i : κ
⊢ s ((v ∘ a) i) = 0

Tactic:
;

Goal state after:
case mem
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
i : κ
⊢ s ((v ∘ a) i) = 0