awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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
have rw₃ : HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (f.sec z).1 : P) (1 : P) = (g : (a : M) → P) (f.sec z).1
Tactic: rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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
have rw₄ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec z).1 : P) ((g : (a : M) → P) (f.sec z).1 : P)
Tactic: rw [lift_apply, mul_assoc, ← g.restrict_apply, IsUnit.liftRight_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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
have 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
Tactic: rw [mul_comm, lift_mul_right]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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
have rw₁ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) (f.sec z).1 : P) ((g : (a : M) → P) (f.sec z).1 : P)
Tactic: rw [mul_comm, lift_mul_right]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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 : (a : N) → P) ((f : (a : M) → N) x : N) : P) ((g : (a : M) → P) x : P)
have 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)
Tactic: rw [lift_spec, ← g.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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_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)
have 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)
Tactic: rw [sec_spec', map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: rw [sec_spec', map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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)
have 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)
Tactic: rw [lift_mk', lift_mk', mul_inv hg]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: rw [lift_mk', lift_mk', mul_inv hg]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: rw [lift_mk', lift_mk', mul_inv hg]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ (f.lift hg).comp f.toMonoidHom = g
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ f.lift ⋯ = j
have h : ∀ (x : N), Eq.{u_3 + 1} (α := P) ((f.lift sorry : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
have 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)
Tactic: simp_rw [lift_spec, j.comp_apply, ← map_mul, toMonoidHom_apply, sec_spec']
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
have 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)
Tactic: simp_rw [lift_spec, j.comp_apply, ← map_mul, toMonoidHom_apply, sec_spec']
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
have 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)
Tactic: simp_rw [lift_spec, j.comp_apply, ← map_mul, toMonoidHom_apply, sec_spec']
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ Eq.{u_3 + 1} (α := P) ((f.lift ⋯ : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
have 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)
Tactic: simp_rw [lift_spec, j.comp_apply, ← map_mul, toMonoidHom_apply, sec_spec']
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ f.lift hg = j
have h : ∀ (x : N), Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) x : P) ((j : (a : N) → P) x : P)
have 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)
Tactic: rw [lift_spec, ← hj, ← hj, ← j.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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)
have h : (f : (a : M) → N) (f.sec x).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ (f : (a : M) → N) (f.sec x).1 = HMul.hMul (α := N) ((f : (a : M) → N) (↑(f.sec x).2 : M) : N) x
have h : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (f.sec x).1 : N) ((f : (a : M) → N) (f.sec x).1 : N)
Tactic: rw [← sec_spec']
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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
⊢ 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)
have rw : Eq.{u_5 + 1} (α := A)
  (((k.lift hl).comp (f.lift (g := k.toMonoidHom) sorry) : (a : N) → A) ((f.toMonoidHom : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_5 + 1} (α := A) ((((k.lift hl).comp (f.lift (g := k.toMonoidHom) sorry)).comp f.toMonoidHom : (a : M) → A) x : A)
  ((l : (a : M) → A) x : A)
Tactic: rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have rw₂ : Eq.{u_5 + 1} (α := A)
  (((k.lift hl).comp (MonoidHom.comp (f.lift (g := k.toMonoidHom) sorry) f.toMonoidHom) : (a : M) → A) x : A)
  ((l : (a : M) → A) x : A)
Tactic: rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have rw₃ : Eq.{u_5 + 1} (α := A) (((k.lift hl).comp k.toMonoidHom : (a : M) → A) x : A) ((l : (a : M) → A) x : A)
Tactic: rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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)
have rw₄ : Eq.{u_5 + 1} (α := A) ((l : (a : M) → A) x : A) ((l : (a : M) → A) x : A)
Tactic: rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (goal)
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)
⊢ 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
have 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
Tactic: constructor