awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x y : R
rw :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) (x - y) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    HSub.hSub (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
rw₂ rw₃ :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔ x - y ∈ I

Tactic:
rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) 1 : R ⧸ I)
rw₁ rw₂ :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔ x - 1 ∈ I

Tactic:
rw [← mk_eq_mk_iff_sub_mem, map_one]

Premises used: map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R ⧸ I
⊢ (mk I : (a : R) → R ⧸ I) (Quotient.out x) = x

Tactic:
Quotient.out_eq x

Premises used: Submodule.Quotient.mk, Quotient.out_eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ Function.Surjective (α := R) (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I)

Tactic:
fun y =>
  Quotient.inductionOn' y fun x => Exists.intro x rfl

Premises used: Quotient.inductionOn', Function.Surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst_1 : I.IsTwoSided
⊢ RingHomSurjective (mk I)

Tactic:
⟨mk_surjective⟩

Premises used: Ideal.Quotient.mk_surjective, RingHomSurjective.mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s))
        x ↔
      Membership.mem (γ := Set R) (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s) x
⊢ Eq (α := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s))
    (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h : (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
⊢ Membership.mem (γ := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s)) x ↔
    Membership.mem (γ := Set R) (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s) x

Tactic:
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]

Premises used: Set.mem_iUnion, Set.mem_image, Ideal.Quotient.eq, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h_1 : ∃ x_1 ∈ s, x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) (-(a - x)) ⋯) : R) + a = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h : ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) + a = x
rw : -(↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) ∈ I
⊢ a - x ∈ I

Tactic:
rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]

Premises used: sub_self, zero_sub, sub_add_eq_sub_sub_swap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h : ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) + a = x
⊢ -(↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) ∈ I

Tactic:
I.neg_mem hi

Premises used: Set.Mem, Submodule.neg_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h : ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) + a = x
⊢ -(↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) ∈ I

Tactic:
exact I.neg_mem hi

Premises used: Submodule.neg_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
⊢ (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x

Tactic:
exact
    ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
      ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
a : R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) : S)
    ((f : (a : R) → S) a : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift I f H) (mk I) = f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : S
obtain : ∀ (x : R), ∃ (a : R ⧸ I), Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) a : S) ((f : (a : R) → S) x : S)
⊢ ∃ (a : R ⧸ I), (lift I f H : (a : R ⧸ I) → S) a = y

Tactic:
obtain ⟨x, rfl⟩ := hf y

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
h :
  Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) : S)
    ((f : (a : R) → S) x : S)
⊢ ∃ (a : R ⧸ I), Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) a : S) ((f : (a : R) → S) x : S)

Tactic:
use Ideal.Quotient.mk I x

Premises used: Ideal.Quotient.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) : S)
    ((f : (a : R) → S) x : S)

Tactic:
simp only [Ideal.Quotient.lift_mk]

Premises used: Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
x : R
⊢ Eq (α := R ⧸ T) ((factor H : (a : R ⧸ S) → R ⧸ T) ((mk S : (a : R) → R ⧸ S) x) : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S : Ideal R
inst_1 : S.IsTwoSided
h :
  ∀ (x : R),
    Eq (α := R ⧸ S)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)
      ((RingHom.comp (RingHom.id (R ⧸ S)) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)
⊢ Eq (α := R ⧸ S →+* R ⧸ S) (factor ⋯) (RingHom.id (R ⧸ S))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S : Ideal R
inst_1 : S.IsTwoSided
x : R
⊢ Eq (α := R ⧸ S) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)
    ((RingHom.comp (RingHom.id (R ⧸ S)) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
a :
  ∀ (x : R),
    Eq (α := R ⧸ T)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S) : (a : R) → R ⧸ T) x : R ⧸ T)
      ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
⊢ Eq (α := R →+* R ⧸ T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S)) (mk T)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
x : R
a :
  Eq (α := R ⧸ T) ((factor H : (a : R ⧸ S) → R ⧸ T) ((mk S : (a : R) → R ⧸ S) x) : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
a₁ a₂ : Eq (α := R ⧸ T) ((mk T : (a : R) → R ⧸ T) x : R ⧸ T) ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
⊢ Eq (α := R ⧸ T) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S) : (a : R) → R ⧸ T) x : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)

Tactic:
rw [RingHom.comp_apply, factor_mk]

Premises used: Ideal.Quotient.factor_mk, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
h :
  ∀ (x : R),
    Eq (α := R ⧸ U)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1)) (mk S) :
            (a : R) → R ⧸ U)
          x :
        R ⧸ U)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (mk S) : (a : R) → R ⧸ U) x : R ⧸ U)
⊢ Eq (α := R ⧸ S →+* R ⧸ U) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1)) (factor ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R
⊢ Eq (α := R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1)) (mk S) :
          (a : R) → R ⧸ U)
        x :
      R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (mk S) : (a : R) → R ⧸ U) x : R ⧸ U)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
rw :
  Eq (α := R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1) : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
    ((factor ⋯ : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
⊢ Eq (α := R ⧸ U) ((factor H2 : (a : R ⧸ T) → R ⧸ U) ((factor H1 : (a : R ⧸ S) → R ⧸ T) x) : R ⧸ U)
    ((factor ⋯ : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)

Tactic:
rw [← RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ Eq (α := R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1) : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
    ((factor ⋯ : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
⊢ Function.Surjective (α := R ⧸ S) (β := R ⧸ T) (⇑(factor H) : (a : R ⧸ S) → R ⧸ T)

Tactic:
Ideal.Quotient.lift_surjective_of_surjective _ _ Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.lift_surjective_of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
a b : R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
x_1 : R ⧸ I
x : R
y_1 : R ⧸ I
y : R
⊢ AddHom.toFun (LinearMap.toAddHom (↑(Submodule.quotEquivOfEq I J h) : R ⧸ I →ₗ[R] R ⧸ J))
      (HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y)) =
    HMul.hMul (α := R ⧸ J)
      (AddHom.toFun (M := R ⧸ I) (LinearMap.toAddHom (↑(Submodule.quotEquivOfEq I J h) : R ⧸ I →ₗ[R] R ⧸ J))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x))
      (AddHom.toFun (M := R ⧸ I) (LinearMap.toAddHom (↑(Submodule.quotEquivOfEq I J h) : R ⧸ I →ₗ[R] R ⧸ J))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
x : R
⊢ Eq (α := R ⧸ J) ((quotEquivOfEq h : (a : R ⧸ I) → R ⧸ J) ((Quotient.mk I : (a : R) → R ⧸ I) x) : R ⧸ J)
    ((Quotient.mk J : (a : R) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
h₁ :
  ∀ (x : R ⧸ J),
    Eq (α := R ⧸ I) ((RingEquiv.symm (quotEquivOfEq h) : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)
      ((quotEquivOfEq ⋯ : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)
⊢ Eq (α := R ⧸ J ≃+* R ⧸ I) (RingEquiv.symm (quotEquivOfEq h)) (quotEquivOfEq ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
x : R ⧸ J
⊢ Eq (α := R ⧸ I) ((RingEquiv.symm (quotEquivOfEq h) : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)
    ((quotEquivOfEq ⋯ : (a : R ⧸ J) → R ⧸ I) x : R ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
inst_2 : J.IsTwoSided
h : I = J
x : R ⧸ I
⊢ Eq (α := R ⧸ J) ((quotEquivOfEq h : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J)
    ((Quotient.factor ⋯ : (a : R ⧸ I) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Quotient, Quot.map, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
P : Ideal R
inst_2 : P.IsPrime
hp : P ≠ ⊥
⊢ P.IsMaximal

Tactic:
have : Finite (R ⧸ P) := finiteQuotient hp
  Ideal.Quotient.maximal_of_isField P <| Finite.isField_of_domain (R ⧸ P)

Premises used: Finite.isField_of_domain, HasQuotient.Quotient, Ideal.Quotient.maximal_of_isField, Ring.HasFiniteQuotients.finiteQuotient
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
⊢ IsNoetherianRing R

Tactic:
(isNoetherianRing_iff_ideal_fg R).mpr fun I ↦ ?_

Premises used: Iff.mpr, isNoetherianRing_iff_ideal_fg
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
refine : ∀ (I : Ideal R), I.FG
⊢ IsNoetherianRing R

Tactic:
refine (isNoetherianRing_iff_ideal_fg R).mpr fun I ↦ ?_

Premises used: Iff.mpr, isNoetherianRing_iff_ideal_fg
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
pos : ∀ (hI : I = 0), I.FG
neg : ∀ (hI : ¬I = 0), I.FG
⊢ I.FG

Tactic:
by_cases hI : I = 0
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I = 0
⊢ I.FG

Tactic:
hI ▸ Submodule.fg_bot

Premises used: Eq.rec, Submodule.fg_bot, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I = 0
⊢ I.FG

Tactic:
exact hI ▸ Submodule.fg_bot
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
neg : ∀ (x : R) (hx₁ : x ∈ I) (hx₂ : x ≠ 0), I.FG
⊢ I.FG

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ I.FG

Tactic:
Submodule.fg_of_fg_map_of_fg_inf_ker (Submodule.mkQ (Ideal.span {x})) ?_ ?_

Premises used: Submodule.FG, Ideal.FG, Submodule.mkQ, Ideal.span, Singleton.singleton, Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
neg :
  Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
    (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)
neg₁ :
  (I ⊓
      LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x})) (τ₁₂ := RingHom.id R)
        (Submodule.mkQ (Ideal.span {x}))).FG
⊢ I.FG

Tactic:
refine Submodule.fg_of_fg_map_of_fg_inf_ker (Submodule.mkQ (Ideal.span {x})) ?_ ?_

Premises used: Submodule.mkQ, Ideal.span, Singleton.singleton, Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Ne (α := Ideal R) (Ideal.span {x}) ⊥

Tactic:
simp [hx₂]
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))

Tactic:
have := finiteQuotient (I := Ideal.span {x}) (by simp [hx₂])
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
⊢ Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
    (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)

Tactic:
Submodule.FG.of_finite

Premises used: Submodule.FG.of_finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
⊢ Submodule.FG.{u_1, u_1} (R := R) (M := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x}))
    (Submodule.map (Submodule.mkQ (Ideal.span {x})) I)

Tactic:
exact Submodule.FG.of_finite

Premises used: Submodule.FG.of_finite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
neg : Submodule.FG (R := R) (Ideal.span {x})
⊢ (I ⊓
      LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient R (B := Submodule R R) (Ideal.span {x})) (τ₁₂ := RingHom.id R)
        (Submodule.mkQ (Ideal.span {x}))).FG

Tactic:
rw [Submodule.ker_mkQ, inf_eq_right.mpr ((Ideal.span_singleton_le_iff_mem I).mpr hx₁)]

Premises used: Iff.mpr, Ideal.span_singleton_le_iff_mem, Submodule.ker_mkQ, inf_eq_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Submodule.FG (R := R) (Ideal.span {x})

Tactic:
Submodule.fg_span_singleton x

Premises used: Submodule.fg_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Submodule.FG (R := R) (Ideal.span {x})

Tactic:
exact Submodule.fg_span_singleton x

Premises used: Submodule.fg_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I ≠ ⊥
⊢ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
have := finiteQuotient hI
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I ≠ ⊥
this : Finite.{u_1 + 1} (R ⧸ I)
⊢ 0 < Nat.card.{u_1} (R ⧸ I)

Tactic:
Nat.card_pos

Premises used: Nat.card_pos
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
I : Ideal R
hI : I ≠ ⊥
this : Finite.{u_1 + 1} (R ⧸ I)
⊢ 0 < Nat.card.{u_1} (R ⧸ I)

Tactic:
exact Nat.card_pos

Premises used: Nat.card_pos
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
x : R
hx : x ≠ 0
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))

Tactic:
have := finiteQuotient (mt Ideal.span_singleton_eq_bot.mp hx)
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
x : R
hx : x ≠ 0
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
⊢ Set.Finite.{u_1} (α := Ideal R)
    {I : Ideal R |
      Ideal.comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
          (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤
        I}

Tactic:
have : {I | Ideal.comap (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤ I}.Finite :=
    .of_equiv _ (Ideal.relIsoOfSurjective _ Ideal.Quotient.mk_surjective).toEquiv
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
x : R
hx : x ≠ 0
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
this :
  Set.Finite.{u_1} (α := Ideal R)
    {I : Ideal R |
      Ideal.comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x}))
          (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤
        I}
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | x ∈ I}

Tactic:
simpa [← RingHom.ker_eq_comap_bot] using this

Premises used: RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
inl : Finite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
inr : Infinite R → Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}

Tactic:
rcases finite_or_infinite R

Premises used: finite_or_infinite
-- Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Goal:
R : Type u_1
inst : CommRing R
inst_1 : HasFiniteQuotients R
B : ℕ
h : Finite R
⊢ Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | Submodule.cardQuot.{u_1, u_1} (R := R) (M := R) I ≤ B}

Tactic:
apply Set.toFinite

Premises used: Set.toFinite