awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
    ((((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)
have 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) sorry (x.toQuot (r := r)),
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry },
                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' := sorry, map_mul' := sorry,
                        map_zero' := sorry, map_add' := sorry })
                    sorry,
                left_inv := sorry, right_inv := sorry } :
              (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' := sorry, map_mul' := sorry, map_zero' := sorry,
              map_add' := sorry } :
            (a : R) → RingQuot r)
          x :
        RingQuot r) :
    T)
  ((f : (a : R) → T) x : T)
Tactic: simp_rw [lift_def, preLift_def, mkRingHom_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
have 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)
Tactic: refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ ∀ (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)
have refine_2 : ∀ (x : B) (h : Membership.mem (γ := Ideal B) (Ideal.ofRel r) x),
  Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) 0) 0
Tactic: refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ ∀ (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)
have 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)
Tactic: refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ ∀ (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)
have 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)
Tactic: refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (hypothesis)
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
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have su₁ : a = y + b
Tactic: symm at su
Cleared hypotheses: su
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (hypothesis)
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
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have su₁ : a - b = y
Tactic: rw [← sub_eq_iff_eq_add] at su
Cleared hypotheses: su
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have refine_1 : Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) (a - b) : RingQuot r) (0 : RingQuot r)
Tactic: rw [← su, map_sub, mkRingHom_rel h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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)
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have 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
Tactic: rw [← su, map_sub, mkRingHom_rel h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have 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
Tactic: rw [← su, map_sub, mkRingHom_rel h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ Eq (α := RingQuot r) ((mkRingHom r : (a : B) → RingQuot r) y : RingQuot r) (0 : RingQuot r)
have refine_1₃ : Eq.{uR + 1} (α := RingQuot r) 0 0
Tactic: rw [← su, map_sub, mkRingHom_rel h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ 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)))
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ Eq (α := RingQuot r →+* RingQuot r) (RingHom.comp (idealQuotientToRingQuot r) (ringQuotToIdealQuotient r))
    (RingHom.id (RingQuot r))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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
⊢ 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)
have simp : mk (r := s) (Quot.mk (Rel s) ((algebraMap S A : (a : S) → A) x)) = (algebraMap S (RingQuot s) : (a : S) → RingQuot s) x
Tactic: simp [mkRingHom_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
⊢ (↑(mkAlgHom S s) : A →+* RingQuot s) = mkRingHom s
have simp_rw : Eq (α := A →+* RingQuot s)
  (↑{ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := sorry, map_mul' := sorry, map_zero' := sorry,
        map_add' := sorry, commutes' := sorry } :
    A →+* RingQuot s)
  { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := sorry, map_mul' := sorry, map_zero' := sorry,
    map_add' := sorry }
Tactic: simp_rw [mkAlgHom_def, mkRingHom_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
⊢ Function.Surjective (α := A) (β := RingQuot s) (⇑(mkAlgHom S s) : (a : A) → RingQuot s)
have suffices : Function.Surjective (β := RingQuot s) fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)
Tactic: suffices Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) by
    simpa [mkAlgHom_def, mkRingHom_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
s : A → A → Prop
toQuot : Quot (Rel s)
a w : A
⊢ ∃ (a_1 : A), (fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)) a_1 = mk (r := s) (Quot.mk (Rel s) a)
have h : (fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x)) a = mk (r := s) (Quot.mk (Rel s) a)
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
⊢ f = g
have H : ∀ (x : RingQuot s), Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) x : B) ((g : (a : RingQuot s) → B) x : B)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
s : A → A → Prop
f g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : RingQuot s
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) x : B) ((g : (a : RingQuot s) → B) x : B)
have H : ∀ (x : A),
  Eq.{u₄ + 1} (α := B) ((f : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
    ((g : (a : RingQuot s) → B) ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) : B)
Tactic: rcases mkAlgHom_surjective S s x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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 u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b : A
r : Rel s a b
of : ∀ ⦃x y : A⦄ (r : s x y), Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)
have add_left : ∀ ⦃a b c : A⦄,
  Rel s a b →
    ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
      Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a + c) : B) ((f : (a : A) → B) (b + c) : B)
Tactic: induction r with
              | of r => exact h r
              | add_left _ r' => simp only [map_add, r']
              | mul_left _ r' => simp only [map_mul, r']
              | mul_right _ r' => simp only [map_mul, r']
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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 u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b : A
r : Rel s a b
of : ∀ ⦃x y : A⦄ (r : s x y), Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
add_left :
  ∀ ⦃a b c : A⦄,
    Rel s a b →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a + c) : B) ((f : (a : A) → B) (b + c) : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)
have mul_left : ∀ ⦃a b c : A⦄,
  Rel s a b →
    ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
      Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a * c) : B) ((f : (a : A) → B) (b * c) : B)
Tactic: induction r with
              | of r => exact h r
              | add_left _ r' => simp only [map_add, r']
              | mul_left _ r' => simp only [map_mul, r']
              | mul_right _ r' => simp only [map_mul, r']
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
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 u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : RingQuot s
a b : A
r : Rel s a b
of : ∀ ⦃x y : A⦄ (r : s x y), Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
add_left :
  ∀ ⦃a b c : A⦄,
    Rel s a b →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a + c) : B) ((f : (a : A) → B) (b + c) : B)
mul_left :
  ∀ ⦃a b c : A⦄,
    Rel s a b →
      ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)),
        Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a * c) : B) ((f : (a : A) → B) (b * c) : B)
⊢ Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)
have mul_right : ∀ ⦃a b c : A⦄,
  Rel s b c →
    ∀ (r' : Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) b : B) ((f : (a : A) → B) c : B)),
      Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) (a * b) : B) ((f : (a : A) → B) (a * c) : B)
Tactic: induction r with
              | of r => exact h r
              | add_left _ r' => simp only [map_add, r']
              | mul_left _ r' => simp only [map_mul, r']
              | mul_right _ r' => simp only [map_mul, r']
Cleared hypotheses: r