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
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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
⊢ z = w
have inl : ∀ (c : P) (hc' : c ∈ T)
  (eq :
    HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) z' : P) =
      HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) w' : P)),
  z = w
Tactic: have ⟨⟨c, hc'⟩, eq⟩ := k.exists_of_eq this
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
c : P
hc' : c ∈ T
eq :
  HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) z' : P) =
    HMul.hMul (β := P) (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) c hc') : P) ((g : (a : M) → P) w' : P)
⊢ z = w
have inl : ∀ (c : M) (hc : c ∈ (↑S : Set M)) (hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P))
  (eq :
    HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
        ((g : (a : M) → P) z' : P) =
      HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
        ((g : (a : M) → P) w' : P)),
  z = w
Tactic: obtain ⟨c, hc, rfl⟩ := surj hc'
Cleared hypotheses: c, hc', eq
-- 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
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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq :
  HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
      ((g : (a : M) → P) z' : P) =
    HMul.hMul (α := P) (β := P) ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) c) hc') : P) : P)
      ((g : (a : M) → P) w' : P)
⊢ z = w
have eq₁ : c * z' = c * w'
Tactic: simp_rw [← map_mul, hg.eq_iff] at eq
Cleared hypotheses: eq
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
c : M
hc : c ∈ (↑S : Set M)
hc' : Membership.mem (α := P) T ((g : (a : M) → P) c : P)
eq : c * z' = c * w'
⊢ z = w
have inl : ∃ (c : ↥S), (↑c : M) * z' = (↑c : M) * w'
Tactic: rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
⊢ z = w
have inr : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
Tactic: apply (f.map_units x).mul_right_cancel
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
have inr : (f : (a : M) → N) z' = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
Tactic: rw [hxz, hxw, hg (inj this)]
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
inr : (f : (a : M) → N) z' = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
have inr₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) z' : N) ((f : (a : M) → N) w' : N)
Tactic: rw [hxz, hxw, hg (inj this)]
-- 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
hg : Injective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z w : N
i : N →* Q := f.map hy k
hizw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) w : Q)
ifkg :
  ∀ (a : M),
    Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) a : N) : Q)
      ((k : (a : P) → Q) ((g : (a : M) → P) a : P) : Q)
z' w' : M
x : ↥S
hxz : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) z'
hxw : HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N) = (f : (a : M) → N) w'
this :
  Eq.{u_4 + 1} (α := Q) ((k : (a : P) → Q) ((g : (a : M) → P) z' : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)
inr : (f : (a : M) → N) z' = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
inr₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) z' : N) ((f : (a : M) → N) w' : N)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N) = HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)
have inr₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) w' : N) ((f : (a : M) → N) w' : N)
Tactic: rw [hxz, hxw, hg (inj this)]
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
z : Q
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = z
have obtain : ∀ (y t : P) (ht : t ∈ T), ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) t ht)
Tactic: obtain ⟨y, ⟨t, ht⟩, rfl⟩ := k.mk'_surjective z
Cleared hypotheses: 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
y t : P
ht : t ∈ T
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) t ht)
have obtain : ∀ (s : M) (hs : s ∈ (↑S : Set M)) (ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)),
  ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
Tactic: obtain ⟨s, hs, rfl⟩ := surj ht
Cleared hypotheses: t, ht
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
y : P
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
⊢ ∃ (a : N), (f.map hy k : (a : N) → Q) a = k.mk' y (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
have obtain : ∀ (x : M),
  ∃ (a : N),
    (f.map hy k : (a : N) → Q) a =
      k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
Tactic: obtain ⟨x, rfl⟩ := hg y
Cleared hypotheses: 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
x : M
⊢ ∃ (a : N),
    (f.map hy k : (a : N) → Q) a =
      k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
have h : (f.map hy k : (a : N) → Q) (f.mk' x (Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs)) =
  k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
Tactic: use f.mk' x ⟨s, hs⟩
-- 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
surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)
hg : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
s : M
hs : s ∈ (↑S : Set M)
ht : Membership.mem (α := P) T ((g : (a : M) → P) s : P)
x : M
⊢ (f.map hy k : (a : N) → Q) (f.mk' x (Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs)) =
    k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
have h : k.mk' ((g : (a : M) → P) x)
    (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ S) s hs) : M)) sorry) =
  k.mk' ((g : (a : M) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : M) → P) s) ht)
Tactic: rw [map_mk']
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : (k : (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
⊢ HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) ((f : (a : M) → N) x.1 : N)
have rw : HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
  (k : (a : N) → P) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N))
Tactic: rw [← hx, map_mul, ← hz]
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : (k : (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
rw :
  HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N))
⊢ HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) ((f : (a : M) → N) x.1 : N)
have rw₁ : HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
  HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P)
Tactic: rw [← hx, map_mul, ← hz]
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
v : P
z : N
hz : (k : (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
rw :
  HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N))
rw₁ :
  HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P)
⊢ HMul.hMul (β := P) v ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
    (k : (a : N) → P) ((f : (a : M) → N) x.1 : N)
have rw₂ : HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P) =
  HMul.hMul (α := P) (β := P) ((k : (a : N) → P) z : P) ((k : (a : N) → P) ((f : (a : M) → N) (↑x.2 : M) : N) : P)
Tactic: rw [← hx, map_mul, ← hz]
-- 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
⊢ f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f
have h : ∀ (x : M),
  Eq.{u_2 + 1} (α := N) ((f.ofMulEquivOfLocalizations (MulEquiv.refl N) : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
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
Q : Type u_4
inst_3 : CommMonoid Q
k : N ≃* P
j : P ≃* Q
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := Q) (((f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom : (a : M) → Q) x : Q)
    ((j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom : (a : M) → Q) x : Q)
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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
v : P
hv : (k : (a : P) → M) v = x.1
w : P
hw : (k : (a : P) → M) w = (↑x.2 : M)
⊢ HMul.hMul (β := N) z
      ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) (↑(v, Subtype.mk (p := fun (x : P) ↦ x ∈ T) w ⋯).2 : P) : N) =
    (f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) (v, Subtype.mk (p := fun (x : P) ↦ x ∈ T) w ⋯).1
have simp_rw : HMul.hMul (β := N) z ((f.toMonoidHom : (a : M) → N) (↑x.2 : M) : N) = (f.toMonoidHom : (a : M) → N) x.1
Tactic: simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw]
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
v : P
hv : (k : (a : P) → M) v = x.1
w : P
hw : (k : (a : P) → M) w = (↑x.2 : M)
⊢ HMul.hMul (β := N) z ((f : (a : M) → N) (↑x.2 : M) : N) = (f : (a : M) → N) x.1
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) x.1 : N)
Tactic: rw [hx]
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ Eq.{u_2 + 1} (α := N) ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) x : N)
      ((f.toMonoidHom.comp k.toMonoidHom : (a : P) → N) y : N) →
    ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
have rw : (∃ (c : ↥S),
    HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)) →
  ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
Tactic: rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
        MonoidHom.coe_coe, toMonoidHom_apply, toMonoidHom_apply, f.eq_iff_exists]
-- 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)
T : Submonoid P
Q : Type u_4
inst_3 : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) x : M) = HMul.hMul (β := M) (↑c : M) ((k : (a : P) → M) y : M)
⊢ ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
have let : ∀ (d : P) (hd : (k : (a : P) → M) d = (↑c : M)), ∃ (c : ↥T), (↑c : P) * x = (↑c : P) * y
Tactic: let ⟨d, hd⟩ := k.surjective c