awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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))
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have 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
Tactic: rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective this with ⟨s, hs, eq'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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 (γ := Ideal (R ⧸ K)) (map (F := R →+* R ⧸ K) (mk K) I) x
have 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)
Tactic: rw [← add_sub_cancel ((mk K) r) x, ← eq', ← map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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
⊢ Membership.mem (γ := Ideal (R ⧸ K)) (comap (F := R ⧸ K →+* R ⧸ J) (factor hJK) (map (F := R →+* R ⧸ J) (mk J) I)) x
have 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
Tactic: rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective h with ⟨r, hr, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ 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)
have hIJ : I ^ a ≤ I
Tactic: apply Ideal.map_mk_comap_factor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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)
⊢ IsUnit a
have rcases : ∀ (b : R ⧸ I ^ n)
  (hb :
    HMul.hMul (α := R ⧸ I ^ n)
        (((factorPow I sorry : 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 sorry : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) a : R ⧸ I ^ n) =
      1 →
    IsUnit a
Tactic: rcases isUnit_iff_exists.mp h with ⟨b, hb, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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
⊢ IsUnit a
have rcases : ∀ (b' : R ⧸ I ^ n.succ) (hb' : (factor sorry : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b), IsUnit a
Tactic: rcases factor_surjective (pow_le_pow_right n.le_succ) b with ⟨b', hb'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
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
⊢ IsUnit a
have hb₁ : Eq (α := R ⧸ I ^ n)
  (((factorPow I sorry : R ⧸ I ^ n.succ →+* R ⧸ I ^ n) : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) (a * b') : R ⧸ I ^ n)
  (((factorPow I sorry : 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
Cleared hypotheses: hb, hb'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
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
⊢ IsUnit a
have hb₁ : Membership.mem (γ := Ideal (R ⧸ I ^ n.succ))
  (RingHom.ker (F := R ⧸ I ^ n.succ →+* R ⧸ I ^ n) (factorPow I sorry : 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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (hypothesis)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  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)
⊢ IsUnit a
have hb₁ : Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
Tactic: rw [factor_ker (pow_le_pow_right n.le_succ)] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
⊢ IsUnit a
have rcases : ∀ (c : R) (hc : c ∈ (↑(I ^ n) : Set R)) (eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1), IsUnit a
Tactic: rcases Ideal.mem_image_of_mem_map_of_surjective (Ideal.Quotient.mk (I ^ (n + 1)))
    Ideal.Quotient.mk_surjective hb with ⟨c, hc, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
c : R
hc : c ∈ (↑(I ^ n) : Set R)
eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1
⊢ IsUnit a
have refine : a *
    (b' *
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))) =
  1
Tactic: refine .of_mul_eq_one (b' * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
c : R
hc : c ∈ (↑(I ^ n) : Set R)
eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1
⊢ (a * b' - 1) *
        HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
          ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) +
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) =
    1
have rw : c * c ∈ I ^ n * HPow.hPow (β := ℕ) I 1
Tactic: rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
c : R
hc : c ∈ (↑(I ^ n) : Set R)
eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1
⊢ c * c ∈ I ^ n * HPow.hPow (β := ℕ) I 1
have apply : c ∈ I ^ (n - 1) * HPow.hPow (β := ℕ) I 1
Tactic: apply Ideal.mul_mem_mul hc (Ideal.mul_le_left (I := I ^ (n - 1)) _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
c : R
hc : c ∈ (↑(I ^ n) : Set R)
eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1
⊢ a *
      (b' *
        HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
          ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))) =
    1
have _ : a *
    (b' *
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))) =
  (a * b' - 1) *
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) +
    HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
      ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))
Tactic: calc
    _ = (a * b' - 1) * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) +
        (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) := by ring
    _ = 1 := by
      rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]
      apply Ideal.mul_mem_mul hc (Ideal.mul_le_left (I := I ^ (n - 1)) _)
      simpa only [← pow_add, Nat.sub_add_cancel npos] using hc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
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' : (factor ⋯ : (a : R ⧸ I ^ n.succ) → R ⧸ I ^ n) b' = b
hb :
  Membership.mem (γ := Ideal (R ⧸ I ^ n.succ)) (map (F := R →+* R ⧸ I ^ n.succ) (mk (I ^ n.succ)) (I ^ n)) (a * b' - 1)
c : R
hc : c ∈ (↑(I ^ n) : Set R)
eq : (mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c = a * b' - 1
_ :
  a *
      (b' *
        HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
          ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))) =
    (a * b' - 1) *
        HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
          ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) +
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))
⊢ a *
      (b' *
        HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
          ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1))) =
    1
have _₁ : (a * b' - 1) *
      HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
        ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) +
    HSub.hSub (α := R ⧸ I ^ (n + 1)) (β := R ⧸ I ^ (n + 1)) (1 : R ⧸ I ^ (n + 1))
      ((mk (I ^ (n + 1)) : (a : R) → R ⧸ I ^ (n + 1)) c : R ⧸ I ^ (n + 1)) =
  1
Tactic: calc
    _ = (a * b' - 1) * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) +
        (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) := by ring
    _ = 1 := by
      rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]
      apply Ideal.mul_mem_mul hc (Ideal.mul_le_left (I := I ^ (n - 1)) _)
      simpa only [← pow_add, Nat.sub_add_cancel npos] using hc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ Function.Injective (α := ↥(I ^ a • N) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ a • N)) (I ^ b) ⊤) (β := M ⧸ I ^ c • N)
    (⇑(powSMulQuotInclusion I M h N) : (a : ↥(I ^ a • N) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • N)
have rw : (powSMulQuotInclusion I M h N).ker = ⊥
Tactic: rw [← LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.PowTransition (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
⊢ Eq (α :=
    ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) ⧸
        HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)) (I ^ (b + d)) ⊤ →ₗ[R]
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    (factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤)
    (powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) ⋯)
have h₁ : ∀ (x : ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)),
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    (((factorPow I M sorry ∘ₗ powSMulQuotInclusion I M sorry ⊤) ∘ₗ
            (HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)) (I ^ (b + d)) ⊤).mkQ :
          (a : ↥(I ^ a • ⊤)) → M ⧸ I ^ c • ⊤)
        x :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    (((powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) sorry) ∘ₗ
            (HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)) (I ^ (b + d)) ⊤).mkQ :
          (a : ↥(I ^ a • ⊤)) → M ⧸ I ^ c • ⊤)
        x :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
⊢ Eq.{u + 1} (α := Ideal α) (span 1) ⊤
have rw : Eq (α := Ideal α) (span {1}) ⊤
Tactic: rw [← Set.singleton_one, span_singleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
rw : Eq (α := Ideal α) (span {1}) ⊤
⊢ Eq.{u + 1} (α := Ideal α) (span 1) ⊤
have rw₁ : Eq.{u + 1} (α := Ideal α) ⊤ ⊤
Tactic: rw [← Set.singleton_one, span_singleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Eq (α := Ideal α) (span s) ⊤ ↔ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Eq (α := Ideal α) (span (↑s' : Set α)) ⊤
have simp_rw : Membership.mem (γ := Ideal α) (span s) 1 ↔
  ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Membership.mem (γ := Ideal α) (span (↑s' : Set α)) 1
Tactic: simp_rw [eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
x y : α
I : Ideal α
⊢ x ∈ span {y} ⊔ I ↔ ∃ (a : α), ∃ b ∈ I, a * y + b = x
have rw : (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) ↔
  ∃ (a : α), ∃ b ∈ I, a * y + b = x
Tactic: rw [Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
x y : α
I : Ideal α
⊢ (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) ↔
    ∃ (a : α), ∃ b ∈ I, a * y + b = x
have mp : (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) →
  ∃ (a : α), ∃ b ∈ I, a * y + b = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
x y : α
I : Ideal α
mp :
  (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) →
    ∃ (a : α), ∃ b ∈ I, a * y + b = x
⊢ (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) ↔
    ∃ (a : α), ∃ b ∈ I, a * y + b = x
have mpr : (∃ (a : α), ∃ b ∈ I, a * y + b = x) →
  ∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
y : α
I : Ideal α
ya : α
hya : Membership.mem (γ := Submodule α α) (span {y}) ya
b : α
hb : b ∈ I
⊢ ∃ (a : α), ∃ b_1 ∈ I, a * y + b_1 = ya + b
have mp : ∀ (a : α) (hya : Membership.mem (γ := Submodule α α) (span {y}) (a * y)),
  ∃ (a_1 : α), ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b
Tactic: obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
Cleared hypotheses: ya, hya
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
x : α
⊢ Eq (α := Ideal α) (span {x, 0}) (span {x})
have rw : Eq (α := Ideal α) (span {0, x}) (span {x})
Tactic: rw [span_pair_comm, span_insert_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
x : α
rw : Eq (α := Ideal α) (span {0, x}) (span {x})
⊢ Eq (α := Ideal α) (span {x, 0}) (span {x})
have rw₁ : Eq (α := Ideal α) (span {x}) (span {x})
Tactic: rw [span_pair_comm, span_insert_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
⊢ Eq (α := Ideal α) (span (range x)) (⨆ (i : ι), span {x i})
have rw : Eq (α := Ideal α) (span (range x)) (span (⋃ (i : ι), {x i}))
Tactic: rw [← span_iUnion, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
rw : Eq (α := Ideal α) (span (range x)) (span (⋃ (i : ι), {x i}))
⊢ Eq (α := Ideal α) (span (range x)) (⨆ (i : ι), span {x i})
have rw₁ : Eq (α := Ideal α) (span (range x)) (span (range x))
Tactic: rw [← span_iUnion, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
⊢ Eq (α := Ideal α) (span (range x)) (span (range fun (i : (↑(Function.support x) : Type u_1)) ↦ x (↑i : ι)))
have rw : Eq (α := Ideal α) (span (range x \ {0})) (span (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)))
Tactic: rw [← span_sdiff_singleton_zero (s := range x), Function.support]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
⊢ Eq (α := Ideal α) (span (range x \ {0})) (span (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)))
have e_s : range x \ {0} = range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
⊢ range x \ {0} = range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)
have e_s : ∀ (a : α),
  a ∈ range x \ {0} ↔ Membership.mem (γ := Set α) (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)) a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : Semiring α
ι : Type u_1
x : ι → α
a : α
⊢ a ∈ range x \ {0} ↔ Membership.mem (γ := Set α) (range fun (i : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)) ↦ x (↑i : ι)) a
have e_s : (∃ (y : ι), x y = a) ∧ ¬a = 0 ↔ ∃ (y : (↑{x_1 : ι | x x_1 ≠ 0} : Type u_1)), x (↑y : ι) = a
Tactic: simp only [mem_diff, mem_range, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y x_1 : α
⊢ x_1 * y = x ↔ x = y * x_1
have rw : x = x_1 * y ↔ x = y * x_1
Tactic: rw [eq_comm, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
x y x_1 : α
rw : x = x_1 * y ↔ x = y * x_1
⊢ x_1 * y = x ↔ x = y * x_1
have rw₁ : x = y * x_1 ↔ x = y * x_1
Tactic: rw [eq_comm, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Span (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
⊢ Eq (α := Ideal α) (span {x}) (span {y}) ↔ Associated x y
have rw : LE.le (α := Ideal α) (span {y}) (span {x}) ∧ LE.le (α := Ideal α) (span {x}) (span {y}) ↔ x ∣ y ∧ y ∣ x
Tactic: rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]