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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
⊢ a = b
have obtain : ∀ (y : M) (n : ↥S) (hym : n • b = (f : (a : M) → M') y), a = b
Tactic: obtain ⟨⟨y, n⟩, (hym : n • b = f y)⟩ := IsLocalizedModule.surj S f b
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') ((↑n : R) • x) : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') ((↑m : R) • y) : M') : N)
⊢ a = b
have h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑n : R) • x) : M') ((f : (a : M) → M') ((↑m : R) • y) : M')
Tactic: apply H at h
Cleared hypotheses: h
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑n : R) • x) : M') ((f : (a : M) → M') ((↑m : R) • y) : M')
⊢ a = b
have h₁ : HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') = HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
Tactic: rw [map_smul, map_smul] 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
⊢ a = b
have rwa : (n * m) • a = (n * m) • b
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
⊢ a = b
have rwa₁ : n • m • a = (n * m) • b
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
rwa₁ : n • m • a = (n * m) • b
⊢ a = b
have rwa₂ : n • m • a = (m * n) • b
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
rwa₁ : n • m • a = (n * m) • b
rwa₂ : n • m • a = (m * n) • b
⊢ a = b
have rwa₃ : n • m • a = m • n • b
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
rwa₁ : n • m • a = (n * m) • b
rwa₂ : n • m • a = (m * n) • b
rwa₃ : n • m • a = m • n • b
⊢ a = b
have rwa₄ : HSMul.hSMul (β := M') n ((f : (a : M) → M') x : M') = m • n • b
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
rwa₁ : n • m • a = (n * m) • b
rwa₂ : n • m • a = (m * n) • b
rwa₃ : n • m • a = m • n • b
rwa₄ : HSMul.hSMul (β := M') n ((f : (a : M) → M') x : M') = m • n • b
⊢ a = b
have rwa₅ : HSMul.hSMul (β := M') n ((f : (a : M) → M') x : M') = HSMul.hSMul (β := M') m ((f : (a : M) → M') y : M')
Tactic: rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
⊢ a = b
have suffices : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') ((↑n : R) • x) : M') : N)
  ((g : (a : M') → N) ((f : (a : M) → M') ((↑m : R) • y) : M') : N)
Tactic: suffices h : g (f (n.val • x)) = g (f (m.val • y)) by
    apply H at h
    rw [map_smul, map_smul] at h
    rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
⊢ Function.Injective.{u_7 + 1, u_8 + 1} (α := M') (β := N) (⇑g : (a : M') → N)
have refine : ∀ {x y : M}
  (hxy :
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
      ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N)),
  Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
Tactic: refine IsLocalizedModule.injective_of_map_eq S f (fun hxy ↦ ?_)
-- 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_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
x y : M
hxy :
  Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N)
⊢ Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
have rw : Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') (x - y) : M') (0 : M')
Tactic: rw [← sub_eq_zero, ← map_sub]
-- 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_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
x y : M
hxy :
  Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N)
⊢ Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') (x - y) : M') (0 : M')
have a : Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') (x - y) : M') : N) (0 : N)
Tactic: apply 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_1 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
h₁ h₂ : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (h₁ + h₂)) ⋯ = lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯
have h : lift S f (g ∘ₗ (h₁ + h₂)) sorry ∘ₗ f = (lift S f (g ∘ₗ h₁) sorry + lift S f (g ∘ₗ h₂) sorry) ∘ₗ f
Tactic: apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
-- 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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift S f (g ∘ₗ h) ⋯)
have h₁ : lift S f (g ∘ₗ (r • h)) sorry ∘ₗ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift S f (g ∘ₗ h) sorry) ∘ₗ f
Tactic: apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') (mk' f x s) =
    mk' g ((h : (a : M) → N) x) s
have simp : (LocalizedModule.lift S (g ∘ₗ h) sorry : (a : LocalizedModule S M) → N')
    (((iso S f).symm : (a : M') → LocalizedModule S M) (mk' f x s) : LocalizedModule S M) =
  mk' g ((h : (a : M) → N) x) s
Tactic: simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯ : (a : LocalizedModule S M) → N')
      (((iso S f).symm : (a : M') → LocalizedModule S M) (mk' f x s) : LocalizedModule S M) =
    mk' g ((h : (a : M) → N) x) s
have rw : ((↑sorry.unit⁻¹ : End R N') : (a : N') → N') ((g ∘ₗ h : (a : M) → N') x : N') = mk' g ((h : (a : M) → N) x) s
Tactic: rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
⊢ Eq.{u_3 + 1} (α := M' →ₗ[R] M') ((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')
have h : ∀ (x : M'),
  Eq (α := M') ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M') x : M')
    ((LinearMap.id : (a : M') → M') x : M')
Tactic: ext 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x : M'
⊢ Eq (α := M') ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M') x : M')
    ((LinearMap.id : (a : M') → M') x : M')
have h : ∀ (x : M) (s : ↥S),
  Eq (α := M')
    ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M')
        (Function.uncurry (mk' f) (x, s)) :
      M')
    ((LinearMap.id : (a : M') → M') (Function.uncurry (mk' f) (x, s)) : M')
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
Cleared hypotheses: 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x y : M'
⊢ Eq.{u_7 + 1} (α := N') ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') x : N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
    x = y
have obtain : ∀ (x : M) (s : ↥S),
  Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
    Function.uncurry (mk' f) (x, s) = y
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
Cleared hypotheses: 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
y : M'
x : M
s : ↥S
⊢ Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
    Function.uncurry (mk' f) (x, s) = y
have obtain : ∀ (y : M) (t : ↥S),
  Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (y, t)) :
        N') →
    Function.uncurry (mk' f) (x, s) = Function.uncurry (mk' f) (y, t)
Tactic: obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
Cleared hypotheses: y
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : M
s : ↥S
y : M
t : ↥S
⊢ Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (y, t)) :
        N') →
    Function.uncurry (mk' f) (x, s) = Function.uncurry (mk' f) (y, t)
have simp : ∀ x_1 ∈ S,
  x_1 • HSMul.hSMul (β := N) s ((h : (a : M) → N) y : N) = x_1 • HSMul.hSMul (β := N) t ((h : (a : M) → N) x : N) →
    ∃ a ∈ S, a • s • y = a • t • x
Tactic: simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_mk'_iff, Subtype.exists,
    Submonoid.mk_smul, exists_prop, forall_exists_index, and_imp]
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : N'
⊢ ∃ (a : M'), (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a = x
have obtain : ∀ (x : N) (s : ↥S),
  ∃ (a : M'),
    (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a = Function.uncurry (mk' g) (x, s)
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x
Cleared hypotheses: x