awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = 0
⊢ n = m

Tactic:
rw [hmn, Nat.add_zero] at this

Premises used: Nat.add_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = 0
this₁ : n = m
⊢ n - m = 0

Tactic:
rw [hmn, Nat.add_zero] at this

Premises used: Nat.add_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m
hmn : n - m = 0
zero : ∀ (g : n ≤ n) (hmn : n - n = 0), x n = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p n) (x n)
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
n : ℕ
g : n ≤ n
hmn : n - n = 0
⊢ x n = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p n) (x n)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = k + 1
⊢ n = m + k + 1

Tactic:
rw [hmn, ← add_assoc] at this

Premises used: add_assoc
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
hmn : n - m = k + 1
this₁ : n = m + k + 1
⊢ n - m = k + 1

Tactic:
rw [hmn, ← add_assoc] at this

Premises used: add_assoc
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m n : ℕ
g : m ≤ n
this : n = m + k + 1
hmn : n - m = k + 1
succ :
  ∀ (g : m ≤ m + k + 1) (hmn : m + k + 1 - m = k + 1),
    x m = (factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1))
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)

Tactic:
subst this
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
⊢ m + k = m + (m + k - m)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
succ :
  Eq (α := M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k)) → M ⧸ p m)
        ((factor ⋯ : (a : M ⧸ p (m + k).succ) → M ⧸ p (m + k)) (x (m + k + 1))) :
      M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1)) : M ⧸ p m)
succ₁ : m + k - m = k
⊢ x m = (factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1))

Tactic:
rw [ih (m.le_add_right k) (by simp), h]

Premises used: Nat.le_add_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
⊢ Eq (α := M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k)) → M ⧸ p m)
        ((factor ⋯ : (a : M ⧸ p (m + k).succ) → M ⧸ p (m + k)) (x (m + k + 1))) :
      M ⧸ p m)
    ((factor ⋯ : (a : M ⧸ p (m + k + 1)) → M ⧸ p m) (x (m + k + 1)) : M ⧸ p m)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
k : ℕ
ih :
  ∀ {m n : ℕ} (g : m ≤ n) (this : n = m + (n - m)) (hmn : n - m = k), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
m : ℕ
g : m ≤ m + k + 1
hmn : m + k + 1 - m = k + 1
⊢ m + k - m = k

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : M ⧸ p m.succ) → M ⧸ p m) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
induction : ∀ (x_1 : ℕ) (hmn : n - m = x_1), x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)
⊢ x m = (factor ⋯ : (a : M ⧸ p n) → M ⧸ p m) (x n)

Tactic:
induction hmn : n - m generalizing m n with
  | zero =>
    rw [hmn, Nat.add_zero] at this
    subst this
    simp
  | succ k ih =>
    rw [hmn, ← add_assoc] at this
    subst this
    rw [ih (m.le_add_right k) (by simp), h]
    · simp
    · lia

Premises used: add_assoc, Submodule.zero, Nat.add_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I : ℕ → Ideal R
inst_1 : ∀ (n : ℕ), (I n).IsTwoSided
hI : Antitone I
x : (n : ℕ) → R ⧸ I n
h : ∀ (m : ℕ), x m = (factor ⋯ : (a : R ⧸ I m.succ) → R ⧸ I m) (x (m + 1))
m n : ℕ
g : m ≤ n
⊢ x m = (factor ⋯ : (a : R ⧸ I n) → R ⧸ I m) (x n)

Tactic:
Submodule.eq_factor_of_eq_factor_succ hI x h g

Premises used: Submodule.Quotient.mk, Submodule.eq_factor_of_eq_factor_succ
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
h :
  ∀ (x : R ⧸ K),
    Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
        x ↔
      Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
⊢ Eq (α := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
    (map (F := R →+* R ⧸ K) (mk K) I)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x ↔
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h :
  ∀
    (h :
      Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I))
        x),
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
h₁ :
  ∀ (h : Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x),
    Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x ↔
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
h₁ :
  ∀ (r : R) (hr : r ∈ (↑I : Set R))
    (eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)),
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk J) Quotient.mk_surjective h with ⟨r, hr, eq⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))

Tactic:
simp [← factor_ker hJK, ← eq]

Premises used: Ideal.Quotient.factor_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))

Tactic:
have : x - ((mk K) r) ∈ J.map (mk K) := by
      simp [← factor_ker hJK, ← eq]
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
this :
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))
h₁ :
  ∀ (s : R) (hs : s ∈ (↑J : Set R))
    (eq' : (mk K : (a : R) → R ⧸ K) s = HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K)),
    Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective this with ⟨s, hs, eq'⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
this :
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))
s : R
hs : s ∈ (↑J : Set R)
eq' : (mk K : (a : R) → R ⧸ K) s = HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K)
h₁ :
  Membership.mem (α := R ⧸ K) (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I)
    ((mk K : (a : R) → R ⧸ K) (r + s) : R ⧸ K)
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x

Tactic:
rw [← add_sub_cancel ((mk K) r) x, ← eq', ← map_add]

Premises used: Ideal.Quotient.mk, map_add, add_sub_cancel, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
this :
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))
s : R
hs : s ∈ (↑J : Set R)
eq' : (mk K : (a : R) → R ⧸ K) s = HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K)
⊢ Membership.mem (α := R ⧸ K) (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I)
    ((mk K : (a : R) → R ⧸ K) (r + s) : R ⧸ K)

Tactic:
mem_map_of_mem (mk K) (Submodule.add_mem _ hr (hIJ hs))

Premises used: Ideal.mem_map_of_mem, Ideal.Quotient.mk, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
r : R
hr : r ∈ (↑I : Set R)
eq : Eq (α := R ⧸ J) ((mk J : (a : R) → R ⧸ J) r : R ⧸ J) ((factor hJK : (a : R ⧸ K) → R ⧸ J) x : R ⧸ J)
this :
  Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) J)
    (HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K))
s : R
hs : s ∈ (↑J : Set R)
eq' : (mk K : (a : R) → R ⧸ K) s = HSub.hSub (β := R ⧸ K) x ((mk K : (a : R) → R ⧸ K) r : R ⧸ K)
⊢ Membership.mem (α := R ⧸ K) (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I)
    ((mk K : (a : R) → R ⧸ K) (r + s) : R ⧸ K)

Tactic:
exact mem_map_of_mem (mk K) (Submodule.add_mem _ hr (hIJ hs))

Premises used: Ideal.mem_map_of_mem, Ideal.Quotient.mk, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
h₁ :
  ∀ (r : R) (hr : r ∈ (↑I : Set R)) (eq : (mk K : (a : R) → R ⧸ K) r = x),
    Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective h with ⟨r, hr, eq⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J K : Ideal R
inst_1 : J.IsTwoSided
inst_2 : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
r : R
hr : r ∈ (↑I : Set R)
eq : (mk K : (a : R) → R ⧸ K) r = x
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x

Tactic:
simpa only [← eq] using mem_map_of_mem (mk J) hr

Premises used: Ideal.mem_map_of_mem, Ideal.Quotient.mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
h : I ≤ J
x : R ⧸ I
⊢ Eq (α := R ⧸ J) ((mapQ I J LinearMap.id h : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J)
    ((factor h : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I ≤ J
x : R ⧸ I
⊢ Eq (α := R ⧸ J) ((factor h : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J) ((Quotient.factor h : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
h : m ≤ n
⊢ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤ ≤ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤

Tactic:
smul_mono_left (Ideal.pow_le_pow_right h)

Premises used: Set.Mem, Ideal.pow_le_pow_right, Submodule.smul_mono_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
hIJ : I ^ a ≤ I
⊢ Eq (α := Ideal (R ⧸ I ^ b))
    (comap (F := R ⧸ I ^ b →+* R ⧸ I ^ a) (factorPow I le : R ⧸ I ^ b →+* R ⧸ I ^ a)
      (map (F := R →+* R ⧸ I ^ a) (mk (I ^ a)) I))
    (map (F := R →+* R ⧸ I ^ b) (mk (I ^ b)) I)

Tactic:
apply Ideal.map_mk_comap_factor

Premises used: Ideal.map_mk_comap_factor
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ I ^ a ≤ I

Tactic:
pow_le_self (Nat.ne_zero_of_lt apos)

Premises used: Set.Mem, Ideal.pow_le_self, Nat.ne_zero_of_lt
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ I ^ a ≤ I

Tactic:
exact pow_le_self (Nat.ne_zero_of_lt apos)

Premises used: Ideal.pow_le_self, Nat.ne_zero_of_lt
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h :
  IsUnit (M := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n)
rcases :
  ∀ (b : R ⧸ I ^ n)
    (hb :
      HMul.hMul (α := R ⧸ I ^ n)
          (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) b =
        1),
    HMul.hMul (β := R ⧸ I ^ n) b
          (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
        1 →
      IsUnit a
⊢ IsUnit a

Tactic:
rcases isUnit_iff_exists.mp h with ⟨b, hb, _⟩

Premises used: isUnit_iff_exists, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h :
  IsUnit (M := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n)
b : R ⧸ I ^ n
hb :
  HMul.hMul (α := R ⧸ I ^ n)
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) b =
    1
right :
  HMul.hMul (β := R ⧸ I ^ n) b
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
    1
rcases : ∀ (b' : R ⧸ I ^ n.succ) (hb' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b), IsUnit a
⊢ IsUnit a

Tactic:
rcases factor_surjective (pow_le_pow_right n.le_succ) b with ⟨b', hb'⟩

Premises used: Nat.le_succ, Ideal.Quotient.factor_surjective, Ideal.pow_le_pow_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h :
  IsUnit (M := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n)
b : R ⧸ I ^ n
hb :
  HMul.hMul (α := R ⧸ I ^ n)
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) b =
    1
right :
  HMul.hMul (β := R ⧸ I ^ n) b
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
    1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
⊢ Eq (α := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) (a * b') : R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) 1 : R ⧸ I ^ n)

Tactic:
rw [← hb', ← map_one (factorPow I n.le_succ), ← map_mul] at hb

Premises used: Ideal.Quotient.factorPow, Nat.le_succ, map_mul, map_one
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h :
  IsUnit (M := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n)
b : R ⧸ I ^ n
hb :
  HMul.hMul (α := R ⧸ I ^ n)
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) b =
    1
right :
  HMul.hMul (β := R ⧸ I ^ n) b
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
    1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb₁ :
  Eq (α := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) (a * b') : R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) 1 : R ⧸ I ^ n)
⊢ (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b

Tactic:
rw [← hb', ← map_one (factorPow I n.le_succ), ← map_mul] at hb

Premises used: Ideal.Quotient.factorPow, Nat.le_succ, map_mul, map_one
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h :
  IsUnit (M := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n)
b : R ⧸ I ^ n
right :
  HMul.hMul (β := R ⧸ I ^ n) b
      (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
    1
b' : R ⧸ I ^ n.succ
hb :
  Eq (α := R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) (a * b') : R ⧸ I ^ n)
    (((factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) 1 : R ⧸ I ^ n)
hb' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
⊢ Membership.mem (γ := Ideal (R ⧸ I ^ n.succ))
    (RingHom.ker (F := R ⧸ I ^ n.succ →+* R ⧸ I ^ n) (factorPow I ⋯ : R ⧸ I ^ n.succ →+* R ⧸ I ^ n)) (a * b' - 1)

Tactic:
apply (RingHom.sub_mem_ker_iff (factorPow I n.le_succ)).mpr at hb

Premises used: Iff.mpr, Ideal.Quotient.factorPow, Nat.le_succ, RingHom.sub_mem_ker_iff