awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : R
simp_rw :
  Eq.{uT + 1} (α := T)
    (((({
                  toFun :=
                    fun
                      (f :
                        { f : R →+* T //
                          ∀ ⦃x y : R⦄,
                            r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
                    {
                      toFun := fun (x : RingQuot r) ↦
                        Quot.lift (r := Rel r) (⇑(↑f : R →+* T) : (a : R) → T) ⋯ (x.toQuot (r := r)),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
                  invFun := fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
                    Subtype.mk (p := fun (f : R →+* T) ↦
                      ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
                      (F.comp
                        { toFun := fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯,
                          map_zero' := ⋯, map_add' := ⋯ })
                      ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) →
                  RingQuot r →+* T)
              (Subtype.mk (p := fun (f : R →+* T) ↦
                ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w) :
            RingHom.{uR, uT} (RingQuot r) T) :
          (a : RingQuot r) → T)
        (({ toFun := fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ } :
              (a : R) → RingQuot r)
            x :
          RingQuot r) :
      T)
    ((f : (a : R) → T) x : T)
⊢ Eq.{uT + 1} (α := T)
    ((((lift (r := r) :
                (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) →
                  RingQuot r →+* T)
              (Subtype.mk (p := fun (f : R →+* T) ↦
                ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w) :
            RingHom.{uR, uT} (RingQuot r) T) :
          (a : RingQuot r) → T)
        ((mkRingHom r : (a : R) → RingQuot r) x : RingQuot r) :
      T)
    ((f : (a : R) → T) x : T)

Tactic:
simp_rw [lift_def, preLift_def, mkRingHom_def]

Premises used: RingQuot.preLift_def, RingQuot.mkRingHom_def, RingQuot.lift_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
x : R
⊢ Eq.{uT + 1} (α := T)
    (((({
                  toFun :=
                    fun
                      (f :
                        { f : R →+* T //
                          ∀ ⦃x y : R⦄,
                            r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T) }) ↦
                    {
                      toFun := fun (x : RingQuot r) ↦
                        Quot.lift (r := Rel r) (⇑(↑f : R →+* T) : (a : R) → T) ⋯ (x.toQuot (r := r)),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
                  invFun := fun (F : RingHom.{uR, uT} (RingQuot r) T) ↦
                    Subtype.mk (p := fun (f : R →+* T) ↦
                      ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
                      (F.comp
                        { toFun := fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯,
                          map_zero' := ⋯, map_add' := ⋯ })
                      ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) →
                  RingQuot r →+* T)
              (Subtype.mk (p := fun (f : R →+* T) ↦
                ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w) :
            RingHom.{uR, uT} (RingQuot r) T) :
          (a : RingQuot r) → T)
        (({ toFun := fun (x : R) ↦ mk (r := r) (Quot.mk (Rel r) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ } :
              (a : R) → RingQuot r)
            x :
          RingQuot r) :
      T)
    ((f : (a : R) → T) x : T)

Tactic:
rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
g : RingHom.{uR, uT} (RingQuot r) T
h : g.comp (mkRingHom r) = f
w₁ :
  ∀ (x : R),
    Eq.{uT + 1} (α := T) ((g.comp (mkRingHom r) : (a : R) → T) x : T)
      ((RingHom.comp
              ((lift (r := r) :
                  (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) →
                    RingQuot r →+* T)
                (Subtype.mk (p := fun (f : R →+* T) ↦
                  ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w))
              (mkRingHom r) :
            (a : R) → T)
          x :
        T)
⊢ g =
    (lift (r := r) :
        (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) → RingQuot r →+* T)
      (Subtype.mk (p := fun (f : R →+* T) ↦
        ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w)

Tactic:
ext
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)
g : RingHom.{uR, uT} (RingQuot r) T
h : g.comp (mkRingHom r) = f
x : R
⊢ Eq.{uT + 1} (α := T) ((g.comp (mkRingHom r) : (a : R) → T) x : T)
    ((RingHom.comp
            ((lift (r := r) :
                (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) →
                  RingQuot r →+* T)
              (Subtype.mk (p := fun (f : R →+* T) ↦
                ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T)) f w))
            (mkRingHom r) :
          (a : R) → T)
        x :
      T)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
T : Type uT
inst_1 : Semiring T
r : R → R → Prop
f : RingHom.{uR, uT} (RingQuot r) T
⊢ f =
    (lift (r := r) :
        (a : { f : R →+* T // ∀ ⦃x y : R⦄, r x y → (f : (a : R) → T) x = (f : (a : R) → T) y }) → RingQuot r →+* T)
      (Subtype.mk (p := fun (f : R →+* T) ↦
        ∀ ⦃x y : R⦄, r x y → Eq.{uT + 1} (α := T) ((f : (a : R) → T) x : T) ((f : (a : R) → T) y : T))
        (f.comp (mkRingHom r)) ⋯)

Tactic:
lift_unique (f.comp (mkRingHom r)) (fun _ _ h ↦ congr_arg (⇑f) (mkRingHom_rel h)) f rfl

Premises used: RingQuot.lift_unique, congr_arg, RingHom.comp, RingQuot.mkRingHom, DFunLike.coe, rfl, RingQuot.mkRingHom_rel
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
⊢ ∀ (a : B),
    Membership.mem (γ := Ideal B) (Ideal.ofRel r) a →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r)

Tactic:
fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
refine_1 :
  ∀ (x : B) (h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x) (x : B)
    (h : Membership.mem (γ := Set B) {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a} x),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r)
refine_2 :
  ∀ (x : B) (h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) 0) 0
refine_3 :
  ∀ (x : B) (h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x) (x y : B)
    (hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) x)
    (hy : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) y),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r) →
        Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (x + y) : RingQuot r) (0 : RingQuot r)
refine_4 :
  ∀ (x : B) (h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x) (a x : B)
    (hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) x),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a • x) : RingQuot r) (0 : RingQuot r)
⊢ ∀ (a : B),
    Membership.mem (γ := Ideal B) (Ideal.ofRel r) a →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r)

Tactic:
refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h_1 : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
y a b : B
h : r a b
su : y + b = a
⊢ a = y + b

Tactic:
symm at su
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h_1 : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
y a b : B
h : r a b
su : a = y + b
⊢ a - b = y

Tactic:
rw [← sub_eq_iff_eq_add] at su

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h_1 : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
y a b : B
h : r a b
su : a - b = y
refine_1 : Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a - b) : RingQuot r) (0 : RingQuot r)
refine_1₁ :
  HSub.hSub (α := RingQuot r) (β := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r)
      ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) =
    0
refine_1₂ :
  HSub.hSub (α := RingQuot r) (β := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r)
      ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) =
    0
refine_1₃ refine_1₄ : Eq.{uR + 1} (α := RingQuot r) 0 0
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)

Tactic:
rw [← su, map_sub, mkRingHom_rel h, sub_self]

Premises used: map_sub, sub_self, RingQuot.mkRingHom_rel
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
a b : B
refine_3 :
  Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) a →
    ∀ (hy : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) b),
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r) →
        Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) (0 : RingQuot r) →
          Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a + b) : RingQuot r) (0 : RingQuot r)
⊢ ∀ (hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) a)
    (hy : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) b),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) (0 : RingQuot r) →
        Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a + b) : RingQuot r) (0 : RingQuot r)

Tactic:
_
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
a b : B
hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) a
refine_3 :
  Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) b →
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) (0 : RingQuot r) →
        Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a + b) : RingQuot r) (0 : RingQuot r)
⊢ ∀ (hy : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) b),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) (0 : RingQuot r) →
        Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a + b) : RingQuot r) (0 : RingQuot r)

Tactic:
_
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x
a b : B
hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) a
hy : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) b
ha : Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) a : RingQuot r) (0 : RingQuot r)
hb : Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) b : RingQuot r) (0 : RingQuot r)
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a + b) : RingQuot r) (0 : RingQuot r)

Tactic:
simp [ha, hb]
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x_1 : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x_1
a x : B
refine_4 :
  Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) x →
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a • x) : RingQuot r) (0 : RingQuot r)
⊢ ∀ (hx : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) x),
    Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r) →
      Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a • x) : RingQuot r) (0 : RingQuot r)

Tactic:
_
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x_1 : B
h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x_1
a x : B
hx_1 : Membership.mem (γ := Submodule B B) (Submodule.span B {x : B | ∃ (a : B) (b : B), r a b ∧ x + b = a}) x
hx : Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r) (0 : RingQuot r)
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a • x) : RingQuot r) (0 : RingQuot r)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.RingQuot
Goal:
B : Type uR
inst : CommRing B
r : B → B → Prop
x : B
⊢ Eq (α := RingQuot r)
    ((idealQuotientToRingQuot r : (a : B ⧸ Ideal.ofRel r) → RingQuot r)
        ((Ideal.Quotient.mk (Ideal.ofRel r) : (a : B) → B ⧸ Ideal.ofRel r) x) :
      RingQuot r)
    ((mkRingHom r : (a : B) → RingQuot r) x : RingQuot r)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
h :
  ∀ (x : B),
    Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
      ((RingHom.comp (RingHom.comp (ringQuotToIdealQuotient r) (idealQuotientToRingQuot r))
              (Ideal.Quotient.mk (Ideal.ofRel r)) :
            (a : B) → B ⧸ Ideal.ofRel r)
          x :
        HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
      ((RingHom.comp (RingHom.id (HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)))
              (Ideal.Quotient.mk (Ideal.ofRel r)) :
            (a : B) → B ⧸ Ideal.ofRel r)
          x :
        HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
⊢ Eq (α :=
    HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r) →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    (RingHom.comp (ringQuotToIdealQuotient r) (idealQuotientToRingQuot r))
    (RingHom.id (HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)))

Tactic:
ext x
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
⊢ Eq (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    ((RingHom.comp (RingHom.comp (ringQuotToIdealQuotient r) (idealQuotientToRingQuot r))
            (Ideal.Quotient.mk (Ideal.ofRel r)) :
          (a : B) → B ⧸ Ideal.ofRel r)
        x :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))
    ((RingHom.comp (RingHom.id (HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r)))
            (Ideal.Quotient.mk (Ideal.ofRel r)) :
          (a : B) → B ⧸ Ideal.ofRel r)
        x :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.ofRel r))

Tactic:
simp
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
w :
  ∀ (x : B),
    Eq (α := RingQuot r)
      ((RingHom.comp (RingHom.comp (idealQuotientToRingQuot r) (ringQuotToIdealQuotient r)) (mkRingHom r) :
            (a : B) → RingQuot r)
          x :
        RingQuot r)
      ((RingHom.comp (RingHom.id (RingQuot r)) (mkRingHom r) : (a : B) → RingQuot r) x : RingQuot r)
⊢ Eq (α := RingQuot r →+* RingQuot r) (RingHom.comp (idealQuotientToRingQuot r) (ringQuotToIdealQuotient r))
    (RingHom.id (RingQuot r))

Tactic:
ext x
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r_1 : R → R → Prop
inst_4 : Semiring T
B : Type uR
inst_5 : CommRing B
r : B → B → Prop
x : B
⊢ Eq (α := RingQuot r)
    ((RingHom.comp (RingHom.comp (idealQuotientToRingQuot r) (ringQuotToIdealQuotient r)) (mkRingHom r) :
          (a : B) → RingQuot r)
        x :
      RingQuot r)
    ((RingHom.comp (RingHom.id (RingQuot r)) (mkRingHom r) : (a : B) → RingQuot r) x : RingQuot r)

Tactic:
simp
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
s : A → A → Prop
x : S
simp :
  mk (r := s) (Quot.mk (Rel s) ((algebraMap S A : (a : S) → A) x)) =
    (algebraMap S (RingQuot s) : (a : S) → RingQuot s) x
⊢ Eq (α := RingQuot s)
    (OneHom.toFun (↑(↑(mkRingHom s) : A →* RingQuot s) : OneHom A (RingQuot s)) ((algebraMap S A : (a : S) → A) x))
    ((algebraMap S (RingQuot s) : (a : S) → RingQuot s) x)

Tactic:
simp [mkRingHom_def]

Premises used: RingQuot.mkRingHom_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
s : A → A → Prop
x : S
⊢ mk (r := s) (Quot.mk (Rel s) ((algebraMap S A : (a : S) → A) x)) =
    (algebraMap S (RingQuot s) : (a : S) → RingQuot s) x

Tactic:
rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
simp_rw :
  Eq (α := A →+* RingQuot s)
    (↑{ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯, commutes' := ⋯ } :
      A →+* RingQuot s)
    { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ }
⊢ (↑(mkAlgHom S s) : A →+* RingQuot s) = mkRingHom s

Tactic:
simp_rw [mkAlgHom_def, mkRingHom_def]

Premises used: RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
⊢ Eq (α := A →+* RingQuot s)
    (↑{ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯, commutes' := ⋯ } :
      A →+* RingQuot s)
    { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ }

Tactic:
rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
x y : A
w : s x y
⊢ Eq (α := RingQuot s) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s)
    ((mkAlgHom S s : (a : A) → RingQuot s) y : RingQuot s)

Tactic:
simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]

Premises used: Quot.sound, RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def, RingQuot.Rel.of
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
this : Function.Surjective (β := RingQuot s) fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)
⊢ Function.Surjective (α := A) (β := RingQuot s) (⇑(mkAlgHom S s) : (a : A) → RingQuot s)

Tactic:
simpa [mkAlgHom_def, mkRingHom_def]

Premises used: RingQuot.mkRingHom_def, RingQuot.mkAlgHom_def