awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₁ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₂ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S (↑x : R) x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₃ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa₄ : ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (m - n)),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₁ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₂ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S (↑x : R) x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₃ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₄ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (m - n)),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa₅ : ∀
  (e :
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
y : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
⊢ ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    x.2 • y =
      ((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')
        x.1
have obtain : ∀ (y : N),
  ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2 (Submodule.Quotient.mk y) =
      ((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')
        x.1
Tactic: obtain ⟨y, rfl⟩ := mk_surjective _ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
y : N
⊢ ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2 (Submodule.Quotient.mk y) =
      ((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')
        x.1
have obtain : ∀ (y : M) (s : ↥p),
  ∃ (x : Prod.{u_7, u_5} (M ⧸ M') ↥p),
    HSMul.hSMul (β := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) x.2
        (Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s))) =
      ((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')
        x.1
Tactic: obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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 ⧸ 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')
        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')
        n :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
⊢ ∃ (c : ↥p), c • m = c • n
have obtain : ∀ (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'))),
  ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
Tactic: obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
Cleared hypotheses: m, n, e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'))
⊢ ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
have obtain : ∀ (x : M) (hx : x ∈ M') (s : ↥p) (hs : mk' f x s = (f : (a : M) → N) (m - n)),
  ∃ (c : ↥p),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
Tactic: obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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),
    HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk m) = HSMul.hSMul (β := M ⧸ M') c (Submodule.Quotient.mk n)
have obtain : ∀ (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: obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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
have 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)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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)
⊢ ∃ (m : M), Eq.{u_5 + 1} (α := P) ((g : (a : M) → P) m : P) (0 : P) ∧ ∃ (s : ↥p), mk' f m s = x
have 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)
Tactic: obtain ⟨⟨a, b⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (hypothesis)
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)
⊢ ∃ (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)
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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))
have 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
Tactic: ext