awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
choose :
  ∀ (x : (i : ι) → (z : N i) → M i × ↥(S i)) (hx : ∀ (i : ι) (z : N i), z * f i (↑(x i z).2 : M i) = f i (x i z).1),
    ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
      z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1
⊢ ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
    z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1

Tactic:
choose x hx using fun i ↦ (hf i).surj

Premises used: Submonoid.IsLocalizationMap.surj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
x : (i : ι) → (z : N i) → M i × ↥(S i)
hx : ∀ (i : ι) (z : N i), z * f i (↑(x i z).2 : M i) = f i (x i z).1
⊢ ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
    z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1

Tactic:
⟨⟨fun i ↦ (x i (z i)).1, ⟨_, fun i _ ↦ (x i (z i)).2.2⟩⟩, funext fun i ↦ hx i (z i)⟩

Premises used: Prod.mk, Prod.fst, Subtype.mk, funext, Exists.intro, Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
x : (i : ι) → (z : N i) → M i × ↥(S i)
hx : ∀ (i : ι) (z : N i), z * f i (↑(x i z).2 : M i) = f i (x i z).1
⊢ ∃ (x : ((i : ι) → M i) × ↥(pi (M := M) Set.univ S)),
    z * Pi.map (α := M) (β := N) f (↑x.2 : (i : ι) → M i) = Pi.map (α := M) (β := N) f x.1

Tactic:
exact ⟨⟨fun i ↦ (x i (z i)).1, ⟨_, fun i _ ↦ (x i (z i)).2.2⟩⟩, funext fun i ↦ hx i (z i)⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map (α := M) (β := N) f x = Pi.map (α := M) (β := N) f y
choose :
  ∀ (c : (i : ι) → ↥(S i)) (hc : ∀ (i : ι), (↑(c i) : M i) * x i = (↑(c i) : M i) * y i),
    ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y
⊢ ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y

Tactic:
choose c hc using fun i ↦ (hf i).exists_of_eq congr($eq i)

Premises used: Submonoid.IsLocalizationMap.exists_of_eq, id, congrFun
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map (α := M) (β := N) f x = Pi.map (α := M) (β := N) f y
c : (i : ι) → ↥(S i)
hc : ∀ (i : ι), (↑(c i) : M i) * x i = (↑(c i) : M i) * y i
⊢ ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y

Tactic:
⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

Premises used: Subtype.mk, funext, Exists.intro, Subtype.property
-- Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Goal:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst : (i : ι) → CommMonoid (M i)
inst_1 : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map (α := M) (β := N) f x = Pi.map (α := M) (β := N) f y
c : (i : ι) → ↥(S i)
hc : ∀ (i : ι), (↑(c i) : M i) * x i = (↑(c i) : M i) * y i
⊢ ∃ (c : ↥(pi (M := M) Set.univ S)), (↑c : (i : ι) → M i) * x = (↑c : (i : ι) → M i) * y

Tactic:
exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
obtain :
  ∀ (c : ↥S) (hc : (↑c : M) * x = (↑c : M) * y),
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)

Tactic:
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h

Premises used: Submonoid.LocalizationMap.eq_iff_exists, Iff.mp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        (((g.restrict S : MonoidHom.{u_1, u_3} (↥S) P) : (a : ↥S) → P) c : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)

Tactic:
rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]

Premises used: MonoidHom.restrict, IsUnit.liftRight_inv_mul, DFunLike.coe, one_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
change :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        (((g.restrict S : MonoidHom.{u_1, u_3} (↥S) P) : (a : ↥S) → P) c : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y

Tactic:
change _ * g c * _ = _

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
c : ↥S
hc : (↑c : M) * x = (↑c : M) * y
rw :
  (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y
rw₁ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * x) : P) =
    (g : (a : M) → P) y
rw₂ :
  HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
      ((g : (a : M) → P) ((↑c : M) * y) : P) =
    (g : (a : M) → P) y
rw₃ :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((↑c : M) * y) : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P) =
    (g : (a : M) → P) y
rw₄ :
  (g : (a : M) → P) ((↑c : M) * y) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P)
rw₅ rw₆ :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑c : M) : P) ((g : (a : M) → P) y : P)
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) c)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑c : M) : P))
      ((g : (a : M) → P) x : P) =
    (g : (a : M) → P) y

Tactic:
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]

Premises used: mul_assoc, mul_comm, Submonoid.LocalizationMap.mul_inv_left, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
hg : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
k : T.LocalizationMap Q
x y : M
h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) x : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) y : P) : Q)

Tactic:
f.eq_of_eq (fun y : S ↦ show IsUnit (k.toMonoidHom.comp g y) from k.map_units ⟨g y, hg y⟩) h

Premises used: Subtype.mk, Submonoid.LocalizationMap.map_units, Subtype.val, DFunLike.coe, Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
rw : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec 1).1 : P) ((g : (a : M) → P) (↑(f.sec 1).2 : M) : P)
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec 1).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec 1).2)⁻¹ : P) : P) =
    1

Tactic:
rw [mul_inv_left, mul_one]

Premises used: Submonoid.LocalizationMap.mul_inv_left, mul_one
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
rw :
  HMul.hMul (α := N) (β := N) (1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N) = (f : (a : M) → N) (↑(f.sec 1).2 : M)
rw₁ rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec 1).1 : N) ((f : (a : M) → N) (↑(f.sec 1).2 : M) : N)

Tactic:
rw [← sec_spec, one_mul]

Premises used: Submonoid.LocalizationMap.sec_spec, one_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec 1).1 : P) ((g : (a : M) → P) (↑(f.sec 1).2 : M) : P)

Tactic:
exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])

Premises used: Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
rw :
  HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec (x * y)).2)⁻¹ : P) : P) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec x).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec x).2)⁻¹ : P) : P) *
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec y).2)⁻¹ : P) : P)

Tactic:
rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ←
      mul_assoc, ← mul_assoc, mul_inv_right hg]

Premises used: Submonoid.LocalizationMap.sec, mul_assoc, Prod.fst, mul_comm, Submonoid.LocalizationMap.mul_inv_right, Submonoid.LocalizationMap.mul_inv_left, DFunLike.coe
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
rw :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M)) : P)
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)

Tactic:
rw [← g.map_mul]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
rw :
  (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M)) : P)
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)

Tactic:
rw [← g.map_mul]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
rw :
  (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M)) : P)
      ((g : (a : M) → P) (f.sec x).1 : P)
⊢ (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)

Tactic:
rw [← g.map_mul]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
rw :
  Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
    ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)
⊢ (g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M)) : P)
      ((g : (a : M) → P) (f.sec x).1 : P)

Tactic:
rw [← g.map_mul]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
repeat :
  Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
    ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)
⊢ HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec (x * y)).1 : P) ((g : (a : M) → P) (↑(f.sec y).2 : M) : P))
      ((g : (a : M) → P) (↑(f.sec x).2 : M) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec y).1 : P) ((g : (a : M) → P) (↑(f.sec (x * y)).2 : M) : P))
      ((g : (a : M) → P) (f.sec x).1 : P)

Tactic:
repeat rw [← g.map_mul]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
    ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)

Tactic:
f.eq_of_eq hg ?_

Premises used: Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
refine :
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : N)
    ((f : (a : M) → N) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : N)
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : P)
    ((g : (a : M) → P) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : P)

Tactic:
refine f.eq_of_eq hg ?_

Premises used: Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
simp_rw :
  HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) (x * y))
        ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N))
      ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N) y)
        ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) *
      HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) x
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (x * y)).1 * (↑(f.sec y).2 : M) * (↑(f.sec x).2 : M)) : N)
    ((f : (a : M) → N) ((f.sec y).1 * (↑(f.sec (x * y)).2 : M) * (f.sec x).1) : N)

Tactic:
simp_rw [map_mul, sec_spec', ← toMonoidHom_apply]

Premises used: map_mul, Submonoid.LocalizationMap.sec_spec', Submonoid.LocalizationMap.toMonoidHom_apply
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x y : N
⊢ HMul.hMul (β := N)
      (HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) (x * y))
        ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N))
      ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec y).2 : M) : N) y)
        ((f.toMonoidHom : (a : M) → N) (↑(f.sec (x * y)).2 : M) : N) *
      HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) x

Tactic:
ac_rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
z : N
⊢ (f.lift hg : (a : N) → P) z =
    HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P)
      ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
y : ↥S
simp_rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (f.sec (f.mk' x y)).1 : N) ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₁ :
  HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) (f.mk' x y))
      ((f : (a : M) → N) (↑y : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₂ :
  HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
      (HMul.hMul (β := N) (f.mk' x y) ((f : (a : M) → N) (↑y : M) : N)) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
simp_rw₃ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) (↑(f.sec (f.mk' x y)).2 : M) : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ((f.sec (f.mk' x y)).1 * (↑y : M)) : N)
    ((f : (a : M) → N) (x * (↑(f.sec (f.mk' x y)).2 : M)) : N)

Tactic:
simp_rw [map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]

Premises used: mul_assoc, map_mul, Submonoid.LocalizationMap.sec_spec', mul_comm, Submonoid.LocalizationMap.mk'_spec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : S.LocalizationMap P
x : M
y : ↥S
⊢ (f.lift ⋯ : (a : N) → P) (f.mk' x y) = g.mk' x y

Tactic:
f.lift_mk' _ _ _

Premises used: Submonoid.LocalizationMap.mk', Submonoid.LocalizationMap.lift_mk'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Maps
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 : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
z : N
v : P
⊢ (f.lift hg : (a : N) → P) z = v ↔
    (g : (a : M) → P) (f.sec z).1 = HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v

Tactic:
mul_inv_left hg _ _ v

Premises used: Submonoid.LocalizationMap.mul_inv_left