-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem leftCancelMulZero_of_le_isLeftRegular
    (f : LocalizationWithZeroMap S N) [IsLeftCancelMulZero M]
    (h : ∀ ⦃x⦄, x ∈ S → IsLeftRegular x) : IsLeftCancelMulZero N

Proof state:
case h
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
b1ne0 : b.1 ≠ 0
main : g (b.1 * (↑x.2 * y.1)) = g (b.1 * (↑y.2 * x.1))
⊢ ↑y.2 * x.1 = ↑x.2 * y.1

Tactic:
exact (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero b1ne0
    ((LocalizationMap.toMap_injective_iff fl).mpr h main)).symm

Result:
no goals

Proof state:
case mul_left_cancel_of_ne_zero.intro.intro.intro
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
⊢ z = w

Tactic:
rw [(LocalizationMap.eq_mk'_iff_mul_eq fl).mpr hx,
  (LocalizationMap.eq_mk'_iff_mul_eq fl).mpr hy, LocalizationMap.eq]

Result:
case mul_left_cancel_of_ne_zero.intro.intro.intro
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
⊢ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
hb1 : b.1 = 0
m0 : fl.toMap 0 = 0
⊢ False

Tactic:
have a0 : a * (LocalizationMap.toMap fl) b.2 = 0 ↔ a = 0 :=
  (f.toLocalizationMap.map_units' b.2).mul_left_eq_zero

Result:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
hb1 : b.1 = 0
m0 : fl.toMap 0 = 0
a0 : a * fl.toMap ↑b.2 = 0 ↔ a = 0
⊢ False

Proof state:
case mul_left_cancel_of_ne_zero.intro
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
⊢ z = w

Tactic:
obtain ⟨x, hx⟩ := LocalizationMap.surj fl z

Result:
case mul_left_cancel_of_ne_zero.intro.intro
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
⊢ z = w

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
⊢ b.1 ≠ 0

Tactic:
intro hb1

Result:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
hb1 : b.1 = 0
⊢ False

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
hb1 : b.1 = 0
m0 : fl.toMap 0 = 0
a0 : a * fl.toMap ↑b.2 = 0 ↔ a = 0
⊢ False

Tactic:
rw [hb1, m0, a0] at hb

Result:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a = 0
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
hb1 : b.1 = 0
m0 : fl.toMap 0 = 0
a0 : a * fl.toMap ↑b.2 = 0 ↔ a = 0
⊢ False

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
b1ne0 : b.1 ≠ 0
⊢ a * w * g ↑b.2 * (g ↑x.2 * g ↑y.2) = a * z * g ↑b.2 * (g ↑x.2 * g ↑y.2)

Tactic:
rw [hazw]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationWithZeroMap N
inst✝ : IsLeftCancelMulZero M
h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
fl : S.LocalizationMap N := f.toLocalizationMap
g : M →* N := f.toMap
a z w : N
ha : a ≠ 0
hazw : a * z = a * w
b : M × ↥S
hb : a * fl.toMap ↑b.2 = fl.toMap b.1
x : M × ↥S
hx : z * fl.toMap ↑x.2 = fl.toMap x.1
y : M × ↥S
hy : w * fl.toMap ↑y.2 = fl.toMap y.1
b1ne0 : b.1 ≠ 0
⊢ a * g ↑b.2 * (g ↑x.2 * (w * g ↑y.2)) = a * w * g ↑b.2 * (g ↑x.2 * g ↑y.2)

Tactic:
rw [← mul_assoc, ← mul_assoc _ w, mul_comm _ w, mul_assoc w, mul_assoc,
  ← mul_assoc w, ← mul_assoc w, mul_comm w]

Result:
no goals