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
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)
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)
⊢ 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)).2 : P) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) (f.sec z).1 : 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)
x : N
⊢ Eq.{u_6 + 1} (α := R) ((k.map hl j : (a : Q) → R) ((f.map hy k : (a : N) → Q) x : Q) : R)
    ((f.map (g := l.comp g) ⋯ j : (a : N) → R) x : R)
have rw : Eq.{u_6 + 1} (α := R) ((k.map hl j : (a : Q) → R) ((f.map hy k : (a : N) → Q) x : Q) : R)
  (((k.map hl j).comp (f.map hy k) : (a : N) → R) x : R)
Tactic: rw [← f.map_comp_map (k := k) hy j hl]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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)
⊢ z = w
have 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)
Tactic: have ifkg (a : M) : i (f a) = k (g a) := f.map_eq hy a
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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
have have : ∀ (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'), z = w
Tactic: have ⟨z', w', x, hxz, hxw⟩ := surj₂ f z 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
⊢ 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)
have rw : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
  ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
⊢ 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)
have rw₁ : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
  ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
⊢ 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)
have rw₂ : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
  ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₂ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
⊢ 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)
have rw₃ : Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
  ((i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₂ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₃ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)) : Q)
⊢ 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)
have rw₄ : HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
  (i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N))
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₂ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₃ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)) : Q)
rw₄ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    (i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N))
⊢ 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)
have rw₅ : HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
rw :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((k : (a : P) → Q) ((g : (a : M) → P) w' : P) : Q)
rw₁ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) ((f : (a : M) → N) z' : N) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₂ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) ((f : (a : M) → N) w' : N) : Q)
rw₃ :
  Eq.{u_4 + 1} (α := Q) ((i : (a : N) → Q) (HMul.hMul (β := N) z ((f : (a : M) → N) (↑x : M) : N)) : Q)
    ((i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N)) : Q)
rw₄ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    (i : (a : N) → Q) (HMul.hMul (β := N) w ((f : (a : M) → N) (↑x : M) : N))
rw₅ :
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) z : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
    HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q)
⊢ 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)
have rw₆ : HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q) =
  HMul.hMul (α := Q) (β := Q) ((i : (a : N) → Q) w : Q) ((i : (a : N) → Q) ((f : (a : M) → N) (↑x : M) : N) : Q)
Tactic: rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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'
⊢ z = w
have 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)
Tactic: have : k (g z') = k (g w') := by rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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)
⊢ z = w
have inl : ∀ (surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)), z = w
Tactic: obtain surj | inj := or
Cleared hypotheses: or
-- 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
or :
  Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P) ∨
    Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → 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)
inl : ∀ (surj : Set.SurjOn (⇑g : (a : M) → P) (↑S : Set M) (↑T : Set P)), z = w
⊢ z = w
have inr : ∀ (inj : Injective.{u_3 + 1, u_4 + 1} (α := P) (β := Q) (⇑k : (a : P) → Q)), z = w
Tactic: obtain surj | inj := or
Cleared hypotheses: or