awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ IsLocalizedModule.mk' f (r • m) s = r • x
have rw : r • IsLocalizedModule.mk' f m s = r • x
Tactic: rw [IsLocalizedModule.mk'_smul, hx]
-- 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
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
rw : r • IsLocalizedModule.mk' f m s = r • x
⊢ IsLocalizedModule.mk' f (r • m) s = r • x
have rw₁ : r • x = r • x
Tactic: rw [IsLocalizedModule.mk'_smul, hx]
-- 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
M' M'' : Submodule R M
r : S
x : N
h : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ r • x ∈ (localized₀ p f M').carrier
have have : ∀ (y : R) (t : ↥p) (hyt : IsLocalization.mk' S y t = r), r • x ∈ (localized₀ p f M').carrier
Tactic: have ⟨y, t, hyt⟩ := IsLocalization.exists_mk'_eq p r
-- 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
M' : Submodule R M
⊢ Eq (α := Submodule S N) (localized' S p f M') (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
have refine : LE.le (α := Submodule S N) (localized' S p f M') (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
Tactic: refine le_antisymm ?_ (span_le.mpr <| by rintro _ ⟨m, hm, rfl⟩; exact ⟨m, hm, 1, by simp⟩)
-- 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
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ Membership.mem (γ := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑M' : Set M))) (IsLocalizedModule.mk' f m s)
have rw : Membership.mem (γ := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑M' : Set M)))
  (IsLocalization.mk' S 1 s • IsLocalizedModule.mk' (S := p) f m 1)
Tactic: rw [← one_smul R m, ← mul_one s, ← IsLocalizedModule.mk'_smul_mk' S]
-- 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
M'_1 M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun (x : Submodule S N) ↦ comap f (restrictScalars R x)) N'
⊢ localized' S p f M' ≤ N'
have rw : (⇑f : (a : M) → N) '' (↑M' : Set M) ⊆ (↑N' : Set N)
Tactic: rw [localized'_eq_span, span_le]
-- 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
M' M'' : Submodule R M
N' : Submodule S N
n : N
hn : n ∈ N'
⊢ Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N'))) n
have obtain : ∀ (m : M) (s : ↥p) (hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'),
  Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N')))
    (Function.uncurry (IsLocalizedModule.mk' f) (m, s))
Tactic: obtain ⟨⟨m, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f n
Cleared hypotheses: n, hn
-- 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
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ Membership.mem (γ := Submodule S N) (localized' S p f (comap f (restrictScalars R N')))
    (Function.uncurry (IsLocalizedModule.mk' f) (m, s))
have refine : m ∈ comap f (restrictScalars R N')
Tactic: refine ⟨m, ?_, s, rfl⟩
-- 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
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ m ∈ comap f (restrictScalars R N')
have rw : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) (IsLocalizedModule.mk' f m s) ∈ N'
Tactic: rw [mem_comap, restrictScalars_mem, ← IsLocalizedModule.mk'_cancel' _ _ s,
      Submonoid.smul_def, ← algebraMap_smul S]
-- 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
⊢ localized₀ p f ⊥ = ⊥
have rw : localized₀ p f ⊥ ≤ ⊥
Tactic: rw [← le_bot_iff]
-- 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
⊢ localized₀ p f ⊤ = ⊤
have rw : ⊤ ≤ localized₀ p f ⊤
Tactic: rw [← top_le_iff]
-- 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
x : N
h : Membership.mem (γ := Submodule R N) ⊤ x
⊢ x ∈ localized₀ p f ⊤
have obtain : ∀ (x : M) (s : ↥p),
  Membership.mem (γ := Submodule R N) ⊤ (Function.uncurry (IsLocalizedModule.mk' f) (x, s)) →
    Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
Cleared hypotheses: x, 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
M' M'' : Submodule R M
⊢ localized₀ p f (M' ⊓ M'') = localized₀ p f M' ⊓ localized₀ p f M''
have simp : ∀ (x : N),
  (∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ↔
    (∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
Tactic: simp only [Submodule.ext_iff, Submodule.mem_inf, mem_localized₀]
-- 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
M' M'' : Submodule R M
⊢ ∀ (x : N),
    (∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ↔
      (∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have refine : ∀ (x : N),
  ((∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x) →
    ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
Tactic: refine fun x ↦ ⟨by grind, ?_⟩
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have h : IsLocalizedModule.mk' f j t = IsLocalizedModule.mk' f i s
Tactic: have h := ht.trans hs.symm
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
h : IsLocalizedModule.mk' f j t = IsLocalizedModule.mk' f i s
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have h₁ : ∃ (s_1 : ↥p), s_1 • t • i = s_1 • s • j
Tactic: rw [IsLocalizedModule.mk'_eq_mk'_iff] 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
h : ∃ (s_1 : ↥p), s_1 • t • i = s_1 • s • j
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have obtain : ∀ (k : ↥p) (hk : k • t • i = k • s • j), ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
Tactic: obtain ⟨k, hk⟩ := 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have refine_1 : (k * t) • i ∈ M''
Tactic: refine ⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_1 : (k * t) • i ∈ M''
⊢ ∃ (m : M), (m ∈ M' ∧ m ∈ M'') ∧ ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x
have refine_2 : IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
Tactic: refine ⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * t) • i ∈ M''
have refine_1 : (k * s) • j ∈ M''
Tactic: rw [mul_smul, hk, smul_smul]
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
have refine_2 : IsLocalizedModule.mk' f (k • t • i) (k * s * t) = x
Tactic: rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_2 : IsLocalizedModule.mk' f (k • t • i) (k * s * t) = x
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
have refine_2₁ : IsLocalizedModule.mk' f (k • s • j) (k * s * t) = x
Tactic: rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]
-- 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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
refine_2 : IsLocalizedModule.mk' f (k • t • i) (k * s * t) = x
refine_2₁ : IsLocalizedModule.mk' f (k • s • j) (k * s * t) = x
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
have refine_2₂ : IsLocalizedModule.mk' f ((k * s) • j) (k * s * t) = x
Tactic: rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]
-- 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
ι : Type u_5
g : ι → Submodule R M
this : Module.{u_1, u_4} (Localization (M := R) p) N := IsLocalizedModule.module p f
⊢ localized₀ p f (⨆ (i : ι), g i) = ⨆ (i : ι), localized₀ p f (g i)
have this₁ : IsScalarTower R (Localization (M := R) p) N
Tactic: have : IsScalarTower R (Localization p) N := IsLocalizedModule.isScalarTower_module p f
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)
have rw : localized₀ p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)) = sSup (localized₀ p f '' s)
Tactic: rw [sSup_eq_iSup', localized₀_iSup, sSup_image']
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
rw : localized₀ p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)) = sSup (localized₀ p f '' s)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)
have rw₁ : ⨆ (i : (↑s : Type u_3)), localized₀ p f (↑i : Submodule R M) = sSup (localized₀ p f '' s)
Tactic: rw [sSup_eq_iSup', localized₀_iSup, sSup_image']
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
rw : localized₀ p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)) = sSup (localized₀ p f '' s)
rw₁ : ⨆ (i : (↑s : Type u_3)), localized₀ p f (↑i : Submodule R M) = sSup (localized₀ p f '' s)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)
have rw₂ : Eq.{u_4 + 1} (α := Submodule R N) (⨆ (i : (↑s : Type u_3)), localized₀ p f (↑i : Submodule R M))
  (⨆ (a : (↑s : Type u_3)), localized₀ p f (↑a : Submodule R M))
Tactic: rw [sSup_eq_iSup', localized₀_iSup, sSup_image']
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ Eq (α := Submodule S N) (localized' S p f (sSup s)) (sSup (localized' S p f '' s))
have rw : Eq (α := Submodule S N) (localized' S p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)))
  (sSup (localized' S p f '' s))
Tactic: rw [sSup_eq_iSup', localized'_iSup, sSup_image']
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
rw :
  Eq (α := Submodule S N) (localized' S p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)))
    (sSup (localized' S p f '' s))
⊢ Eq (α := Submodule S N) (localized' S p f (sSup s)) (sSup (localized' S p f '' s))
have rw₁ : Eq (α := Submodule S N) (⨆ (i : (↑s : Type u_3)), localized' S p f (↑i : Submodule R M)) (sSup (localized' S p f '' s))
Tactic: rw [sSup_eq_iSup', localized'_iSup, sSup_image']
-- 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
M' M'' : Submodule R M
s : Set (Submodule R M)
rw :
  Eq (α := Submodule S N) (localized' S p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)))
    (sSup (localized' S p f '' s))
rw₁ :
  Eq (α := Submodule S N) (⨆ (i : (↑s : Type u_3)), localized' S p f (↑i : Submodule R M))
    (sSup (localized' S p f '' s))
⊢ Eq (α := Submodule S N) (localized' S p f (sSup s)) (sSup (localized' S p f '' s))
have rw₂ : Eq.{u_4 + 1} (α := Submodule S N) (⨆ (i : (↑s : Type u_3)), localized' S p f (↑i : Submodule R M))
  (⨆ (a : (↑s : Type u_3)), localized' S p f (↑a : Submodule R M))
Tactic: rw [sSup_eq_iSup', localized'_iSup, sSup_image']
-- 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
s : Set M
⊢ Eq (α := Submodule S N) (localized' S p f (span R s)) (span S ((⇑f : (a : M) → N) '' s))
have rw : Eq.{u_4 + 1} (α := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑(span R s) : Set M)))
  (span S ((⇑f : (a : M) → N) '' s))
Tactic: rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]
-- 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
s : Set M
rw :
  Eq.{u_4 + 1} (α := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑(span R s) : Set M)))
    (span S ((⇑f : (a : M) → N) '' s))
⊢ Eq (α := Submodule S N) (localized' S p f (span R s)) (span S ((⇑f : (a : M) → N) '' s))
have rw₁ : Eq (α := Submodule S N) (span S (↑(map f (span R s)) : Set N)) (span S ((⇑f : (a : M) → N) '' s))
Tactic: rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]