awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
have c : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
  HMul.hMul (α := T)
    (liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      sorry (r₁ /ₒ s₁))
    (liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      sorry (r₂ /ₒ s₂))
Tactic: rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
have c₁ : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
    liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      sorry (r₂ /ₒ s₂)
Tactic: rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
c₁ :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂)
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
have c₂ : HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
Tactic: rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
c₁ :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂)
c₂ :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
have c₃ : (f : (a : R) → T) (ra * r₂) =
  (↑((fS : (a : ↥S) → Tˣ) (sa * s₁)) : T) *
    (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
Tactic: rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
⊢ φ = universalMulHom f fS hf
have h : ∀ (x : OreLocalization S R),
  Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) x : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) x : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
x : OreLocalization S R
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) x : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) x : T)
have h : ∀ (r : R) (s : ↥S),
  Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
Tactic: cases x with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h : (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₁ : (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
    ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₂ : (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₃ : HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₃ :
  HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₄ : HMul.hMul (α := T) (β := T) ((↑1 : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₃ :
  HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₄ :
  HMul.hMul (α := T) (β := T) ((↑1 : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₅ : HMul.hMul (β := T)
    (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ)) : T)
    ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₃ :
  HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₄ :
  HMul.hMul (α := T) (β := T) ((↑1 : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₅ :
  HMul.hMul (β := T)
      (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ)) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₆ : HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s) : T))
    ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]