awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : (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)
⊢ 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

Premises used: Nat.le_succ, Ideal.pow_le_pow_right, Ideal.Quotient.factor_ker
-- 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' : (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)
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
⊢ 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⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Quotient.eq
-- 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' : (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

Tactic:
.of_mul_eq_one (b' * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c)) ?_

Premises used: HMul.hMul, Ideal.Quotient.mk, IsUnit.of_mul_eq_one, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- 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' : (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
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
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one (b' * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c)) ?_
-- 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' : (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))

Tactic:
ring
-- 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' : (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
rw : c * c ∈ I ^ n * HPow.hPow (β := ℕ) I 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

Tactic:
rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]

Premises used: mul_sub, sub_add_sub_cancel', pow_add, sub_eq_self, Ideal.Quotient.eq_zero_iff_mem, map_mul, mul_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' : (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
apply : c ∈ I ^ (n - 1) * HPow.hPow (β := ℕ) I 1
⊢ c * c ∈ I ^ n * HPow.hPow (β := ℕ) I 1

Tactic:
apply Ideal.mul_mem_mul hc (Ideal.mul_le_left (I := I ^ (n - 1)) _)

Premises used: Ideal.mul_mem_mul, Ideal.mul_le_left
-- 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' : (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 ∈ I ^ (n - 1) * HPow.hPow (β := ℕ) I 1

Tactic:
simpa only [← pow_add, Nat.sub_add_cancel npos] using hc

Premises used: pow_add, Nat.sub_add_cancel
-- 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' : (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' - 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
⊢ 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:
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

Premises used: HMul.hMul, Ideal.Quotient.mk, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R_1 : Type u_1
inst : Ring R_1
I_1 J K : Ideal R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u_3
inst_3 : CommRing R
I : Ideal R
M : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ HSMul.hSMul (β := Submodule R ↥(I ^ a • N)) (I ^ b) ⊤ ≤ comap (I ^ a • N).subtype (I ^ c • N)

Tactic:
simp [← map_le_iff_le_comap, h, pow_add, mul_smul]

Premises used: pow_add, Submodule.map_le_iff_le_comap, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
x : ↥(I ^ a • N)
⊢ Eq (α := M ⧸ I ^ c • N)
    ((powSMulQuotInclusion I M h N : (a : ↥(I ^ a • N) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • N) (Quotient.mk x) : M ⧸ I ^ c • N)
    (Quotient.mk (↑x : M) : M ⧸ I ^ c • N)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
rw : (powSMulQuotInclusion I M h N).ker = ⊥
⊢ 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)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
⊢ (powSMulQuotInclusion I M h N).ker = ⊥

Tactic:
simp [powSMulQuotInclusion, mapQ, ← le_bot_iff, ker_liftQ, LinearMap.ker_comp, pow_add, mul_smul,
    map_le_iff_le_comap, ← Submodule.map_le_map_iff_of_injective (I ^ a • N).subtype_injective, h]

Premises used: le_bot_iff, Submodule.map_le_map_iff_of_injective, pow_add, LinearMap.ker_comp, Submodule.powSMulQuotInclusion, Submodule.mapQ, HPow.hPow, HSMul.hSMul, Submodule.map_le_iff_le_comap, Submodule.subtype_injective, Submodule.ker_liftQ, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R_1 : Type u_1
inst : Ring R_1
I_1 J K : Ideal R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u_3
inst_3 : CommRing R
I : Ideal R
M : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
⊢ c ≤ e

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
Goal:
R_1 : Type u_1
inst : Ring R_1
I_1 J K : Ideal R_1
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
R : Type u_3
inst_3 : CommRing R
I : Ideal R
M : Type u_4
inst_4 : AddCommGroup M
inst_5 : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
⊢ e = b + d + a

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
h₁ :
  ∀ (x : ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)),
    Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
      (((factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤) ∘ₗ
              (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) ⊤) ⋯) ∘ₗ
              (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) ⊤)
⊢ 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) ⊤) ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
x : ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    (((factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤) ∘ₗ
            (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) ⊤) ⋯) ∘ₗ
            (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:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition
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
⊢ (powSMulQuotInclusion I M h N).range = map (I ^ c • N).mkQ (I ^ a • N)

Tactic:
simp [powSMulQuotInclusion, mapQ, range_liftQ, LinearMap.range_comp]

Premises used: LinearMap.range_comp, Submodule.powSMulQuotInclusion, Submodule.mapQ, Submodule.range_liftQ
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Eq (α := Submodule α α) (Submodule.span α s) (span s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ Eq.{u + 1} (α := Ideal α) (span ∅) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ Eq.{u + 1} (α := Ideal α) (span univ) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s t : Set α
⊢ Eq (α := Ideal α) (span (s ∪ t)) (span s ⊔ span t)

Tactic:
Submodule.span_union _ _

Premises used: Set.Mem, setOf, Submodule.span_union
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Sort u_1
s : ι → Set α
⊢ Eq.{u + 1} (α := Ideal α) (span (⋃ (i : ι), s i)) (⨆ (i : ι), span (s i))

Tactic:
Submodule.span_iUnion _

Premises used: Submodule.span_iUnion
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
ι : Sort u_1
p : ι → Ideal α
⊢ Eq.{u + 1} (α := Ideal α) (⨆ (i : ι), p i) (span (⋃ (i : ι), (↑(p i) : Set α)))

Tactic:
Submodule.iSup_eq_span p

Premises used: Submodule.iSup_eq_span
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
x : α
⊢ Membership.mem (γ := Ideal α) (span s) x ↔ ∀ (p : Ideal α), s ⊆ (↑p : Set α) → x ∈ p

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ s ⊆ (↑(span s) : Set α)

Tactic:
Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
I : Ideal α
⊢ span s ≤ I ↔ s ⊆ (↑I : Set α)

Tactic:
Submodule.span_le

Premises used: Set.Mem, Submodule.span_le
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s t : Set α
⊢ s ⊆ t → LE.le (α := Ideal α) (span s) (span t)

Tactic:
Submodule.span_mono

Premises used: Set.Mem, Submodule.span_mono
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ span (↑I : Set α) = I

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ Eq (α := Ideal α) (span {1}) ⊤

Tactic:
(eq_top_iff_one _).2 <| subset_span <| mem_singleton _

Premises used: Iff.mpr, Set.mem_singleton, Ideal.subset_span, Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ IsCompactElement.{u} (α := Ideal α) ⊤

Tactic:
simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1

Premises used: Ideal.span_singleton_one, Submodule.singleton_span_isCompactElement, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
x y : α
⊢ Membership.mem (γ := Ideal α) (span (insert y s)) x ↔
    ∃ (a : α) (z : α), Membership.mem (γ := Ideal α) (span s) z ∧ x = a * y + z

Tactic:
Submodule.mem_span_insert

Premises used: Set.Mem, Submodule.mem_span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
β : Type u_1
f : β → α
x : β
⊢ Membership.mem (γ := Ideal α) (span (range f)) (f x)

Tactic:
subset_span (mem_range_self x)

Premises used: Set.mem_range_self, Ideal.subset_span
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x y : α
⊢ Membership.mem (γ := Ideal α) (span {y}) x ↔ ∃ (a : α), a * y = x

Tactic:
Submodule.mem_span_singleton

Premises used: Set.Mem, Submodule.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x : α
⊢ Membership.mem (γ := Ideal α) (span {x}) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x : α
⊢ span {x} ≤ I ↔ x ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ Eq (α := Ideal α) (span {a * x}) (span {x})

Tactic:
Submodule.span_singleton_smul_eq h2 x

Premises used: Submodule.span_singleton_smul_eq
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x : α
s : Set α
⊢ Eq (α := Ideal α) (span (insert x s)) (span {x} ⊔ span s)

Tactic:
Submodule.span_insert x s

Premises used: Set.Mem, setOf, Submodule.span_insert
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Eq (α := Ideal α) (span s) ⊥ ↔ ∀ x ∈ s, x = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x : α
⊢ Eq (α := Ideal α) (span {x}) ⊥ ↔ x = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ Eq (α := Ideal α) (span {0}) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u_1
inst : CommSemiring α
x : α
hx : ¬IsUnit x
⊢ Ne (α := Ideal α) (span {x}) ⊤

Tactic:
(Ideal.ne_top_iff_one _).mpr fun h1 =>
    let ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
    hx ⟨⟨x, y, mul_comm y x ▸ hy, hy⟩, rfl⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', False, Ideal.ne_top_iff_one, _private.0.Ideal.span_singleton_ne_top.match_1, Eq.rec, Units.mk, Exists.intro, Iff.mp, mul_comm, rfl
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
⊢ Eq.{u + 1} (α := Ideal α) (span 0) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Eq (α := Ideal α) (span (insert 0 s)) (span s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Eq (α := Ideal α) (span (s \ {0})) (span s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
rw : Eq (α := Ideal α) (span {1}) ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal α) ⊤ ⊤
⊢ Eq.{u + 1} (α := Ideal α) (span 1) ⊤

Tactic:
rw [← Set.singleton_one, span_singleton_one]

Premises used: Ideal.span_singleton_one, Set.singleton_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
simp_rw :
  Membership.mem (γ := Ideal α) (span s) 1 ↔
    ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Membership.mem (γ := Ideal α) (span (↑s' : Set α)) 1
⊢ Eq (α := Ideal α) (span s) ⊤ ↔ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Eq (α := Ideal α) (span (↑s' : Set α)) ⊤

Tactic:
simp_rw [eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Membership.mem (γ := Ideal α) (span s) 1 ↔
    ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Membership.mem (γ := Ideal α) (span (↑s' : Set α)) 1

Tactic:
⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

Premises used: Membership.mem, Submodule.mem_span_finite_of_mem_span, _private.0.Ideal.span_eq_top_iff_finite.match_1, Iff.intro, Ideal.span_mono, Ideal.span, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
s : Set α
⊢ Membership.mem (γ := Ideal α) (span s) 1 ↔
    ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ Membership.mem (γ := Ideal α) (span (↑s' : Set α)) 1

Tactic:
exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩
-- Module: Mathlib.RingTheory.Ideal.Span
Goal:
α : Type u
inst : Semiring α
x y : α
I : Ideal α
rw :
  (∃ (y_1 : α), Membership.mem (γ := Submodule α α) (span {y}) y_1 ∧ ∃ z ∈ I, y_1 + z = x) ↔
    ∃ (a : α), ∃ b ∈ I, a * y + b = x
⊢ x ∈ span {y} ⊔ I ↔ ∃ (a : α), ∃ b ∈ I, a * y + b = x

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup