awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
empty : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
insert :
  ∀ (a : ι) (s_1 : Finset ι),
    a ∉ s_1 →
      Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i)) →
        Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ Insert.insert a s_1, mk (f i) (s i))
          (mk (∏ i ∈ Insert.insert a s_1, f i) (∏ i ∈ Insert.insert a s_1, s i))
empty₁ : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
insert₁ :
  ∀ (a : ι) (s_1 : Finset ι),
    a ∉ s_1 →
      Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i)) →
        Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ Insert.insert a s_1, mk (f i) (s i))
          (mk (∏ i ∈ Insert.insert a s_1, f i) (∏ i ∈ Insert.insert a s_1, s i))
empty₂ : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
insert₂ :
  ∀ (a : ι) (s_1 : Finset ι),
    a ∉ s_1 →
      Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i)) →
        Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ Insert.insert a s_1, mk (f i) (s i))
          (mk (∏ i ∈ Insert.insert a s_1, f i) (∏ i ∈ Insert.insert a s_1, s i))
empty₃ : Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ ∅, mk (f i) (s i)) (mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i))
insert₃ :
  ∀ (a : ι) (s_1 : Finset ι),
    a ∉ s_1 →
      Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ s_1, mk (f i) (s i)) (mk (∏ i ∈ s_1, f i) (∏ i ∈ s_1, s i)) →
        Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ Insert.insert a s_1, mk (f i) (s i))
          (mk (∏ i ∈ Insert.insert a s_1, f i) (∏ i ∈ Insert.insert a s_1, s i))
⊢ Eq.{u_1 + 1} (α := Localization S) (∏ i ∈ t, mk (f i) (s i)) (mk (∏ i ∈ t, f i) (∏ i ∈ t, s i))

Tactic:
classical
  induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

Premises used: Finset.prod_insert, Localization.mk_one, Localization.mk_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H :
  ∀ {a c : M} {b d : ↥S} (h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)),
    Eq.ndrec (motive := fun (x : Localization S) ↦ p x) (f a b) ⋯ = f c d
a : M
b : ↥S
⊢ rec (p := fun (x : Localization S) ↦ p x) f (@H) (mk a b) = f a b

Tactic:
rfl

Premises used: Localization.mk, Localization.rec, Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
p : Sort u
x : Localization S
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
a c : M
b d : ↥S
h : (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d)
⊢ Eq.ndrec (motive := fun (x : Localization S) ↦ p) (f a b) ⋯ = f c d

Tactic:
simpa only [eq_rec_constant] using H h

Premises used: eq_rec_constant
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ (mk a b).liftOn f @H = f a b

Tactic:
rfl

Premises used: Localization.mk, Localization.rec, Quotient.mk', Localization.liftOn, OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Localization S → Prop
H : ∀ (y : M × ↥S), p (mk y.1 y.2)
x : Localization S
⊢ p x

Tactic:
rec (fun a b ↦ H (a, b)) (fun _ ↦ rfl) x

Premises used: Localization.rec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Localization S → Prop
x : Localization S
H : ∀ (y : M × ↥S), p (mk y.1 y.2)
⊢ p x

Tactic:
ind H x

Premises used: Localization.ind
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S : (a : M × ↥S) → M × ↥S → Prop) (a, b) (a', b') →
      (r S : (a : M × ↥S) → M × ↥S → Prop) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ (mk a b).liftOn₂ (mk c d) f @H = f a b c d

Tactic:
rfl

Premises used: Localization.mk, Localization.rec, Localization.liftOn₂, Quotient.mk', Localization.liftOn, OreLocalization.oreDiv, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Localization S → Localization S → Prop
x y : Localization S
H : ∀ (x y : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2)
⊢ p x y

Tactic:
induction_on x fun x ↦ induction_on y <| H x

Premises used: Localization.induction_on
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
p : Localization S → Localization S → Localization S → Prop
x y z : Localization S
H : ∀ (x y z : M × ↥S), p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)
⊢ p x y z

Tactic:
induction_on₂ x y fun x y ↦ induction_on z <| H x y

Premises used: Localization.induction_on₂
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
y : ↥S
⊢ (r S : (a : M × ↥S) → M × ↥S → Prop) 1 ((↑y : M), y)

Tactic:
fun _ hb ↦ hb y
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
x y : M × ↥S
h : (↑y.2 : M) * x.1 = (↑x.2 : M) * y.1
rw rw₁ : (↑1 : M) * ((↑x.2 : M) * y.1) = (↑1 : M) * ((↑x.2 : M) * y.1)
⊢ (↑1 : M) * ((↑y.2 : M) * x.1) = (↑1 : M) * ((↑x.2 : M) * y.1)

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
symm : 1 = mk (↑a : M) a
⊢ mk (↑a : M) a = 1

Tactic:
symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
rw : (r S : (a : M × ↥S) → M × ↥S → Prop) (1, 1) ((↑a : M), a)
⊢ 1 = mk (↑a : M) a

Tactic:
rw [← mk_one, mk_eq_mk_iff]

Premises used: Localization.mk_one, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S : (a : M × ↥S) → M × ↥S → Prop) (1, 1) ((↑a : M), a)

Tactic:
one_rel a

Premises used: Localization.one_rel
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S : (a : M × ↥S) → M × ↥S → Prop) (1, 1) ((↑a : M), a)

Tactic:
exact one_rel a

Premises used: Localization.one_rel
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
a : M
haS : a ∈ S
⊢ mk a (Subtype.mk (p := fun (x : M) ↦ x ∈ S) a haS) = 1

Tactic:
mk_self ⟨a, haS⟩

Premises used: Subtype.mk, Localization.mk_self
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Localization S
x : M
y : ↥S
⊢ ∃ (a : M × ↥S),
    Eq (α := Localization S) ((mkHom : (a : M × ↥S) → Localization S) a : Localization S)
      (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (x, y) :
        Quot (α := M × ↥S) (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop))

Tactic:
⟨⟨x, y⟩, rfl⟩

Premises used: Prod.mk, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
b : Localization S
x : M
y : ↥S
⊢ ∃ (a : M × ↥S),
    Eq (α := Localization S) ((mkHom : (a : M × ↥S) → Localization S) a : Localization S)
      (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (x, y) :
        Quot (α := M × ↥S) (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop))

Tactic:
exact ⟨⟨x, y⟩, rfl⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
rw :
  Eq (α := Localization S)
    (OreLocalization.oreNum (HSMul.hSMul (β := M) c 1) b • a /ₒ
      (OreLocalization.oreDenom (HSMul.hSMul (β := M) c 1) b * 1))
    (c • a /ₒ b)
⊢ c • mk a b = mk (c • a) b

Tactic:
rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]

Premises used: Localization.mk, OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
change : Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)
⊢ Eq (α := Localization S)
    (OreLocalization.oreNum (HSMul.hSMul (β := M) c 1) b • a /ₒ
      (OreLocalization.oreDenom (HSMul.hSMul (β := M) c 1) b * 1))
    (c • a /ₒ b)

Tactic:
change (c • 1) • a /ₒ (b * 1) = _

Premises used: HMul.hMul, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
R : Type u_4
inst_1 : SMul R M
inst_2 : IsScalarTower R M M
c : R
a : M
b : ↥S
rw : Eq (α := OreLocalization S M) (c • HSMul.hSMul (α := M) 1 a /ₒ (b * 1)) (c • a /ₒ b)
rw₁ : Eq (α := OreLocalization S M) (c • a /ₒ (b * 1)) (c • a /ₒ b)
rw₂ rw₃ : Eq (α := OreLocalization S M) (c • a /ₒ b) (c • a /ₒ b)
⊢ Eq (α := OreLocalization S M) (HSMul.hSMul (β := M) c 1 • a /ₒ (b * 1)) (c • a /ₒ b)

Tactic:
rw [smul_assoc, one_smul, mul_one]

Premises used: smul_assoc, one_smul, mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑1 : M) : N) ((f : (a : M) → N) 1 : N) = (f : (a : M) → N) (↑1 : M)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)

Tactic:
rw [← (hf.map_units 1).mul_right_inj, mul_one]

Premises used: Submonoid.IsLocalizationMap.map_units, IsUnit.mul_right_inj, mul_one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑1 : M) : N) ((f : (a : M) → N) 1 : N) = (f : (a : M) → N) (↑1 : M)

Tactic:
(map_mul ..).symm.trans congr(f $(mul_one _))

Premises used: congrArg, id, map_mul, mul_one, OfNat.ofNat, Eq.symm, Subtype.val, DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
F : Type u_4
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑1 : M) : N) ((f : (a : M) → N) 1 : N) = (f : (a : M) → N) (↑1 : M)

Tactic:
exact (map_mul ..).symm.trans congr(f $(mul_one _))

Premises used: congrArg, id, map_mul, mul_one, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
f : M → N
hf : S.IsLocalizationMap f
E : Type u_4
inst_3 : EquivLike E N P
inst_4 : MulEquivClass E N P
e_1 : E
y : P
e : N ≃* P := (↑e_1 : N ≃* P)
x : M × ↥S
eq : HMul.hMul (α := N) ((e.symm : (a : P) → N) y : N) (f (↑x.2 : M)) = f x.1
⊢ Eq.{u_2 + 1} (α := N) ((e.symm : (a : P) → N) (y * ((⇑e_1 : (a : N) → P) ∘ f) (↑x.2 : M)) : N)
    ((e.symm : (a : P) → N) (((⇑e_1 : (a : N) → P) ∘ f) x.1) : N)

Tactic:
simpa [e]
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f g : S.LocalizationMap N
mk :
  ∀ (toMulHom : M →ₙ* N) (isLocalizationMap : S.IsLocalizationMap toMulHom.toFun),
    { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom →
      { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N } = g
⊢ f.toMonoidHom = g.toMonoidHom → f = g

Tactic:
cases f
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
mk :
  ∀
    (eq :
      { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom =
        g.toMonoidHom),
    toMulHom = g.toMulHom
⊢ { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N } = g

Tactic:
congr! with eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
eq : { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom
mk : ∀ (x : M), Eq.{u_2 + 1} (α := N) ((toMulHom : (a : M) → N) x : N) ((g.toMulHom : (a : M) → N) x : N)
⊢ toMulHom = g.toMulHom

Tactic:
ext
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
eq : { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom
x : M
⊢ Eq.{u_2 + 1} (α := N) ((toMulHom : (a : M) → N) x : N) ((g.toMulHom : (a : M) → N) x : N)

Tactic:
congr($eq _)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
g : S.LocalizationMap N
toMulHom : M →ₙ* N
isLocalizationMap : S.IsLocalizationMap toMulHom.toFun
eq : { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap : S.LocalizationMap N }.toMonoidHom = g.toMonoidHom
x : M
⊢ Eq.{u_2 + 1} (α := N) ((toMulHom : (a : M) → N) x : N) ((g.toMulHom : (a : M) → N) x : N)

Tactic:
exact congr($eq _)
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ Eq.{u_2 + 1} (α := N) ((f.toMonoidHom : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f g : S.LocalizationMap N
h : ∀ (x : M), Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
y : ↥S
⊢ IsUnit.{u_2} (M := N) ((f : (a : M) → N) (↑y : M) : N)

Tactic:
f.2.1 y

Premises used: Submonoid.IsLocalizationMap.map_units, Submonoid.LocalizationMap.isLocalizationMap
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ ∃ (x : M × ↥S), HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1

Tactic:
f.2.2 z

Premises used: Submonoid.LocalizationMap.isLocalizationMap, Submonoid.IsLocalizationMap.surj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x y : M
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) → ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y

Tactic:
f.2.3

Premises used: Submonoid.IsLocalizationMap.exists_of_eq, Submonoid.LocalizationMap.isLocalizationMap
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
let :
  ∀ (a : M × ↥S) (ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1),
    ∃ (z' : M) (w' : M) (d : ↥S),
      HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
        HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'

Tactic:
let ⟨a, ha⟩ := surj f z
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
let :
  ∀ (b : M × ↥S) (hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1),
    ∃ (z' : M) (w' : M) (d : ↥S),
      HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
        HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'

Tactic:
let ⟨b, hb⟩ := surj f w
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'

Tactic:
⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩

Premises used: HMul.hMul, Prod.fst, And.intro, Exists.intro, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
refine_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) (a.1 * (↑b.2 : M))
refine_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) ((↑a.2 : M) * b.1)
⊢ ∃ (z' : M) (w' : M) (d : ↥S),
    HMul.hMul (β := N) z ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) z' ∧
      HMul.hMul (β := N) w ((f : (a : M) → N) (↑d : M) : N) = (f : (a : M) → N) w'

Tactic:
refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
refine_1 :
  z * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (β := N) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N)) ((f : (a : M) → N) (↑b.2 : M) : N)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) (a.1 * (↑b.2 : M))

Tactic:
simp_rw [mul_def, map_mul, ← ha]

Premises used: map_mul, Submonoid.mul_def
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ z * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (β := N) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N)) ((f : (a : M) → N) (↑b.2 : M) : N)

Tactic:
(mul_assoc z _ _).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ z * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (β := N) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N)) ((f : (a : M) → N) (↑b.2 : M) : N)

Tactic:
exact (mul_assoc z _ _).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
refine_2 :
  w * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (α := N) ((f : (a : M) → N) (↑a.2 : M) : N) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N))
⊢ HMul.hMul (β := N) w ((f : (a : M) → N) (↑(a.2 * b.2) : M) : N) = (f : (a : M) → N) ((↑a.2 : M) * b.1)

Tactic:
simp_rw [mul_def, map_mul, ← hb]

Premises used: map_mul, Submonoid.mul_def
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ w * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (α := N) ((f : (a : M) → N) (↑a.2 : M) : N) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N))

Tactic:
mul_left_comm w _ _

Premises used: mul_left_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : HMul.hMul (β := N) z ((f : (a : M) → N) (↑a.2 : M) : N) = (f : (a : M) → N) a.1
b : M × ↥S
hb : HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N) = (f : (a : M) → N) b.1
⊢ w * HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑a.2 : M) : N) ((f : (a : M) → N) (↑b.2 : M) : N) =
    HMul.hMul (α := N) ((f : (a : M) → N) (↑a.2 : M) : N) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑b.2 : M) : N))

Tactic:
exact mul_left_comm w _ _

Premises used: mul_left_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
f : S.LocalizationMap N
x y : M
h_1 : ∃ (c : ↥S), (↑c : M) * x = (↑c : M) * y
c : ↥S
h : (↑c : M) * x = (↑c : M) * y
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((↑c : M) * x) : N) ((f : (a : M) → N) ((↑c : M) * y) : N)

Tactic:
replace h := congr_arg f h