awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
⊢ a = default
have change : a = mk 1 1
Tactic: change a = mk 1 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
⊢ a = default
have with_unfolding_all : a = mk 1 1
Tactic: with_unfolding_all change a = mk 1 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
x : R × ↥M
⊢ Eq (α := Localization (M := R) M) (mk x.1 x.2) (mk 1 1)
have e_x : x.1 = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
x : R × ↥M
e_x : x.1 = 1
⊢ Eq (α := Localization (M := R) M) (mk x.1 x.2) (mk 1 1)
have e_y : x.2 = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑b : R) * c + (↑d : R) * a) (b * d)
have rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a + (↑b : R) * c) (d * b)
Tactic: rw [add_comm (b * c) (d * a), mul_comm b d]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c b) = mk (a + c) b
have rw : ((r'.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) ((↑b : R) * c + (↑b : R) * a, b * b) (a + c, b)
Tactic: rw [add_mk, mk_eq_mk_iff, r_eq_r']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ ((r'.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) ((↑b : R) * c + (↑b : R) * a, b * b) (a + c, b)
have refine : (↑1 : R) * ((↑((↑b : R) * c + (↑b : R) * a, b * b).2 : R) * (a + c, b).1) =
  (↑1 : R) * ((↑(a + c, b).2 : R) * ((↑b : R) * c + (↑b : R) * a, b * b).1)
Tactic: refine (r' M).symm ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (↑1 : R) * ((↑((↑b : R) * c + (↑b : R) * a, b * b).2 : R) * (a + c, b).1) =
    (↑1 : R) * ((↑(a + c, b).2 : R) * ((↑b : R) * c + (↑b : R) * a, b * b).1)
have simp : 1 * ((↑b : R) * (↑b : R) * (a + c)) = 1 * ((↑b : R) * ((↑b : R) * c + (↑b : R) * a))
Tactic: simp only [Submonoid.coe_one, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ Eq (α := Localization (M := R) M) (mk x y) (mk' (Localization (M := R) M) x y)
have rw : Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y) (mk' (Localization (M := R) M) x y)
Tactic: rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
y : ↥M
rw :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y) (mk' (Localization (M := R) M) x y)
⊢ Eq (α := Localization (M := R) M) (mk x y) (mk' (Localization (M := R) M) x y)
have rw₁ : Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
  (Submonoid.LocalizationMap.mk' (toLocalizationMap M (Localization (M := R) M)) x y)
Tactic: rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
y : ↥M
rw :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y) (mk' (Localization (M := R) M) x y)
rw₁ :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
    (Submonoid.LocalizationMap.mk' (toLocalizationMap M (Localization (M := R) M)) x y)
⊢ Eq (α := Localization (M := R) M) (mk x y) (mk' (Localization (M := R) M) x y)
have rw₂ : Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
  (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
Tactic: rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
m : A
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M) (mk ((algebraMap A R : (a : A) → R) m) 1 : Localization (M := R) M)
    ((algebraMap A (Localization (M := R) M) : (a : A) → Localization M) m : Localization (M := R) M)
have rw : Eq (α := Localization (M := R) M)
  ((algebraMap R (Localization (M := R) M) : (a : R) → Localization M) ((algebraMap A R : (a : A) → R) m) :
    Localization (M := R) M)
  ((algebraMap A (Localization (M := R) M) : (a : A) → Localization M) m : Localization (M := R) M)
Tactic: rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) ↔ x = 0
have mp : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
mp : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) → x = 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) ↔ x = 0
have mpr : x = 0 → Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ x = 0
have mp : ∀ (c : ↥M) (hc : (↑c : R) * x = 0), x = 0
Tactic: obtain ⟨c, hc⟩ := (map_eq_zero_iff M _ _).mp h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
have mpr : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
mpr : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
have mpr₁ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
have rw : ¬x = 0
Tactic: rw [Ne, to_map_eq_zero_iff S hM]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw₂ : Eq (α := Localization (M := R) M) (mk ((↑b : R) * -c + (↑d : R) * a) (b * d)) (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₂ :
  Eq (α := Localization (M := R) M) (mk ((↑b : R) * -c + (↑d : R) * a) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw₃ : Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + (↑b : R) * -c) (b * d)) (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₂ :
  Eq (α := Localization (M := R) M) (mk ((↑b : R) * -c + (↑d : R) * a) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₃ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + (↑b : R) * -c) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw₄ : Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + -((↑b : R) * c)) (b * d))
  (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₂ :
  Eq (α := Localization (M := R) M) (mk ((↑b : R) * -c + (↑d : R) * a) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₃ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + (↑b : R) * -c) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₄ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + -((↑b : R) * c)) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
have rw₅ : Eq (α := Localization (M := R) M) (mk ((↑d : R) * a - (↑b : R) * c) (b * d)) (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
Tactic: rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ mk' S (-x) y = -mk' S x y
have rw : -mk' S x y = mk' S (-x) y
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
rw : -mk' S x y = mk' S (-x) y
⊢ mk' S (-x) y = -mk' S x y
have rw₁ : HMul.hMul (β := S) (-mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
rw : -mk' S x y = mk' S (-x) y
rw₁ :
  HMul.hMul (β := S) (-mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
⊢ mk' S (-x) y = -mk' S x y
have rw₂ : -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
rw : -mk' S x y = mk' S (-x) y
rw₁ :
  HMul.hMul (β := S) (-mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
rw₂ :
  -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
⊢ mk' S (-x) y = -mk' S x y
have rw₃ : -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = -(algebraMap R S : (a : R) → S) x
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
rw : -mk' S x y = mk' S (-x) y
rw₁ :
  HMul.hMul (β := S) (-mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
rw₂ :
  -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
rw₃ : -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = -(algebraMap R S : (a : R) → S) x
⊢ mk' S (-x) y = -mk' S x y
have rw₄ : Eq.{u_2 + 1} (α := S) (-(algebraMap R S : (a : R) → S) x : S) (-(algebraMap R S : (a : R) → S) x : S)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
have rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
have rw₁ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
rw₁ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
have rw₂ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + mk' S (-x₂) y₂
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
rw₁ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
rw₂ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + mk' S (-x₂) y₂
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
have rw₃ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S (x₁ * (↑y₂ : R) + -x₂ * (↑y₁ : R)) (y₁ * y₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
rw₁ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
rw₂ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + mk' S (-x₂) y₂
rw₃ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S (x₁ * (↑y₂ : R) + -x₂ * (↑y₁ : R)) (y₁ * y₂)
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
have rw₄ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
have rw : ∀ (x y : R),
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
      ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
Tactic: rw [IsLocalization.injective_iff_map_algebraMap_eq M]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
have refine : ∀ (x y : R)
  (hz :
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
      ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)),
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
Tactic: refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz :
  Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
    ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
have hz₁ : Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) (x - y) : S) : T) (0 : T)
Tactic: rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz : Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) (x - y) : S) : T) (0 : T)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
have hz₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x - y) : S) (0 : S)
Tactic: apply h at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x - y) : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
have rwa : ∀ (hz : HSub.hSub (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) = 0),
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
Tactic: rwa [map_sub, sub_eq_zero] at hz
Cleared hypotheses: hz