awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w v : P
rw :
  HMul.hMul (β := P) w ((f.lift hg : (a : N) → P) z : P) = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₁ :
  w *
        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) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₂ :
  HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) *
        (↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) =
      v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₃ :
  HMul.hMul (β := P) w ((g : (a : M) → P) (f.sec z).1 : P) =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
rw₄ rw₅ :
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v
⊢ HMul.hMul (α := P) ((f.lift hg : (a : N) → P) z : P) w = v ↔
    HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P) w =
      HMul.hMul (α := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) v

Tactic:
rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]

Premises used: mul_assoc, Submonoid.LocalizationMap.lift_apply, mul_comm, Submonoid.LocalizationMap.mul_inv_left
-- 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
v : P
y : ↥S
rw :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) y)⁻¹ : P) : P) =
      v ↔
    (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v
⊢ (f.lift hg : (a : N) → P) (f.mk' x y) = v ↔
    (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v

Tactic:
rw [f.lift_mk' hg]

Premises used: 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)
x : M
v : P
y : ↥S
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) y)⁻¹ : P) : P) =
      v ↔
    (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v

Tactic:
mul_inv_left hg _ _ _

Premises used: Submonoid.LocalizationMap.mul_inv_left
-- 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
v : P
y : ↥S
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) y)⁻¹ : P) : P) =
      v ↔
    (g : (a : M) → P) x = HMul.hMul (α := P) ((g : (a : M) → P) (↑y : M) : P) v

Tactic:
exact mul_inv_left hg _ _ _

Premises used: Submonoid.LocalizationMap.mul_inv_left
-- 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
rw :
  HMul.hMul (β := P)
      (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))
      ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
rw₁ :
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)
        ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) =
    (g : (a : M) → P) (f.sec z).1
rw₂ :
  HMul.hMul (α := P) ((g : (a : M) → P) (f.sec z).1 : P)
      (HMul.hMul (α := P) (β := P) ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) (f.sec z).2)⁻¹ : P) : P)
        ((g.restrict S : (a : ↥S) → P) (f.sec z).2 : P)) =
    (g : (a : M) → P) (f.sec z).1
rw₃ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P) (1 : P) = (g : (a : M) → P) (f.sec z).1
rw₄ rw₅ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec z).1 : P) ((g : (a : M) → P) (f.sec z).1 : P)
⊢ HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1

Tactic:
rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, mul_one]

Premises used: mul_assoc, MonoidHom.restrict_apply, Submonoid.LocalizationMap.lift_apply, mul_one, IsUnit.liftRight_inv_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)
z : N
rw :
  HMul.hMul (α := P) (β := P) ((f.lift hg : (a : N) → P) z : P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) =
    (g : (a : M) → P) (f.sec z).1
rw₁ rw₂ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec z).1 : P) ((g : (a : M) → P) (f.sec z).1 : P)
⊢ HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) ((f.lift hg : (a : N) → P) z : P) =
    (g : (a : M) → P) (f.sec z).1

Tactic:
rw [mul_comm, lift_mul_right]

Premises used: Submonoid.LocalizationMap.lift_mul_right, mul_comm
-- 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
rw :
  Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec ((f : (a : M) → N) x)).1 : P)
    ((g : (a : M) → P) ((↑(f.sec ((f : (a : M) → N) x)).2 : M) * x) : P)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)

Tactic:
rw [lift_spec, ← g.map_mul]

Premises used: Submonoid.LocalizationMap.lift_spec, 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 : M
rw :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec ((f : (a : M) → N) x)).2 : M) : N) ((f : (a : M) → N) x : N) =
    (f : (a : M) → N) ((↑(f.sec ((f : (a : M) → N) x)).2 : M) * x)
rw₁ rw₂ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec ((f : (a : M) → N) x)).2 : M) : N) ((f : (a : M) → N) x : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) (↑(f.sec ((f : (a : M) → N) x)).2 : M) : N) ((f : (a : M) → N) x : N)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec ((f : (a : M) → N) x)).1 : N)
    ((f : (a : M) → N) ((↑(f.sec ((f : (a : M) → N) x)).2 : M) * x) : N)

Tactic:
rw [sec_spec', map_mul]

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

Tactic:
exact f.eq_of_eq hg (by rw [sec_spec', map_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 : M × ↥S
rw :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
      (f.lift hg : (a : N) → P) (f.mk' y.1 y.2) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (x.1 * (↑y.2 : M)) : P) ((g : (a : M) → P) (y.1 * (↑x.2 : M)) : P)
rw₁ :
  HMul.hMul (α := P) (β := P) ((g : (a : M) → P) x.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) x.2)⁻¹ : P) : P) =
      HMul.hMul (α := P) (β := P) ((g : (a : M) → P) y.1 : P)
        ((↑((IsUnit.liftRight (g.restrict S) hg : (a : ↥S) → Pˣ) y.2)⁻¹ : P) : P) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (x.1 * (↑y.2 : M)) : P) ((g : (a : M) → P) (y.1 * (↑x.2 : M)) : P)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (x.1 * (↑y.2 : M)) : P) ((g : (a : M) → P) (y.1 * (↑x.2 : M)) : P) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (x.1 * (↑y.2 : M)) : P) ((g : (a : M) → P) (y.1 * (↑x.2 : M)) : P)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) (f.mk' x.1 x.2) : P)
      ((f.lift hg : (a : N) → P) (f.mk' y.1 y.2) : P) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (x.1 * (↑y.2 : M)) : P) ((g : (a : M) → P) (y.1 * (↑x.2 : M)) : P)

Tactic:
rw [lift_mk', lift_mk', mul_inv hg]

Premises used: Submonoid.LocalizationMap.lift_mk', Submonoid.LocalizationMap.mul_inv
-- 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)
h : ∀ (x : M), Eq.{u_3 + 1} (α := P) (((f.lift hg).comp f.toMonoidHom : (a : M) → P) x : P) ((g : (a : M) → P) x : P)
⊢ (f.lift hg).comp f.toMonoidHom = g

Tactic:
ext
-- 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
⊢ Eq.{u_3 + 1} (α := P) (((f.lift hg).comp f.toMonoidHom : (a : M) → P) x : P) ((g : (a : M) → P) x : P)

Tactic:
f.lift_eq hg _

Premises used: Submonoid.LocalizationMap.lift_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 : M
⊢ Eq.{u_3 + 1} (α := P) (((f.lift hg).comp f.toMonoidHom : (a : M) → P) x : P) ((g : (a : M) → P) x : P)

Tactic:
exact f.lift_eq hg _

Premises used: Submonoid.LocalizationMap.lift_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
j : N →* P
h : ∀ (x : N), Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
⊢ f.lift ⋯ = j

Tactic:
ext
-- 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
j : N →* P
x : N
h :
  (j.comp f.toMonoidHom : (a : M) → P) (f.sec x).1 =
    HMul.hMul (α := P) (β := P) ((j.comp f.toMonoidHom : (a : M) → P) (↑(f.sec x).2 : M) : P) ((j : (a : N) → P) x : P)
h₁ :
  (j : (a : N) → P) ((f.toMonoidHom : (a : M) → N) (f.sec x).1 : N) =
    HMul.hMul (α := P) (β := P) ((j : (a : N) → P) ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) : P)
      ((j : (a : N) → P) x : P)
h₂ :
  Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f.toMonoidHom : (a : M) → N) (f.sec x).1 : N) : P)
    ((j : (a : N) → P) (HMul.hMul (α := N) ((f.toMonoidHom : (a : M) → N) (↑(f.sec x).2 : M) : N) x) : P)
h₃ :
  Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) (f.sec x).1 : N) : P)
    ((j : (a : N) → P) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x) : P)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)

Tactic:
simp_rw [lift_spec, j.comp_apply, ← map_mul, toMonoidHom_apply, sec_spec']

Premises used: Submonoid.LocalizationMap.lift_spec, map_mul, Submonoid.LocalizationMap.sec_spec', Submonoid.LocalizationMap.toMonoidHom_apply, MonoidHom.comp_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)
j : N →* P
hj : ∀ (x : M), Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)
h : ∀ (x : N), Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
⊢ f.lift hg = j

Tactic:
ext
-- 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)
j : N →* P
hj : ∀ (x : M), Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)
x : N
h :
  Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) (f.sec x).1 : N) : P)
    ((j : (a : N) → P) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x) : P)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) x : P) ((j : (a : N) → P) x : P)

Tactic:
rw [lift_spec, ← hj, ← hj, ← j.map_mul]

Premises used: Submonoid.LocalizationMap.lift_spec, 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)
j : N →* P
hj : ∀ (x : M), Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)
x : N
h : (f : (a : M) → N) (f.sec x).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x
⊢ Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) (f.sec x).1 : N) : P)
    ((j : (a : N) → P) (HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x) : P)

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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)
j : N →* P
hj : ∀ (x : M), Eq.{u_3 + 1} (α := P) ((j : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)
x : N
h h₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec x).1 : N) ((f : (a : M) → N) (f.sec x).1 : N)
⊢ (f : (a : M) → N) (f.sec x).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x

Tactic:
rw [← sec_spec']

Premises used: Submonoid.LocalizationMap.sec_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
f : S.LocalizationMap N
x : N
⊢ (f.lift ⋯ : (a : N) → N) x = x

Tactic:
DFunLike.ext_iff.1 (f.lift_of_comp <| MonoidHom.id N) x

Premises used: Submonoid.LocalizationMap.lift_of_comp, DFunLike.ext_iff, MonoidHom.id, 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
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst_2 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_3 : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit.{u_5} (M := A) ((l : (a : M) → A) (↑w : M) : A)
x : M
rw :
  Eq.{u_5 + 1} (α := A)
    (((k.lift hl).comp (f.lift (g := k.toMonoidHom) ⋯) : (a : N) → A) ((f.toMonoidHom : (a : M) → N) x : N) : A)
    ((l : (a : M) → A) x : A)
rw₁ :
  Eq.{u_5 + 1} (α := A) ((((k.lift hl).comp (f.lift (g := k.toMonoidHom) ⋯)).comp f.toMonoidHom : (a : M) → A) x : A)
    ((l : (a : M) → A) x : A)
rw₂ :
  Eq.{u_5 + 1} (α := A)
    (((k.lift hl).comp (MonoidHom.comp (f.lift (g := k.toMonoidHom) ⋯) f.toMonoidHom) : (a : M) → A) x : A)
    ((l : (a : M) → A) x : A)
rw₃ : Eq.{u_5 + 1} (α := A) (((k.lift hl).comp k.toMonoidHom : (a : M) → A) x : A) ((l : (a : M) → A) x : A)
rw₄ rw₅ : Eq.{u_5 + 1} (α := A) ((l : (a : M) → A) x : A) ((l : (a : M) → A) x : A)
⊢ Eq.{u_5 + 1} (α := A) (((k.lift hl).comp (f.lift (g := k.toMonoidHom) ⋯) : (a : N) → A) ((f : (a : M) → N) x : N) : A)
    ((l : (a : M) → A) x : A)

Tactic:
rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]

Premises used: MonoidHom.comp_assoc, Submonoid.LocalizationMap.lift_comp, Submonoid.LocalizationMap.toMonoidHom_apply, MonoidHom.comp_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
f : S.LocalizationMap N
Q : Type u_4
inst_2 : CommMonoid Q
k : S.LocalizationMap Q
A : Type u_5
inst_3 : CommMonoid A
l : M →* A
hl : ∀ (w : ↥S), IsUnit.{u_5} (M := A) ((l : (a : M) → A) (↑w : M) : A)
⊢ (k.lift hl).comp (f.lift ⋯) = f.lift hl

Tactic:
lift_comp_lift f le_rfl k hl

Premises used: le_rfl, Submonoid.LocalizationMap.lift_comp_lift
-- 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
k : S.LocalizationMap P
z : N
⊢ (k.lift ⋯ : (a : P) → N) ((f.lift ⋯ : (a : N) → P) z : P) = z

Tactic:
(DFunLike.congr_fun (lift_comp_lift_eq f k f.map_units) z).trans (lift_id f z)

Premises used: Submonoid.LocalizationMap.lift_comp_lift_eq, DFunLike.congr_fun, Submonoid.LocalizationMap.map_units, Eq.trans, Submonoid.LocalizationMap.lift_id
-- 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)
mp :
  Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) →
    ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
mpr :
  (∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1) →
    Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P) ↔
    ∀ (v : P), ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1

Tactic:
constructor
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
mp :
  ∀ (z : N) (hz : (f.lift hg : (a : N) → P) z = v),
    ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1

Tactic:
obtain ⟨z, hz⟩ := H v
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
mp :
  ∀ (x : M × ↥S) (hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1),
    ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1

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

Premises used: Submonoid.LocalizationMap.surj
-- 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)
H : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
v : P
z : N
hz : (f.lift hg : (a : N) → P) z = v
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
h : HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1
⊢ ∃ (x : M × ↥S), HMul.hMul (β := P) v ((g : (a : M) → P) (↑x.2 : M) : P) = (g : (a : M) → P) x.1

Tactic:
use x