awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit (M := S ⧸ I)
      ((DoubleQuot.quotQuotEquivQuotOfLE ⋯ : (a : (S ⧸ I ^ n) ⧸ map (mk (I ^ n)) I) → S ⧸ I)
          ((mk (map (F := S →+* S ⧸ I ^ n) (mk (I ^ n)) I) : (a : S ⧸ I ^ n) → (S ⧸ I ^ n) ⧸ map (mk (I ^ n)) I)
            ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x)) :
        S ⧸ I) ↔
    IsUnit (M := S ⧸ I) ((mk I : (a : S) → S ⧸ I) x : S ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
h : HPow.hPow (α := Ideal (S ⧸ I ^ n)) (map (F := S →+* S ⧸ I ^ n) (mk (I ^ n)) I) n = 0
⊢ IsNilpotent (R := Ideal (S ⧸ I ^ n)) (map (F := S →+* S ⧸ I ^ n) (mk (I ^ n)) I)

Tactic:
use n
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := Ideal (S ⧸ I ^ n)) (map (F := S →+* S ⧸ I ^ n) (mk (I ^ n)) I) n = 0

Tactic:
simp [← Ideal.map_pow]

Premises used: Ideal.map_pow
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
rw : Ne (α := S ⧸ I) ((mk I : (a : S) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I) ↔ x ∉ I
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n) ↔ x ∉ I

Tactic:
rw [isUnit_mk_pow_iff_isUnit_mk I hn, isUnit_iff_ne_zero]

Premises used: isUnit_iff_ne_zero, Ideal.Quotient.isUnit_mk_pow_iff_isUnit_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ Ne (α := S ⧸ I) ((mk I : (a : S) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I) ↔ x ∉ I

Tactic:
Ideal.Quotient.eq_zero_iff_mem.not

Premises used: Set.Mem, Iff.not, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ Ne (α := S ⧸ I) ((mk I : (a : S) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I) ↔ x ∉ I

Tactic:
exact Ideal.Quotient.eq_zero_iff_mem.not

Premises used: Iff.not, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
pos : ∀ (hn : n = 0), IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)
neg : ∀ (hn : n ≠ 0), IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
by_cases! hn : n = 0
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
pos :
  IsUnit (M := HasQuotient.Quotient S (B := Ideal S) ⊤)
    ((mk ⊤ : (a : S) → S ⧸ ⊤) x : HasQuotient.Quotient S (B := Ideal S) ⊤)
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
rw [pow_eq_top_iff.mpr (Or.inr hn)]

Premises used: Iff.mpr, Ideal.pow_eq_top_iff, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit (M := HasQuotient.Quotient S (B := Ideal S) ⊤)
    ((mk ⊤ : (a : S) → S ⧸ ⊤) x : HasQuotient.Quotient S (B := Ideal S) ⊤)

Tactic:
isUnit_of_subsingleton _

Premises used: isUnit_of_subsingleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit (M := HasQuotient.Quotient S (B := Ideal S) ⊤)
    ((mk ⊤ : (a : S) → S ⧸ ⊤) x : HasQuotient.Quotient S (B := Ideal S) ⊤)

Tactic:
exact isUnit_of_subsingleton _

Premises used: isUnit_of_subsingleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n ≠ 0
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
(isUnit_mk_pow_iff_notMem I hn).mpr hx

Premises used: Iff.mpr, Ideal.Quotient.isUnit_mk_pow_iff_notMem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n ≠ 0
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
exact (isUnit_mk_pow_iff_notMem I hn).mpr hx

Premises used: Iff.mpr, Ideal.Quotient.isUnit_mk_pow_iff_notMem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
⊢ IsNoetherianRing.{u_1} (R ⧸ I)

Tactic:
isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| inferInstance

Premises used: Iff.mpr, inferInstance, isNoetherianRing_iff, isNoetherian_of_tower
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
r : R
⊢ Eq.{v + 1} (α := S)
    ((f.kerLift : (a : R ⧸ ker f) → S)
        ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) r : HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)
    ((f : (a : R) → S) r : S)

Tactic:
Ideal.Quotient.lift_mk _ _ _

Premises used: Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
rw : ∀ (x : R ⧸ I), Eq.{v + 1} (α := S) ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) x : S) (0 : S) → x = 0
⊢ Function.Injective.{u + 1, v + 1} (α := R ⧸ I) (β := S) (⇑(Ideal.Quotient.lift I f H) : (a : R ⧸ I) → S)

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]

Premises used: RingHom.ker_eq_bot_iff_eq_zero, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
u : R ⧸ I
hu : Eq.{v + 1} (α := S) ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) u : S) (0 : S)
obtain :
  ∀ (v : R)
    (hu :
      Eq.{v + 1} (α := S)
        ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) : S)
        (0 : S)),
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) (0 : R ⧸ I)
⊢ u = 0

Tactic:
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu :
  Eq.{v + 1} (α := S)
    ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) : S) (0 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)

Tactic:
rw [Ideal.Quotient.lift_mk] at hu

Premises used: Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu : Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)
rw : v ∈ I
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) (0 : R ⧸ I)

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu : Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)
⊢ v ∈ I

Tactic:
hI (RingHom.mem_ker.mpr hu)

Premises used: Iff.mpr, Set.Mem, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu : Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)
⊢ v ∈ I

Tactic:
exact hI (RingHom.mem_ker.mpr hu)

Premises used: Iff.mpr, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
a : R
⊢ Membership.mem (γ := Ideal R) (ker f) a → Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)

Tactic:
simp only [mem_ker, imp_self]

Premises used: RingHom.mem_ker, imp_self
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g (⇑f : (a : R) → S)
x_1 : HasQuotient.Quotient R (B := Ideal R) (ker f)
x : R
mk :
  Eq.{v + 1} (α := S)
    ((f.kerLift : (a : R ⧸ ker f) → S)
        (((⇑(Ideal.Quotient.mk (ker f)) : (a : R) → R ⧸ ker f) ∘ g)
          ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x))) :
      S)
    ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x) : S)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((⇑(Ideal.Quotient.mk (ker f)) : (a : R) → R ⧸ ker f) ∘ g)
      ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x)))
    (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x)

Tactic:
apply kerLift_injective

Premises used: RingHom.kerLift_injective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g (⇑f : (a : R) → S)
x_1 : HasQuotient.Quotient R (B := Ideal R) (ker f)
x : R
⊢ Eq.{v + 1} (α := S)
    ((f.kerLift : (a : R ⧸ ker f) → S)
        (((⇑(Ideal.Quotient.mk (ker f)) : (a : R) → R ⧸ ker f) ∘ g)
          ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x))) :
      S)
    ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x) : S)

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk,
        Function.comp_apply, hf (f x)]

Premises used: Ideal.Quotient.mk_eq_mk, Function.comp_apply, Submodule.Quotient.quot_mk_eq_mk, DFunLike.coe, RingHom.kerLift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g (⇑f : (a : R) → S)
x : HasQuotient.Quotient R (B := Ideal R) (ker f)
⊢ Eq.{v + 1} (α := S) ((quotientKerEquivOfRightInverse hf : (a : R ⧸ ker f) → S) x : S)
    ((f.kerLift : (a : R ⧸ ker f) → S) x : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g (⇑f : (a : R) → S)
x : S
⊢ Eq.{u + 1} (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((quotientKerEquivOfRightInverse hf).symm : (a : S) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))
    ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) (g x) : HasQuotient.Quotient R (B := Ideal R) (ker f))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S)
    ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
        ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)
    ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
a :
  Eq.{v + 1} (α := S)
    ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
        (((quotientKerEquivOfSurjective hf).symm : (a : S) → R ⧸ ker f) ((f : (a : R) → S) x) :
          HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)
    ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
        ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)
⊢ Eq.{u + 1} (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((quotientKerEquivOfSurjective hf).symm : (a : S) → R ⧸ ker f) ((f : (a : R) → S) x) :
      HasQuotient.Quotient R (B := Ideal R) (ker f))
    ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))

Tactic:
apply (RingHom.quotientKerEquivOfSurjective hf).injective

Premises used: RingEquiv.injective, RingHom.quotientKerEquivOfSurjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S)
    ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
        (((quotientKerEquivOfSurjective hf).symm : (a : S) → R ⧸ ker f) ((f : (a : R) → S) x) :
          HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)
    ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
        ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f)) :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a :
  ∀ (x : R),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
      (((quotientKerEquivOfSurjective hf).symm.toRingHom.comp f : (a : R) → R ⧸ ker f) x :
        HasQuotient.Quotient R (B := Ideal R) (ker f))
      ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))
⊢ (quotientKerEquivOfSurjective hf).symm.toRingHom.comp f = Ideal.Quotient.mk (ker f)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((quotientKerEquivOfSurjective hf).symm.toRingHom.comp f : (a : R) → R ⧸ ker f) x :
      HasQuotient.Quotient R (B := Ideal R) (ker f))
    ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I) ⊥

Tactic:
eq_bot_iff.2 <|
    Ideal.map_le_iff_le_comap.2 fun _ hx =>
      (Submodule.mem_bot (R ⧸ I)).2 <| Ideal.Quotient.eq_zero_iff_mem.2 hx

Premises used: Iff.mpr, Submodule.mem_bot, Ideal.Quotient.eq_zero_iff_mem, HasQuotient.Quotient, Ideal.map_le_iff_le_comap, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
⊢ ker (F := R →+* R ⧸ I) (Quotient.mk I) = I

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
h : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥) x ↔ x ∈ I
h₁ : Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) ⊥ ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔ x ∈ I
h₂ : Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ↔ x ∈ I
h₃ h₄ : x ∈ I ↔ x ∈ I
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I

Tactic:
rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]

Premises used: Submodule.mem_bot, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : J.IsTwoSided
h rw : I ≤ J
⊢ Eq (α := Ideal (R ⧸ J)) (map (F := R →+* R ⧸ J) (Quotient.mk J) I) ⊥

Tactic:
rw [map_eq_bot_iff_le_ker, mk_ker]

Premises used: Ideal.mk_ker, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ≤ J
⊢ I ≤ J

Tactic:
h
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : J.IsTwoSided
h : I ≤ J
⊢ I ≤ J

Tactic:
exact h
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
h :
  ∀ (x : R ⧸ I),
    Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x ↔
      Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ Eq (α := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f))

Tactic:
apply Ideal.ext

Premises used: Ideal.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
h :
  Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x →
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
h₁ :
  Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x →
    Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
h :
  ∀ (y : R) (hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x),
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x

Tactic:
obtain ⟨y, hy⟩ := Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
y : R
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
h :
  ∀ (y : R) (hx : Membership.mem (γ := Ideal R) (ker f) y) (hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x),
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x

Tactic:
rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx

Premises used: RingHom.mem_ker, Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : Membership.mem (γ := Ideal R) (ker f) y
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
h :
  ∃ (x : R),
    Membership.mem (γ := Ideal R) (ker f) x ∧
      Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x

Tactic:
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : Membership.mem (γ := Ideal R) (ker f) y
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ ∃ (x : R),
    Membership.mem (γ := Ideal R) (ker f) x ∧
      Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
⟨y, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : Membership.mem (γ := Ideal R) (ker f) y
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ ∃ (x : R),
    Membership.mem (γ := Ideal R) (ker f) x ∧
      Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
exact ⟨y, hx, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ ∃ (x_1 : R), Membership.mem (γ := Ideal R) (ker f) x_1 ∧ (Quotient.mk I : (a : R) → R ⧸ I) x_1 = x

Tactic:
rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : ∃ (x_1 : R), Membership.mem (γ := Ideal R) (ker f) x_1 ∧ (Quotient.mk I : (a : R) → R ⧸ I) x_1 = x
h :
  ∀ (y : R) (hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x),
    Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x

Tactic:
obtain ⟨y, hy⟩ := hx
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x
h : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) (0 : S)
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x

Tactic:
rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]

Premises used: RingHom.mem_ker, Ideal.Quotient.lift_mk, And.right
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) (0 : S)

Tactic:
hy.left

Premises used: Set.Mem, setOf, Set.preimage, And.left, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) (0 : S)

Tactic:
exact hy.left

Premises used: And.left