awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
m n : M
e :
  Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((Submodule.toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
x : M
hx : x ∈ M'
s : ↥p
hs : mk' f x s = (f : (a : M) → N) (m - n)
c : ↥p
hc : c • s • (m - n) = c • x
⊢ ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)

Tactic:
exact ⟨c * s, by simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
      ← smul_sub, mul_smul, hc] using M'.smul_mem c hx⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
⊢ IsLocalizedModule p (Submodule.toLocalizedQuotient p M')

Tactic:
IsLocalizedModule.toLocalizedQuotient' _ _ _ _

Premises used: IsLocalizedModule.toLocalizedQuotient'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
h :
  ∀ (x : N),
    Membership.mem (γ := Submodule R N)
        (ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
        x ↔
      x ∈ localized₀ p f g.ker
⊢ ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g) =
    localized₀ p f g.ker

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ Eq.{u_6 + 1} (α := Q)
      ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) x : Q) (0 : Q) ↔
    ∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
h :
  ∀
    (h :
      Eq.{u_6 + 1} (α := Q)
        ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) x : Q) (0 : Q)),
    ∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x
h₁ :
  (∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x) →
    Eq.{u_6 + 1} (α := Q)
      ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) x : Q) (0 : Q)
⊢ Eq.{u_6 + 1} (α := Q)
      ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) x : Q) (0 : Q) ↔
    ∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
h :
  Eq.{u_6 + 1} (α := Q)
    ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) x : Q) (0 : Q)
h₁ :
  ∀ (a : M) (b : ↥p)
    (h :
      Eq.{u_6 + 1} (α := Q)
        ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q)
            (Function.uncurry (mk' f) (a, b)) :
          Q)
        (0 : Q)),
    ∃ (m : M),
      Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = Function.uncurry (mk' f) (a, b)
⊢ ∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x

Tactic:
obtain ⟨⟨a, b⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b : ↥p
h :
  Eq.{u_6 + 1} (α := Q)
    ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q)
        (Function.uncurry (mk' f) (a, b)) :
      Q)
    (0 : Q)
⊢ ∃ (s' : ↥p), HSMul.hSMul (β := P) s' ((g : (a : M) → P) a : P) = 0

Tactic:
simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_zero, eq_zero_iff p f'] at h

Premises used: IsLocalizedModule.map_mk', Function.uncurry_apply_pair, IsLocalizedModule.mk'_eq_zero, IsLocalizedModule.eq_zero_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b : ↥p
h : ∃ (s' : ↥p), HSMul.hSMul (β := P) s' ((g : (a : M) → P) a : P) = 0
h₁ :
  ∀ (c : ↥p) (hc : HSMul.hSMul (β := P) c ((g : (a : M) → P) a : P) = 0),
    ∃ (m : M),
      Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = Function.uncurry (mk' f) (a, b)
⊢ ∃ (m : M),
    Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = Function.uncurry (mk' f) (a, b)

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b c : ↥p
hc : HSMul.hSMul (β := P) c ((g : (a : M) → P) a : P) = 0
⊢ Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) (c • a) : P) (0 : P)

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b c : ↥p
hc : HSMul.hSMul (β := P) c ((g : (a : M) → P) a : P) = 0
⊢ mk' f (c • a) (c * b) = Function.uncurry (mk' f) (a, b)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b c : ↥p
hc : HSMul.hSMul (β := P) c ((g : (a : M) → P) a : P) = 0
⊢ ∃ (m : M),
    Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = Function.uncurry (mk' f) (a, b)

Tactic:
refine ⟨c • a, by simpa, c * b, by simp⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
m : M
hm : Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P)
a : ↥p
⊢ Eq.{u_6 + 1} (α := Q)
    ((((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g : N →ₗ[R] Q) : (a : N) → Q) (mk' f m a) : Q)
    (0 : Q)

Tactic:
simp [IsLocalizedModule.map_mk', hm]

Premises used: IsLocalizedModule.map_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ∀ (x : N),
    Membership.mem (γ := Submodule S N) (localized' S p f g.ker) x ↔
      Membership.mem (γ := Submodule S N)
        (ker.{u_2, u_2, u_4, u_6} (M₂ := Q)
          (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g)))
        x

Tactic:
apply SetLike.ext_iff.mp (f.ker_localizedMap_eq_localized₀_ker p f' g).symm

Premises used: LinearMap.ker_localizedMap_eq_localized₀_ker, SetLike.ext_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
h :
  ∀ (x : N),
    Membership.mem (γ := Submodule R N)
        (ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
        x ↔
      Membership.mem (γ := Submodule R N) (Submodule.restrictScalars R (localized' S p f g.ker)) x
⊢ Eq (α := Submodule R N)
    (ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
    (Submodule.restrictScalars R (localized' S p f g.ker))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ Membership.mem (γ := Submodule R N)
      (ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
      x ↔
    Membership.mem (γ := Submodule R N) (Submodule.restrictScalars R (localized' S p f g.ker)) x

Tactic:
simp [localized'_ker_eq_ker_localizedMap S p f f']

Premises used: LinearMap.localized'_ker_eq_ker_localizedMap
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : M
hx : x ∈ g.ker
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := Submodule R N)
    (ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
    ((f : (a : M) → N) x : N)

Tactic:
simp [mem_ker, mem_ker.mp hx]

Premises used: LinearMap.mem_ker, Iff.mp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ IsLocalizedModule (M' :=
    ↥(ker.{u_1, u_1, u_4, u_6} (R₂ := R) (M₂ := Q) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g)))
    p (toKerIsLocalized p f f' g)

Tactic:
let e : Submodule.localized' S p f (ker g) ≃ₗ[S]
      ker ((map p f f' g).extendScalarsOfIsLocalization p S) :=
    LinearEquiv.ofEq _ _ (localized'_ker_eq_ker_localizedMap S p f f' g)
  IsLocalizedModule.of_linearEquiv p (Submodule.toLocalized' S p f (ker g)) (e.restrictScalars R)

Premises used: Submodule.toLocalized', LinearMap.extendScalarsOfIsLocalization, Set.Mem, LinearEquiv.restrictScalars, LinearMap.ker, LinearMap.localized'_ker_eq_ker_localizedMap, IsLocalizedModule.lift, LocalizedModule.liftOn, LinearMap.toKerIsLocalized, LinearMap.restrict, Submodule.localized', LinearEquiv.ofEq, Submodule.comap, IsLocalizedModule.map, LinearMap.codRestrict, LocalizedModule.lift', IsLocalizedModule.of_linearEquiv, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
h :
  ∀ (x : Q),
    Membership.mem (γ := Submodule R Q)
        (range.{u_1, u_1, u_4, u_6} (R := R) (M := N) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
        x ↔
      x ∈ localized₀ p f' g.range
⊢ range.{u_1, u_1, u_4, u_6} (R := R) (M := N) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g) =
    localized₀ p f' g.range

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
x : Q
⊢ Membership.mem (γ := Submodule R Q)
      (range.{u_1, u_1, u_4, u_6} (R := R) (M := N) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
      x ↔
    x ∈ localized₀ p f' g.range

Tactic:
simp [mem_localized₀, mem_range, (mk'_surjective p f).exists]

Premises used: Function.Surjective.exists, IsLocalizedModule.mk'_surjective, LinearMap.mem_range, Submodule.mem_localized₀
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P : Type u_5
inst_11 : AddCommMonoid P
inst_12 : Module R P
Q : Type u_6
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : Module S Q
inst_16 : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst_17 : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ∀ (x : Q),
    Membership.mem (γ := Submodule S Q) (localized' S p f' g.range) x ↔
      Membership.mem (γ := Submodule S Q)
        (range.{u_2, u_2, u_4, u_6} (M := N)
          (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g)))
        x

Tactic:
apply SetLike.ext_iff.mp (f.range_localizedMap_eq_localized₀_range p f' g).symm

Premises used: SetLike.ext_iff, Iff.mp, Eq.symm, LinearMap.range_localizedMap_eq_localized₀_range
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
inst : AddCommMonoid M
⊢ Eq (α := (x : ℕ) → M →+ M) (toAddMonoidHom M) nsmulAddMonoidHom

Tactic:
rfl

Premises used: nsmulAddMonoidHom, DistribSMul.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
inst : AddCommGroup M
⊢ Eq (α := (x : ℤ) → M →+ M) (toAddMonoidHom M : (x : ℤ) → M →+ M) (zsmulAddGroupHom : (n : ℤ) → M →+ M)

Tactic:
rfl

Premises used: zsmulAddGroupHom, DistribSMul.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) a = 0

Tactic:
simpa only [Int.cast_zero] using zero_smul R a

Premises used: Int.cast_zero, zero_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
z : ℕ
a : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(↑z.succ : ℤ) : R) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(↑z : ℤ) : R) a + a

Tactic:
simp [add_comm, add_smul]

Premises used: add_comm, add_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
z : ℕ
a : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(Int.negSucc z) : R) a =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(↑z.succ : ℤ) : R) a)

Tactic:
simp [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
nth_rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + a = 0

Tactic:
nth_rw 2 [← one_smul R a]

Premises used: one_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
rw : HAdd.hAdd (α := R) (-1) 1 • a = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0

Tactic:
rw [← add_smul, neg_add_cancel, zero_smul]

Premises used: zero_smul, neg_add_cancel, add_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b = HSMul.hSMul (α := ℕ) 0 b
zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 b
zero₂ zero₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b

Tactic:
rw [Nat.cast_zero, zero_smul, zero_smul]

Premises used: zero_smul, Nat.cast_zero
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
succ₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b =
    n • b + HSMul.hSMul (α := ℕ) 1 b
succ₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
succ₄ : n • b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
succ₅ succ₆ : n • b + b = n • b + b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b

Tactic:
rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

Premises used: Nat.cast_succ, one_smul, add_smul