awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Ring B
inst_4 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_5 : I.IsTwoSided
inst_6 : J.IsTwoSided
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ Eq.{u_4 + 1} (α := B ⧸ J)
    (((AlgHom.comp (quotientMapₐ J f H) (Quotient.mkₐ R₁ I) : AlgHom.{u_1, u_3, u_4} R₁ A (B ⧸ J)) : (a : A) → B ⧸ J)
        x :
      B ⧸ J)
    (((AlgHom.comp (Quotient.mkₐ R₁ J) f : AlgHom.{u_1, u_3, u_4} R₁ A (B ⧸ J)) : (a : A) → B ⧸ J) x : B ⧸ J)

Tactic:
simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]

Premises used: AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk, Ideal.quotient_map_mkₐ
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
inst_7 : Ring B
inst_8 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_9 : I.IsTwoSided
inst_10 : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (F := A →+* B) (↑f : A →+* B) I
⊢ I = map (F := B →+* A) (↑f.symm : B →+* A) J

Tactic:
simp only [← AlgEquiv.toAlgHom_toRingHom, hIJ, map_map, ← AlgHom.comp_toRingHom,
        AlgEquiv.symm_comp, AlgHom.id_toRingHom, map_id]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_toRingHom, Ideal.map_id, AlgEquiv.symm_comp, Ideal.map_map, AlgHom.id_toRingHom
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Ring B
inst_4 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_5 : I.IsTwoSided
inst_6 : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (F := A →+* B) (↑f : A →+* B) I
⊢ Eq (α := AlgEquiv.{u_1, u_4, u_3} R₁ (B ⧸ J) (A ⧸ I)) (AlgEquiv.symm (I.quotientEquivAlg J f hIJ))
    (J.quotientEquivAlg I f.symm ⋯)

Tactic:
rfl

Premises used: AlgEquiv.symm, Quotient.liftOn', AddCon.liftOn, Submodule.quotientRel, AddAction.orbitRel, Equiv.symm, AddCon.Quotient, Ideal.quotientEquivAlg, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Ring B
inst_4 : Algebra R₁ B
I : Ideal A
J : Ideal B
inst_5 : I.IsTwoSided
inst_6 : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (F := A →+* B) (↑f : A →+* B) I
x : A
⊢ Eq.{u_4 + 1} (α := B ⧸ J)
    (((I.quotientEquivAlg J f hIJ : AlgEquiv.{u_1, u_3, u_4} R₁ (A ⧸ I) (B ⧸ J)) : (a : A ⧸ I) → B ⧸ J)
        ((Quotient.mk I : (a : A) → A ⧸ I) x) :
      B ⧸ J)
    ((Quotient.mk J : (a : B) → B ⧸ J) ((f : (a : A) → B) x) : B ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
⊢ Membership.mem (γ := Submodule R R) (comap (F := R →+* A) (algebraMap R A) P) (r₁ - r₂)

Tactic:
have := h (p.quotientRel_def.mp hr)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : Membership.mem (γ := Submodule R R) (comap (F := R →+* A) (algebraMap R A) P) (r₁ - r₂)
⊢ HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) r₁ : A) ((algebraMap R A : (a : R) → A) r₂ : A) ∈ P

Tactic:
rw [mem_comap, map_sub] at this

Premises used: map_sub, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : HSub.hSub (α := A) (β := A) ((algebraMap R A : (a : R) → A) r₁ : A) ((algebraMap R A : (a : R) → A) r₂ : A) ∈ P
⊢ r₁ • a₁ ≈ r₂ • a₂

Tactic:
simpa only [Algebra.smul_def] using P.quotientRel_def.mpr
      (P.mul_sub_mul_mem this <| P.quotientRel_def.mp ha)

Premises used: Submodule.quotientRel_def, Iff.mpr, Iff.mp, Algebra.smul_def, Ideal.mul_sub_mul_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r : R ⧸ p
a : R
x : A ⧸ P
a_1 : A
⊢ HMul.hMul (α := A ⧸ P) (β := A ⧸ P)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1) =
    HMul.hMul (α := A ⧸ P) (β := A ⧸ P) (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)

Tactic:
congr_arg (⟦·⟧) (Algebra.commutes _ _)

Premises used: Quotient.map₂, Quotient.mk, congr_arg, Submodule.quotientRel, AddAction.orbitRel, Algebra.commutes
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r : R ⧸ p
a : R
x : A ⧸ P
a_1 : A
⊢ HMul.hMul (α := A ⧸ P) (β := A ⧸ P)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1) =
    HMul.hMul (α := A ⧸ P) (β := A ⧸ P) (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)

Tactic:
exact congr_arg (⟦·⟧) (Algebra.commutes _ _)

Premises used: Quotient.mk, congr_arg, Algebra.commutes
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r : R ⧸ p
a : R
x : A ⧸ P
a_1 : A
⊢ HSMul.hSMul (α := R ⧸ p) (β := A ⧸ P) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1) =
    HMul.hMul (α := A ⧸ P) (β := A ⧸ P)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1)

Tactic:
congr_arg (⟦·⟧) (Algebra.smul_def _ _)

Premises used: Quotient.map₂, Quotient.mk, congr_arg, Algebra.smul_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
R : Type u_5
inst_7 : CommRing R
inst_8 : Algebra R A
p : Ideal R
P : Ideal A
inst_9 : P.IsTwoSided
h : p ≤ comap (F := R →+* A) (algebraMap R A) P
r : R ⧸ p
a : R
x : A ⧸ P
a_1 : A
⊢ HSMul.hSMul (α := R ⧸ p) (β := A ⧸ P) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1) =
    HMul.hMul (α := A ⧸ P) (β := A ⧸ P)
      (((quotientMap P (algebraMap R A) h : RingHom.{u_5, u_3} (R ⧸ p) (A ⧸ P)) : (a : R ⧸ p) → A ⧸ P)
          (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) a) :
        A ⧸ P)
      (Quot.mk (⇑(Submodule.quotientRel P) : A → A → Prop) a_1)

Tactic:
exact congr_arg (⟦·⟧) (Algebra.smul_def _ _)

Premises used: Quotient.mk, congr_arg, Algebra.smul_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab :
  Eq.{u_3 + 1} (α := A ⧸ I)
    ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)) (A ⧸ I) :
          (a : R ⧸ comap (algebraMap R A) I) → A ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a) :
      A ⧸ I)
    ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)) (A ⧸ I) :
          (a : R ⧸ comap (algebraMap R A) I) → A ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b) :
      A ⧸ I)
⊢ HSub.hSub (α := A) (β := A) (((algebraMap R A : R →+* A) : (a : R) → A) a : A)
      (((algebraMap R A : R →+* A) : (a : R) → A) b : A) ∈
    I

Tactic:
replace hab := Quotient.eq.mp hab
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab :
  HSub.hSub (α := A) (β := A) (((algebraMap R A : R →+* A) : (a : R) → A) a : A)
      (((algebraMap R A : R →+* A) : (a : R) → A) b : A) ∈
    I
⊢ Membership.mem (α := A) I (((algebraMap R A : R →+* A) : (a : R) → A) (a - b) : A)

Tactic:
rw [← map_sub] at hab

Premises used: map_sub
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab : Membership.mem (α := A) I (((algebraMap R A : R →+* A) : (a : R) → A) (a - b) : A)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I))
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a)
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b)

Tactic:
Quotient.eq.mpr hab

Premises used: Iff.mpr, Submodule.Quotient.mk, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
R : Type u_5
inst_1 : CommRing R
I : Ideal A
inst_2 : I.IsTwoSided
inst_3 : Algebra R A
a₁ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
a : R
a₂ : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I)
b : R
hab : Membership.mem (α := A) I (((algebraMap R A : R →+* A) : (a : R) → A) (a - b) : A)
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* A) (algebraMap R A) I))
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) a)
    (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I)) : R → R → Prop) b)

Tactic:
exact Quotient.eq.mpr hab

Premises used: Iff.mpr, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
h : I = J
x : A
⊢ Eq (α := A ⧸ J) ((quotientEquivAlgOfEq R₁ h : (a : A ⧸ I) → A ⧸ J) ((Quotient.mk I : (a : A) → A ⧸ I) x) : A ⧸ J)
    ((Quotient.mk J : (a : A) → A ⧸ J) x : A ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
h : I = J
⊢ Eq (α := A ⧸ I →ₐ[R₁] A ⧸ J) (↑(quotientEquivAlgOfEq R₁ h) : A ⧸ I →ₐ[R₁] A ⧸ J) (Quotient.factorₐ R₁ ⋯)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Ideal.Quotient.factor, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Quotient.factorₐ, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
h : I = J
⊢ Eq (α := A ⧸ I →+* A ⧸ J) (↑(quotientEquivAlgOfEq R₁ h) : A ⧸ I →+* A ⧸ J) (Quotient.factor ⋯)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.Quotient.factor, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
h : I = J
h₁ :
  ∀ (a : A ⧸ J),
    Eq (α := A ⧸ I) ((AlgEquiv.symm (quotientEquivAlgOfEq R₁ h) : (a : A ⧸ J) → A ⧸ I) a : A ⧸ I)
      ((quotientEquivAlgOfEq R₁ ⋯ : (a : A ⧸ J) → A ⧸ I) a : A ⧸ I)
⊢ Eq (α := (A ⧸ J) ≃ₐ[R₁] A ⧸ I) (AlgEquiv.symm (quotientEquivAlgOfEq R₁ h)) (quotientEquivAlgOfEq R₁ ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
h : I = J
a : A ⧸ J
⊢ Eq (α := A ⧸ I) ((AlgEquiv.symm (quotientEquivAlgOfEq R₁ h) : (a : A ⧸ J) → A ⧸ I) a : A ⧸ I)
    ((quotientEquivAlgOfEq R₁ ⋯ : (a : A ⧸ J) → A ⧸ I) a : A ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
        x ↔
      x ∈ I ⊔ J
⊢ comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J) = I ⊔ J

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      x ↔
    x ∈ I ⊔ J

Tactic:
simp only [mem_comap, mem_quotient_iff_mem_sup, sup_comm]

Premises used: sup_comm, Ideal.mem_quotient_iff_mem_sup, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
h : I ≤ J
⊢ comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J) = J

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
p : Ideal R
inst_2 : p.IsPrime
hIP : I ≤ p
hf : Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
hk : ker (F := R →+* R ⧸ I) (Quotient.mk I) ≤ p
⊢ IsPrime (α := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p)

Tactic:
apply Ideal.map_isPrime_of_surjective

Premises used: Ideal.map_isPrime_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
p : Ideal R
inst_2 : p.IsPrime
hIP : I ≤ p
⊢ Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)

Tactic:
Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
p : Ideal R
inst_2 : p.IsPrime
hIP : I ≤ p
⊢ Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)

Tactic:
exact Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
p : Ideal R
inst_2 : p.IsPrime
hIP : I ≤ p
⊢ ker (F := R →+* R ⧸ I) (Quotient.mk I) ≤ p

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ (quotientBot R : (a : R ⧸ ⊥) → R)
      ((Ideal.Quotient.mk ⊥ : (a : R) → R ⧸ ⊥) r : HasQuotient.Quotient R (B := Ideal R) ⊥) =
    r

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) ⊥)
    ((RingEquiv.symm (quotientBot R) : (a : R) → R ⧸ ⊥) r : HasQuotient.Quotient R (B := Ideal R) ⊥)
    ((Ideal.Quotient.mk ⊥ : (a : R) → R ⧸ ⊥) r : HasQuotient.Quotient R (B := Ideal R) ⊥)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Algebra R S
x : R
⊢ Equiv.toFun (α := HasQuotient.Quotient S (B := Ideal S) ⊥) (RingEquiv.toEquiv (RingEquiv.quotientBot S))
      ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) ⊥) : (a : R) → S ⧸ ⊥) x) =
    (algebraMap R S : (a : R) → S) x

Tactic:
simp [← Ideal.Quotient.mk_algebraMap]

Premises used: Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ (quotientBot R S : (a : S ⧸ ⊥) → S)
      ((Ideal.Quotient.mk ⊥ : (a : S) → S ⧸ ⊥) s : HasQuotient.Quotient S (B := Ideal S) ⊥) =
    s

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) ⊥)
    ((symm (quotientBot R S) : (a : S) → S ⧸ ⊥) s : HasQuotient.Quotient S (B := Ideal S) ⊥)
    ((Ideal.Quotient.mk ⊥ : (a : S) → S ⧸ ⊥) s : HasQuotient.Quotient S (B := Ideal S) ⊥)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
⊢ Eq (α := Ideal (R ⧸ I)) (RingHom.ker (quotLeftToQuotSup I J)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)

Tactic:
simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
    map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]

Premises used: Ideal.Quotient.mk, sup_idem, sup_assoc, Ideal.ker_quotient_lift, sup_comm, Ideal.map_eq_iff_sup_ker_eq_of_surjective, Ideal.Quotient.factor, DoubleQuot.quotLeftToQuotSup, Quotient.mk_surjective, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
rw : comap (quotQuotMk I J) ⊥ = I ⊔ J
rw₁ :
  comap (F := R →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
      (RingHom.comp (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)) (Ideal.Quotient.mk I)) ⊥ =
    I ⊔ J
rw₂ :
  comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
      (comap (F :=
        R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)) ⊥) =
    I ⊔ J
rw₃ :
  comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
      (RingHom.ker (F :=
        R ⧸ I →+* HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))) =
    I ⊔ J
rw₄ : comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J) = I ⊔ J
rw₅ : J ⊔ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) ⊥ = I ⊔ J
rw₆ : J ⊔ RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) = I ⊔ J
rw₇ : J ⊔ I = I ⊔ J
rw₈ rw₉ : I ⊔ J = I ⊔ J
⊢ RingHom.ker (quotQuotMk I J) = I ⊔ J

Tactic:
rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
    comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ← RingHom.ker,
    mk_ker, sup_comm]

Premises used: Ideal.Quotient.mk, DoubleQuot.quotQuotMk, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, sup_comm, RingHom.ker_eq_comap_bot, Ideal.mk_ker, RingHom.ker, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h :
  ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
⊢ (quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)

Tactic:
apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h :
  ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
⊢ (quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)

Tactic:
repeat apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
⊢ ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
h :
  ((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp
      (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)) =
    RingHom.comp
      (RingHom.id (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))
⊢ (liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J) =
    RingHom.id (HasQuotient.Quotient (R ⧸ I) (B := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J))

Tactic:
apply Ideal.Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext