-- 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:
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 * (z * g ↑x.2 * g ↑y.2) = g b.1 * g (↑y.2 * x.1)

Tactic:
rw [hx, hb, mul_comm (g x.1), ← map_mul g]

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
hb1 : b.1 = 0
⊢ False

Tactic:
have m0 : (LocalizationMap.toMap fl) 0 = 0 := f.map_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
⊢ 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 * z * g ↑b.2 * (g ↑x.2 * g ↑y.2) = a * g ↑b.2 * (z * g ↑x.2 * g ↑y.2)

Tactic:
rw [mul_assoc a, mul_comm z, ← mul_assoc a, mul_assoc, mul_assoc z]

Result:
no goals

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
⊢ ↑1 * (↑y.2 * x.1) = ↑1 * (↑x.2 * y.1)

Tactic:
rw [OneMemClass.coe_one, one_mul, one_mul]

Result:
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
⊢ ↑y.2 * x.1 = ↑x.2 * y.1

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
⊢ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Tactic:
use 1

Result:
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
⊢ ↑1 * (↑y.2 * x.1) = ↑1 * (↑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
b1ne0 : b.1 ≠ 0
⊢ g b.1 * (g ↑x.2 * g y.1) = a * g ↑b.2 * (g ↑x.2 * (w * g ↑y.2))

Tactic:
rw [hb, hy]

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨y, hy⟩ := LocalizationMap.surj fl w

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
⊢ 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
b1ne0 : b.1 ≠ 0
⊢ g (b.1 * (↑x.2 * y.1)) = g b.1 * (g ↑x.2 * g y.1)

Tactic:
rw [map_mul g,map_mul g]

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 = 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

Tactic:
exact ha hb

Result:
no goals