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)
H : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
x y : M
mp :
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) →
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
have mp₁ : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P) →
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Maps (hypothesis)
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 : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := P) (⇑(f.lift hg) : (a : N) → P)
x y : M
h : Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have h₁ : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) ((f : (a : M) → N) x : N) : P)
  ((f.lift hg : (a : N) → P) ((f : (a : M) → N) y : N) : P)
Tactic: rw [← f.lift_eq hg, ← f.lift_eq hg] at h
Cleared hypotheses: h
-- 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)
H :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
      Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
⊢ z = w
have mpr : ∀ (w_1 : M × ↥S), HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1 → z = w
Tactic: obtain ⟨_, _⟩ := f.surj z
-- 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)
H :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
      Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
⊢ z = w
have mpr : ∀ (w_2 : M × ↥S), HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1 → z = w
Tactic: obtain ⟨_, _⟩ := f.surj w
-- 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)
H :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ↔
      Eq.{u_3 + 1} (α := P) ((g : (a : M) → P) x : P) ((g : (a : M) → P) y : P)
z w : N
h : Eq.{u_3 + 1} (α := P) ((f.lift hg : (a : N) → P) z : P) ((f.lift hg : (a : N) → P) w : P)
w_1 : M × ↥S
h_1 : HMul.hMul (β := N) z ((f : (a : M) → N) (↑w_1.2 : M) : N) = (f : (a : M) → N) w_1.1
w_2 : M × ↥S
h_2 : HMul.hMul (β := N) w ((f : (a : M) → N) (↑w_2.2 : M) : N) = (f : (a : M) → N) w_2.1
⊢ z = w
have mpr : f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2
Tactic: rw [← f.mk'_sec z, ← f.mk'_sec w]
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (f.map hy k : (a : N) → Q) (f.mk' x y) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯)
have rw : (k.toMonoidHom.comp g : (a : M) → Q) x =
  HMul.hMul (α := Q) ((k.toMonoidHom.comp g : (a : M) → Q) (↑y : M) : Q)
    (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) sorry))
Tactic: rw [map, lift_mk', mul_inv_left]
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMonoidHom.comp g : (a : M) → Q) x =
    HMul.hMul (α := Q) ((k.toMonoidHom.comp g : (a : M) → Q) (↑y : M) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))
have change : (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
  HMul.hMul (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑y : M) : P) : Q)
    (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) sorry))
Tactic: change k (g x) = k (g y) * _
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
    HMul.hMul (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑y : M) : P) : Q)
      (k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) ⋯))
have rw : (k : (a : P) → Q) ((g : (a : M) → P) x : P) =
  k.mk' (HMul.hMul (α := P) (β := P) ((g : (a : M) → P) (↑y : M) : P) ((g : (a : M) → P) x : P))
    (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑y : M)) sorry)
Tactic: rw [mul_mk'_eq_mk'_of_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
z : N
⊢ HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q)
      ((f.map hy k : (a : N) → Q) z : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)
have rw : HMul.hMul (α := Q) (β := Q) ((f.map hy k : (a : N) → Q) z : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
  (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)
Tactic: rw [mul_comm, f.map_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
z : N
rw :
  HMul.hMul (α := Q) (β := Q) ((f.map hy k : (a : N) → Q) z : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)
⊢ HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q)
      ((f.map hy k : (a : N) → Q) z : Q) =
    (k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P)
have rw₁ : Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
  ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
Tactic: rw [mul_comm, f.map_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
⊢ (k.map hl j).comp (f.map hy k) = f.map (g := l.comp g) ⋯ j
have h : ∀ (z : N),
  Eq.{u_6 + 1} (α := R) (((k.map hl j).comp (f.map hy k) : (a : N) → R) z : R)
    ((f.map (g := l.comp g) sorry j : (a : N) → R) z : R)
Tactic: ext z
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ Eq.{u_6 + 1} (α := R) (((k.map hl j).comp (f.map hy k) : (a : N) → R) z : R)
    ((f.map (g := l.comp g) ⋯ j : (a : N) → R) z : R)
have h : HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
    ((↑((IsUnit.liftRight ((j.toMonoidHom.comp l).restrict T) sorry : (a : ↥T) → Rˣ)
              (k.sec ((f.map hy k : (a : N) → Q) z)).2)⁻¹ :
        R) :
      R) =
  HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
    ((↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).restrict S) sorry : (a : ↥S) → Rˣ) (f.sec z).2)⁻¹ : R) : R)
Tactic: change j _ * _ = j (l _) * _
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp l).restrict T) ⋯ : (a : ↥T) → Rˣ)
                (k.sec ((f.map hy k : (a : N) → Q) z)).2)⁻¹ :
          R) :
        R) =
    HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
      ((↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).restrict S) ⋯ : (a : ↥S) → Rˣ) (f.sec z).2)⁻¹ : R) : R)
have h : HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
    ((j.toMonoidHom.comp (l.comp g) : (a : M) → R) (↑(f.sec z).2 : M) : R) =
  HMul.hMul (α := R) (β := R) ((j.toMonoidHom.comp l : (a : P) → R) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : R)
    ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
Tactic: rw [mul_inv_left, ← mul_assoc, mul_inv_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j.toMonoidHom.comp (l.comp g) : (a : M) → R) (↑(f.sec z).2 : M) : R) =
    HMul.hMul (α := R) (β := R)
      ((j.toMonoidHom.comp l : (a : P) → R) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
have h : HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
    ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : A) : R) =
  HMul.hMul (α := R) (β := R)
    ((j : (a : A) → R) ((l : (a : P) → A) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : A) : R)
    ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
Tactic: change j _ * j (l (g _)) = j (l _) * _
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ HMul.hMul (α := R) (β := R) ((j : (a : A) → R) ((l : (a : P) → A) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : A) : R) =
    HMul.hMul (α := R) (β := R)
      ((j : (a : A) → R) ((l : (a : P) → A) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : A) : R)
      ((j : (a : A) → R) ((l : (a : P) → A) ((g : (a : M) → P) (f.sec z).1 : P) : A) : R)
have h : Eq.{u_6 + 1} (α := R)
  ((j : (a : A) → R)
      ((l : (a : P) → A)
          (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
        A) :
    R)
  ((j : (a : A) → R)
      ((l : (a : P) → A)
          (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
        A) :
    R)
Tactic: rw [← map_mul j, ← map_mul j, ← l.map_mul, ← l.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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ Eq.{u_6 + 1} (α := R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
          A) :
      R)
    ((j : (a : A) → R)
        ((l : (a : P) → A)
            (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
          A) :
      R)
have h : Eq.{u_4 + 1} (α := Q)
  ((k : (a : P) → Q)
      (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
    Q)
  ((k : (a : P) → Q)
      (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
    Q)
Tactic: refine k.comp_eq_of_eq hl j ?_
-- 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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
⊢ Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)
have h : HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
  (k : (a : P) → Q)
    (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P))
Tactic: rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
h :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q)
      (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P))
⊢ Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)
have h₁ : HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
Tactic: rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
h :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q)
      (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P))
h₁ :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
⊢ Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)
have h₂ : HMul.hMul (β := Q)
    (HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((f.map hy k : (a : N) → Q) z : Q))
    ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
Tactic: rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_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
T : Submonoid P
hy : ∀ (y : ↥S), Membership.mem (α := P) T ((g : (a : M) → P) (↑y : M) : P)
Q : Type u_4
inst_3 : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst_4 : CommMonoid A
U : Submonoid A
R : Type u_6
inst_5 : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), Membership.mem (α := A) U ((l : (a : P) → A) (↑w : P) : A)
z : N
h :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    (k : (a : P) → Q)
      (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P))
h₁ :
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (k.sec ((f.map hy k : (a : N) → Q) z)).1 : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
h₂ :
  HMul.hMul (β := Q)
      (HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
        ((f.map hy k : (a : N) → Q) z : Q))
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q) =
    HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
⊢ Eq.{u_4 + 1} (α := Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (k.sec ((f.map hy k : (a : N) → Q) z)).1 ((g : (a : M) → P) (↑(f.sec z).2 : M) : P)) :
      Q)
    ((k : (a : P) → Q)
        (HMul.hMul (β := P) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) ((g : (a : M) → P) (f.sec z).1 : P)) :
      Q)
have h₃ : HMul.hMul (α := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
    (HMul.hMul (α := Q) (β := Q) ((f.map hy k : (a : N) → Q) z : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) (↑(f.sec z).2 : M) : P) : Q)) =
  HMul.hMul (α := Q) (β := Q) ((k : (a : P) → Q) (↑(k.sec ((f.map hy k : (a : N) → Q) z)).2 : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : P) : Q)
Tactic: rw [map_mul k, map_mul k, sec_spec', mul_assoc, map_mul_right]