awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
have rw : Eq (α := LocalizedModule S M₂)
  ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
              (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
            h :
          LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
        (a : LocalizedModule S M₁) → LocalizedModule S M₂)
      ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
          (a : LocalizedModule S M₀) → LocalizedModule S M₁)
        (mk m s)) :
    LocalizedModule S M₂)
  (0 : LocalizedModule S M₂)
Tactic: rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
rw :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
              LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
            (a : LocalizedModule S M₀) → LocalizedModule S M₁)
          (mk m s)) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
have rw₁ : Eq (α := LocalizedModule S M₂)
  ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
              (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
            h :
          LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
        (a : LocalizedModule S M₁) → LocalizedModule S M₂)
      (mk ((g : (a : M₀) → M₁) m) s) :
    LocalizedModule S M₂)
  (0 : LocalizedModule S M₂)
Tactic: rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
rw :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
              LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
            (a : LocalizedModule S M₀) → LocalizedModule S M₁)
          (mk m s)) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₁ :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
have rw₂ : Eq (α := LocalizedModule S M₂) (mk ((h : (a : M₁) → M₂) ((g : (a : M₀) → M₁) m : M₁)) s : LocalizedModule S M₂)
  (0 : LocalizedModule S M₂)
Tactic: rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
rw :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
              LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
            (a : LocalizedModule S M₀) → LocalizedModule S M₁)
          (mk m s)) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₁ :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₂ :
  Eq (α := LocalizedModule S M₂) (mk ((h : (a : M₁) → M₂) ((g : (a : M₀) → M₁) m : M₁)) s : LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
have rw₃ : Eq (α := LocalizedModule S M₂) (mk 0 s) 0
Tactic: rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
rw :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
              LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
            (a : LocalizedModule S M₀) → LocalizedModule S M₁)
          (mk m s)) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₁ :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₂ :
  Eq (α := LocalizedModule S M₂) (mk ((h : (a : M₁) → M₂) ((g : (a : M₀) → M₁) m : M₁)) s : LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₃ : Eq (α := LocalizedModule S M₂) (mk 0 s) 0
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
have rw₄ : Eq (α := LocalizedModule S M₂) 0 0
Tactic: rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
hx : IsInteger f x
⊢ IsInteger f (a • x)
have rcases : ∀ (x' : M) (hx : (f : (a : M) → M') x' = x), IsInteger f (a • x)
Tactic: rcases hx with ⟨x', hx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : (f : (a : M) → M') x' = x
⊢ IsInteger f (a • x)
have h : (f : (a : M) → M') (a • x') = a • x
Tactic: use a • x'
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : (f : (a : M) → M') x' = x
⊢ (f : (a : M) → M') (a • x') = a • x
have h : (f : (a : M) → M') (a • x') = HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M')
Tactic: rw [← hx, LinearMapClass.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : (f : (a : M) → M') x' = x
h : (f : (a : M) → M') (a • x') = HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M')
⊢ (f : (a : M) → M') (a • x') = a • x
have h₁ : HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M') = HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M')
Tactic: rw [← hx, LinearMapClass.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
have choose : ∀ (sec : (i : ι) → Prod.{u_2, u_1} M ↥S) (hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1),
  ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
Tactic: choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
have refine_1 : (i : ι) → (hi : i ∈ s) → M
Tactic: refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
refine_1 : (i : ι) → (hi : i ∈ s) → M
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
have refine_2 : ∀ (i : ι) (hi : i ∈ s),
  (f : (a : M) → M') (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) (∏ j ∈ s.erase i, (sec j).2) (sec i).1) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ i ∈ s, (sec i).2) : R) (g i)
Tactic: refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
⊢ (f : (a : M) → M') (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) (∏ j ∈ s.erase i, (sec j).2) (sec i).1) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(∏ i ∈ s, (sec i).2) : R) (g i)
have refine_2 : HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') (∏ j ∈ s.erase i, (sec j).2) ((f : (a : M) → M') (sec i).1 : M') =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ i ∈ s, (↑(sec i).2 : R)) (g i)
Tactic: simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finsetProd]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') (∏ j ∈ s.erase i, (sec j).2) ((f : (a : M) → M') (sec i).1 : M') =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ i ∈ s, (↑(sec i).2 : R)) (g i)
have refine_2 : (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) • g i =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ i ∈ s, (↑(sec i).2 : R)) (g i)
Tactic: rw [← hsec, ← mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
⊢ (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) • g i =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ i ∈ s, (↑(sec i).2 : R)) (g i)
have refine_2 : (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) = ∏ i ∈ s, (↑(sec i).2 : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
⊢ (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) = ∏ i ∈ s, (↑(sec i).2 : R)
have refine_2 : (↑(sec i).2 : R) * ∏ i ∈ s.erase i, (↑(sec i).2 : R) = ∏ i ∈ s, (↑(sec i).2 : R)
Tactic: simp only [Submonoid.coe_mul, Submonoid.coe_finsetProd, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
⊢ (↑(sec i).2 : R) * ∏ i ∈ s.erase i, (↑(sec i).2 : R) = ∏ i ∈ s, (↑(sec i).2 : R)
have refine_2 : Eq.{u_1 + 1} (α := R) (∏ x ∈ insert i (s.erase i), (↑(sec x).2 : R)) (∏ i ∈ s, (↑(sec i).2 : R))
Tactic: rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),
      Finset.insert_erase hi]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : (i : ι) → Prod.{u_2, u_1} M ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1
i : ι
hi : i ∈ s
refine_2 : Eq.{u_1 + 1} (α := R) (∏ x ∈ insert i (s.erase i), (↑(sec x).2 : R)) (∏ i ∈ s, (↑(sec i).2 : R))
⊢ (↑(sec i).2 : R) * ∏ i ∈ s.erase i, (↑(sec i).2 : R) = ∏ i ∈ s, (↑(sec i).2 : R)
have refine_2₁ : Eq.{u_1 + 1} (α := R) (∏ x ∈ s, (↑(sec x).2 : R)) (∏ i ∈ s, (↑(sec i).2 : R))
Tactic: rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),
      Finset.insert_erase hi]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
have choose : ∀ (sec : (i : ι) → Prod.{u_2, u_1} M ↥S) (hsec : ∀ (i : ι), (sec i).2 • g i = (f : (a : M) → M') (sec i).1),
  ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
Tactic: classical
  choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))
  refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩
  · exact (∏ j ∈ s.erase i, (sec j).2) • (sec i).1
  · simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finsetProd]
    rw [← hsec, ← mul_smul, Submonoid.smul_def]
    congr
    simp only [Submonoid.coe_mul, Submonoid.coe_finsetProd, mul_comm]
    rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),
      Finset.insert_erase hi]