awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
m : M
x : G × ↥S
eq : HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M) = (f : (a : G) → M) x.1
h₁ : (f : (a : G) → M) (x.1 * (↑x.2 : G)⁻¹) = m
h₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x.1 : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₃ :
  HMul.hMul (β := M) (HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M)) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₄ : m * HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (↑x.2 : G) : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₅ : HMul.hMul (β := M) m ((f : (a : G) → M) ((↑x.2 : G) * (↑x.2 : G)⁻¹) : M) = m
h₆ : HMul.hMul (β := M) m ((f : (a : G) → M) 1 : M) = m
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₇ : m * 1 = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
F : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
S : Submonoid G
inst_2 : FunLike F G M
inst_3 : MulHomClass F G M
f : F
h : IsLocalizationMap.{u_2, u_1} (M := G) (N := M) S (⇑f : (a : G) → M)
m : M
x : G × ↥S
eq : HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M) = (f : (a : G) → M) x.1
h₁ : (f : (a : G) → M) (x.1 * (↑x.2 : G)⁻¹) = m
h₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x.1 : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₃ :
  HMul.hMul (β := M) (HMul.hMul (β := M) m ((f : (a : G) → M) (↑x.2 : G) : M)) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₄ : m * HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (↑x.2 : G) : M) ((f : (a : G) → M) (↑x.2 : G)⁻¹ : M) = m
h₅ : HMul.hMul (β := M) m ((f : (a : G) → M) ((↑x.2 : G) * (↑x.2 : G)⁻¹) : M) = m
h₆ : HMul.hMul (β := M) m ((f : (a : G) → M) 1 : M) = m
h₇ : m * 1 = m
⊢ (f : (a : G) → M) (x.1 / (↑x.2 : G)) = m
have h₈ : m = m
Tactic: rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℤ
⊢ ∃ (x : ℕ), ∃ y ∈ S, z = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
have inl : ∀ (z : ℕ), ∃ (x : ℕ), ∃ y ∈ S, (↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
Tactic: obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℤ
inl : ∀ (z : ℕ), ∃ (x : ℕ), ∃ y ∈ S, (↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
⊢ ∃ (x : ℕ), ∃ y ∈ S, z = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
have inr : ∀ (z : ℕ), ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
Tactic: obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
have inr : ∀ (n : ℕ) (hnS : n ∈ S) (hn0 : n ≠ 0), ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
Tactic: have ⟨n, hnS, hn0⟩ := S.bot_or_exists_ne_zero.resolve_left hS
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
⊢ ∃ (x : ℕ), ∃ y ∈ S, -(↑z : ℤ) = HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
have key : z < n * (z / n + 1)
Tactic: have key : z < n * (z / n + 1) := Nat.lt_mul_div_succ _ <| Nat.pos_of_ne_zero hn0
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
⊢ Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔ ∀ ⦃x : M⦄, x ∈ S → IsRegular x
have simp_rw : (∀ ⦃a₁ a₂ : M⦄ (a : M) (b : a ∈ S), a * a₁ = a * a₂ → a₁ = a₂) ↔
  ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂
Tactic: simp_rw [Commute.isRegular_iff (Commute.all _), IsLeftRegular,
    Injective, LocalizationMap.eq_iff_exists, exists_imp, Subtype.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
⊢ IsRegular.{u_2} (R := N) ((f : (a : M) → N) m : N)
have refine : ∀ (n₁ n₂ : N)
  (eq :
    Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
      ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)),
  n₁ = n₂
Tactic: refine (Commute.isRegular_iff (Commute.all _)).mpr fun n₁ n₂ eq ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
⊢ n₁ = n₂
have have : ∀ (ms₁ : M × ↥S) (eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1), n₁ = n₂
Tactic: have ⟨ms₁, eq₁⟩ := f.surj n₁
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
⊢ n₁ = n₂
have have : ∀ (ms₂ : M × ↥S) (eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1), n₁ = n₂
Tactic: have ⟨ms₂, eq₂⟩ := f.surj n₂
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
⊢ n₁ = n₂
have rw : HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
  HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
Tactic: rw [← (f.map_units (ms₁.2 * ms₂.2)).mul_left_inj, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq :
  Eq.{u_2 + 1} (α := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁)
    ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂)
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
⊢ HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
have eq₃ : HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁ : N)
    ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
  HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂ : N)
    ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
Tactic: replace eq := congr($eq * f (ms₁.2 * ms₂.2))
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₁ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (α := N) (β := N) ((fun (x : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) m : N) x) n₂ : N)
      ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
⊢ HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
have eq₃ : HMul.hMul (α := N) ((f : (a : M) → N) m : N)
    (HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)) =
  HMul.hMul (α := N) ((f : (a : M) → N) m : N)
    (HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N))
Tactic: simp_rw [mul_assoc] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)) =
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N))
⊢ HMul.hMul (β := N) n₁ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N) =
    HMul.hMul (β := N) n₂ ((f : (a : M) → N) ((↑ms₁.2 : M) * (↑ms₂.2 : M)) : N)
have rw : ∀
  (eq :
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N)) =
      HMul.hMul (α := N) ((f : (a : M) → N) m : N)
        (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N))),
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N)
Tactic: rw [map_mul, ← mul_assoc n₁, eq₁, ← mul_assoc n₂, mul_right_comm n₂, eq₂] at eq ⊢
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq :
  HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N)) =
    HMul.hMul (α := N) ((f : (a : M) → N) m : N)
      (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N))
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₁.1 : N) ((f : (a : M) → N) (↑ms₂.2 : M) : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) ms₂.1 : N) ((f : (a : M) → N) (↑ms₁.2 : M) : N)
have simp_rw : ∀ (eq : ∃ (c : ↥S), (↑c : M) * (m * (ms₁.1 * (↑ms₂.2 : M))) = (↑c : M) * (m * (ms₂.1 * (↑ms₁.2 : M)))),
  ∃ (c : ↥S), (↑c : M) * (ms₁.1 * (↑ms₂.2 : M)) = (↑c : M) * (ms₂.1 * (↑ms₁.2 : M))
Tactic: simp_rw [← map_mul, eq_iff_exists] at eq ⊢
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : HMul.hMul (β := N) n₁ ((f : (a : M) → N) (↑ms₁.2 : M) : N) = (f : (a : M) → N) ms₁.1
ms₂ : M × ↥S
eq₂ : HMul.hMul (β := N) n₂ ((f : (a : M) → N) (↑ms₂.2 : M) : N) = (f : (a : M) → N) ms₂.1
eq : ∃ (c : ↥S), (↑c : M) * (m * (ms₁.1 * (↑ms₂.2 : M))) = (↑c : M) * (m * (ms₂.1 * (↑ms₁.2 : M)))
⊢ ∃ (c : ↥S), (↑c : M) * (ms₁.1 * (↑ms₂.2 : M)) = (↑c : M) * (ms₂.1 * (↑ms₁.2 : M))
have eq₃ : ∃ (c : ↥S), m * ((↑c : M) * (ms₁.1 * (↑ms₂.2 : M))) = m * ((↑c : M) * (ms₂.1 * (↑ms₁.2 : M)))
Tactic: simp_rw [mul_left_comm _ m] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
inst_2 : IsCancelMul M
⊢ IsCancelMul N
have simp_rw : ∀ (r : N), IsRightRegular r
Tactic: simp_rw [isCancelMul_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
inst_2 : IsCancelMul M
n : N
⊢ IsRightRegular n
have have : ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
  IsRightRegular n
Tactic: have ⟨ms, eq⟩ := f.surj n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
inst_2 : Subsingleton M
x y : N
⊢ x = y
have obtain : ∀ (mx : M) (sx : ↥S), f.mk' mx sx = y
Tactic: obtain ⟨mx, sx, rfl⟩ := f.mk'_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : CommMonoid M
S : Submonoid M
inst_1 : CommMonoid N
f : S.LocalizationMap N
inst_2 : Subsingleton M
y : N
mx : M
sx : ↥S
⊢ f.mk' mx sx = y
have obtain : ∀ (my : M) (sy : ↥S), f.mk' mx sx = f.mk' my sy
Tactic: obtain ⟨my, sy, rfl⟩ := f.mk'_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.DivPairs (goal)
Goal:
M : Type u_1
G : Type u_2
H : Type u_3
inst : CommMonoid M
inst_1 : CommGroup G
inst_2 : CommGroup H
f : LocalizationMap.{u_1, u_2} (M := M) ⊤ G
g : LocalizationMap.{u_1, u_3} (M := M) ⊤ H
s : Submonoid G
⊢ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s
have h : ∀ (x : M × M), x ∈ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) ↔ x ∈ divPairs f s
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Finite (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
inst_1 : Monoid.FG M
hS : S.FG
⊢ Monoid.FG.{u_1} (Localization S)
have hS₁ : Monoid.FG.{u_1} ↥S
Tactic: rw [← Monoid.fg_iff_submonoid_fg] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
a : GrothendieckGroup M
⊢ a⁻¹ * a = 1
have H : ∀ (y : M × ↥⊤), (mk y.1 y.2)⁻¹ * mk y.1 y.2 = 1
Tactic: cases a using ind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
⊢ (mk y.1 y.2)⁻¹ * mk y.1 y.2 = 1
have H : Submonoid.LocalizationMap.mk' (monoidOf ⊤) ((↑y.2 : M) * y.1)
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 sorry * y.2) =
  1
Tactic: rw [inv_mk, mk_eq_monoidOf_mk', ← Submonoid.LocalizationMap.mk'_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
⊢ Submonoid.LocalizationMap.mk' (monoidOf ⊤) ((↑y.2 : M) * y.1)
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) =
    1
have h : (↑y.2 : M) * y.1 = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 sorry * y.2) : M)
Tactic: convert! Submonoid.LocalizationMap.mk'_self' _ _
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
⊢ (↑y.2 : M) * y.1 = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
have h : y.1 * (↑y.2 : M) = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 sorry * y.2) : M)
Tactic: rw [mul_comm, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
y : M × ↥⊤
h : y.1 * (↑y.2 : M) = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
⊢ (↑y.2 : M) * y.1 = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 ⋯ * y.2) : M)
have h₁ : y.1 * (↑y.2 : M) = (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) y.1 sorry) : M) * (↑y.2 : M)
Tactic: rw [mul_comm, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
inst : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk m₁ s₁ / mk m₂ s₂ =
    mk (m₁ * (↑s₂ : M)) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) ((↑s₁ : M) * m₂) ⋯)
have simp : mk (m₁ * (↑s₂ : M)) (s₁ * Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) m₂ sorry) =
  mk (m₁ * (↑s₂ : M)) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) ⊤ x) ((↑s₁ : M) * m₂) sorry)
Tactic: simp [div_eq_mul_inv, mk_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
⊢ (fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of)
      ((fun (f : M →* G) ↦
          (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ : MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
        f) =
    f
have h : ∀ (x : M),
  Eq.{u_2 + 1} (α := G)
    (((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of)
            ((fun (f : M →* G) ↦
                (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) sorry :
                  MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
              f) :
          (a : M) → G)
        x :
      G)
    ((f : (a : M) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G
⊢ (fun (f : M →* G) ↦
        (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) ⋯ : MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
      ((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of) f) =
    f
have h : ∀ (x : Localization (M := M) ⊤),
  Eq.{u_2 + 1} (α := G)
    (((fun (f : M →* G) ↦
              (Submonoid.LocalizationMap.lift (monoidOf ⊤) (g := f) sorry :
                MonoidHom.{u_1, u_2} (Localization (M := M) ⊤) G))
            ((fun (f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) ↦ f.comp of) f) :
          (a : Localization ⊤) → G)
        x :
      G)
    ((f : (a : Localization ⊤) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup (goal)
Goal:
M : Type u_1
G : Type u_2
inst : CommMonoid M
inst_1 : CommGroup G
f : M →* G
x : GrothendieckGroup M
⊢ (((lift : (a : M →* G) → GrothendieckGroup M →* G) f : MonoidHom.{u_1, u_2} (GrothendieckGroup M) G) :
        (a : GrothendieckGroup M) → G)
      x =
    HDiv.hDiv (α := G) (β := G) ((f : (a : M) → G) (Submonoid.LocalizationMap.sec (monoidOf ⊤) x).1 : G)
      ((f : (a : M) → G) (↑(Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2 : M) : G)
have simp : Eq.{u_2 + 1} (α := G)
  ((↑((IsUnit.liftRight (f.restrict ⊤) sorry : (a : ↥⊤) → Gˣ) (Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2) : G) : G)
  ((f : (a : M) → G) (↑(Submonoid.LocalizationMap.sec (monoidOf ⊤) x).2 : M) : G)
Tactic: simp [lift, (monoidOf ⊤).lift_apply, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
have choose : ∀ (x : (z : N) → M × ↥S)
  (hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1),
  ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
Tactic: choose x hx using hf.surj
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
have have : ∀ (val : Fintype ι),
  ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
Tactic: have ⟨_⟩ := nonempty_fintype ι
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
⊢ ∃ (s : ↥S) (x : ι → M), ∀ (i : ι), HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) (x i)
have refine : ∀ (i : ι),
  HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: refine ⟨∏ i : ι, (x (n i)).2, fun i ↦ (x (n i)).1 * ∏ j ∈ univ.erase i, (x (n j)).2, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Lemmas (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst : Finite ι
inst_1 : CommMonoid M
inst_2 : CommMonoid N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
S : Submonoid M
hf : IsLocalizationMap.{u_1, u_2} (N := N) S (⇑f : (a : M) → N)
n : ι → N
x : (z : N) → M × ↥S
hx : ∀ (z : N), HMul.hMul (β := N) z ((f : (a : M) → N) (↑(x z).2 : M) : N) = (f : (a : M) → N) (x z).1
val : Fintype ι
i : ι
⊢ HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑(∏ i : ι, (x (n i)).2) : M) : N) =
    (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
have rw : HMul.hMul (β := N) (n i) ((f : (a : M) → N) (↑((x (n i)).2 * ∏ x_1 ∈ erase univ i, (x (n x_1)).2) : M) : N) =
  (f : (a : M) → N) ((fun (i : ι) ↦ (x (n i)).1 * (↑(∏ j ∈ erase univ i, (x (n j)).2) : M)) i)
Tactic: rw [← univ.mul_prod_erase _ (mem_univ i), S.coe_mul, map_mul, ← mul_assoc, hx, map_mul]