awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw : p.2 • x =
  Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₄ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₄ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₅ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') (↑p.2 : R) ((e.symm : (a : M'') → M') x : M'))
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₄ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₅ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') (↑p.2 : R) ((e.symm : (a : M'') → M') x : M'))
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₆ : (↑p.2 : R) • x = HSMul.hSMul (β := M'') (↑p.2 : R) ((e : (a : M') → M'') ((e.symm : (a : M'') → M') x : M') : M'')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₄ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₅ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') (↑p.2 : R) ((e.symm : (a : M'') → M') x : M'))
rw₆ : (↑p.2 : R) • x = HSMul.hSMul (β := M'') (↑p.2 : R) ((e : (a : M') → M'') ((e.symm : (a : M'') → M') x : M') : M'')
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1
have rw₇ : (↑p.2 : R) • x = (↑p.2 : R) • x
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁ x₂ : M
h :
  Eq.{u_4 + 1} (α := M'') (((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x₁ : M'')
    (((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x₂ : M'')
⊢ ∃ (c : ↥S), c • x₁ = c • x₂
have h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
Tactic: simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      EmbeddingLike.apply_eq_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
⊢ ∃ (x_1 : Prod.{u_4, u_1} M'' ↥S), x_1.2 • x = (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') x_1.1
have obtain : ∀ (p : M) (s : ↥S) (h : (p, s).2 • x = (f : (a : M) → M') (p, s).1),
  ∃ (x_1 : Prod.{u_4, u_1} M'' ↥S), x_1.2 • x = (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') x_1.1
Tactic: obtain ⟨⟨p, s⟩, h⟩ := hf.surj x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁ x₂ : M''
h :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((e : (a : M'') → M) x₁ : M) : M')
    ((f : (a : M) → M') ((e : (a : M'') → M) x₂ : M) : M')
⊢ ∃ (c : ↥S), c • x₁ = c • x₂
have obtain : ∀ (c : ↥S)
  (hc : HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₁ : M) = HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₂ : M)),
  ∃ (c : ↥S), c • x₁ = c • x₂
Tactic: obtain ⟨c, hc⟩ := hf.exists_of_eq h
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
inst_5 : IsLocalization S R'
inst_6 : Module R' M
inst_7 : IsScalarTower R R' M
s : ↥S
⊢ IsUnit.{u_2} (M := End R M) ((algebraMap R (End R M) : (a : R) → End R M) (↑s : R) : End R M)
have rw : IsUnit.{u_2} (M := End R M)
  ((Algebra.lsmul R R M : (a : R') → End R M) ((algebraMap R R' : (a : R) → R') (↑s : R)) : End R M)
Tactic: rw [← (Algebra.lsmul R (A := R') R M).commutes]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : c • (m', s').2 • (m, s).1 = c • (m, s).2 • (m', s').1
⊢ Eq.{u_4 + 1} (α := M'')
    ((fun (p : Prod.{u_2, u_1} M ↥S) ↦
        (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑p.2 : R)) ⋯)⁻¹ : End R M'') :
              (a : M'') → M'')
            ((g : (a : M) → M'') p.1 : M'') :
          M''))
      (m, s))
    ((fun (p : Prod.{u_2, u_1} M ↥S) ↦
        (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑p.2 : R)) ⋯)⁻¹ : End R M'') :
              (a : M'') → M'')
            ((g : (a : M) → M'') p.1 : M'') :
          M''))
      (m', s'))
have dsimp : Eq (α := M'')
  (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R)) sorry)⁻¹ : End R M'') : (a : M'') → M'')
      ((g : (a : M) → M'') m : M'') :
    M'')
  (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s' : R)) sorry)⁻¹ : End R M'') :
        (a : M'') → M'')
      ((g : (a : M) → M'') m' : M'') :
    M'')
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
⊢ Eq (α := M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m : M'') :
      M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s' : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m' : M'') :
      M'')
have rw : HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
  HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, eq_comm,
      Module.End.algebraMap_isUnit_inv_apply_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')
have this : c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
  c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
Tactic: have : c • s • g m' = c • s' • g m := by
      simp only [Submonoid.smul_def, ← g.map_smul, eq1]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')
have this₁ : Function.Injective (α := M'') (β := M'') (⇑sorry.unit.inv : (a : M'') → M'')
Tactic: have : Function.Injective (h c).unit.inv := ((Module.End.isUnit_iff _).1 (by simp)).1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')
have apply_fun : Eq (α := M'')
  ((sorry.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')) : M'')
  ((sorry.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) : M'')
Tactic: apply_fun (h c).unit.inv
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
⊢ Eq (α := M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')) : M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) : M'')
have rw : HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
  ((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'')
    ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M''))
Tactic: rw [Units.inv_eq_val_inv, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ←
      (h c).unit⁻¹.val.map_smul]