awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
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₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
a : R
aS : a ∈ S
x : M₀
hx : (g : (a : M₀) → M₁) x = a • m
h₁ :
  Eq (α := LocalizedModule S M₁)
    (mk ((g : (a : M₀) → M₁) x) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s) : LocalizedModule S M₁)
    (mk m s : LocalizedModule S M₁)
h₂ : Eq (α := LocalizedModule S M₁) (mk (a • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s)) (mk m s)
h₃ :
  Eq (α := LocalizedModule S M₁) (mk (a • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s))
    (mk (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s))
h₄ h₅ :
  Eq (α := LocalizedModule S M₁) (mk (a • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s))
    (mk (a • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s))
⊢ Eq (α := 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 x (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s)) :
      LocalizedModule S M₁)
    (mk m s : LocalizedModule S M₁)

Tactic:
rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]

Premises used: LocalizedModule.mk_cancel_common_left, Submonoid.mk_smul, Subtype.mk, IsLocalizedModule.map_LocalizedModules
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
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₀
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₁)
      x =
    y
revert :
  ∀
    (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₁)
          x =
        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₂)
⊢ 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₂)

Tactic:
revert hx
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
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₀
⊢ ∀
    (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₁)
          x =
        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₂)

Tactic:
induction_on (fun m s hx ↦ ?_) x

Premises used: LocalizedModule.induction_on
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
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₀
refine :
  ∀ (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₂)
⊢ ∀
    (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₁)
          x =
        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₂)

Tactic:
refine induction_on (fun m s hx ↦ ?_) x
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
M₀' : Type u_5
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_3
M₁' : Type u_6
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_4
M₂' : Type u_7
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
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₂)
⊢ Exact.{u_5, u_6, u_7} (M := M₀') (N := M₁') (P := M₂')
    (⇑((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g : M₀' →ₗ[R] M₁') : (a : M₀') → M₁')
    (⇑((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h : M₁' →ₗ[R] M₂') : (a : M₁') → M₂')

Tactic:
Function.Exact.of_ladder_linearEquiv_of_exact
    (map_iso_commute S f₀ f₁ g) (map_iso_commute S f₁ f₂ h) (LocalizedModule.map_exact S g h ex)

Premises used: Function.Exact.of_ladder_linearEquiv_of_exact, LocalizedModule.map_exact, IsLocalizedModule.map_iso_commute
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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'
⊢ IsInteger f 0

Tactic:
Submodule.zero_mem _

Premises used: IsLocalizedModule.IsInteger, Submodule.zero_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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'
x y : M'
hx : IsInteger f x
hy : IsInteger f y
⊢ IsInteger f (x + y)

Tactic:
Submodule.add_mem _ hx hy

Premises used: IsLocalizedModule.IsInteger, Submodule.add_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
rcases : ∀ (x' : M) (hx : (f : (a : M) → M') x' = x), IsInteger f (a • x)
⊢ IsInteger f (a • x)

Tactic:
rcases hx with ⟨x', hx⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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') = a • x
⊢ IsInteger f (a • x)

Tactic:
use a • x'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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')
h₁ h₂ : HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M') = HSMul.hSMul (β := M') a ((f : (a : M) → M') x' : M')
⊢ (f : (a : M) → M') (a • x') = a • x

Tactic:
rw [← hx, LinearMapClass.map_smul]

Premises used: LinearMapClass.map_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
x : M'
⊢ ∃ (a : ↥S), IsInteger f ((↑a : R) • x)

Tactic:
let ⟨⟨Num, denom⟩, h⟩ := IsLocalizedModule.surj S f x
  ⟨denom, Set.mem_range.mpr ⟨Num, h.symm⟩⟩

Premises used: Iff.mpr, Set.mem_range, Exists, IsLocalizedModule.IsInteger, Exists.intro, _private.0.IsLocalizedModule.exists_integer_multiple.match_1, HSMul.hSMul, Eq.symm, Subtype.val, IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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'
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)
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)

Tactic:
choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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)

Tactic:
⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩

Premises used: Finset.prod, Exists.intro, Prod.snd
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
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)
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)

Tactic:
refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
⊢ M

Tactic:
exact (∏ j ∈ s.erase i, (sec j).2) • (sec i).1

Premises used: Prod.fst, Finset.prod, Finset.erase, Prod.snd
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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 :
  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)
⊢ (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:
simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finsetProd]

Premises used: Submonoid.coe_finsetProd, LinearMap.map_smul_of_tower
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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 :
  (↑((∏ 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)
⊢ 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:
rw [← hsec, ← mul_smul, Submonoid.smul_def]

Premises used: Submonoid.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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 : (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) = ∏ i ∈ s, (↑(sec i).2 : R)
⊢ (↑((∏ 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:
congr
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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 : (↑(sec i).2 : R) * ∏ i ∈ s.erase i, (↑(sec i).2 : R) = ∏ i ∈ s, (↑(sec i).2 : R)
⊢ (↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) : R) = ∏ i ∈ s, (↑(sec i).2 : R)

Tactic:
simp only [Submonoid.coe_mul, Submonoid.coe_finsetProd, mul_comm]

Premises used: Submonoid.coe_finsetProd, mul_comm, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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))
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R) (∏ x ∈ s, (↑(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)

Tactic:
rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),
      Finset.insert_erase hi]

Premises used: Finset.prod_insert, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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'
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)
refine_1 :
  (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) → M
refine_2 refine_2₁ :
  ∀ (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)
⊢ ∃ (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]

Premises used: Submonoid.coe_finsetProd, Submonoid.smul_def, mul_comm, LinearMap.map_smul_of_tower, SemigroupAction.mul_smul, Submonoid.coe_mul, IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
inst_6 : Finite ι
g : ι → M'
intro : ∀ (val : Fintype ι), ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
inst_6 : Finite ι
g : ι → M'
val : Fintype ι
intro :
  ∀ (b : ↥S) (hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger f ((↑b : R) • g i)),
    ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples S f Finset.univ g

Premises used: Finset.univ, IsLocalizedModule.exist_integer_multiples
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
inst_6 : Finite ι
g : ι → M'
val : Fintype ι
b : ↥S
hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger f ((↑b : R) • g i)
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)

Tactic:
⟨b, fun i => hb i (Finset.mem_univ _)⟩

Premises used: Finset.mem_univ, Exists.intro
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
inst_6 : Finite ι
g : ι → M'
val : Fintype ι
b : ↥S
hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger f ((↑b : R) • g i)
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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
s : Finset M'
⊢ ∃ (b : ↥S), ∀ a ∈ s, IsInteger f ((↑b : R) • a)

Tactic:
exist_integer_multiples S f s id

Premises used: IsLocalizedModule.exist_integer_multiples, id
-- Module: Mathlib.Algebra.Module.LocalizedModule.Int
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'
i : ↥s
⊢ (f : (a : M) → M') (integerMultiple S f s g i) = commonDenom S f s g • g (↑i : ι)

Tactic:
((exist_integer_multiples S f s g).choose_spec _ i.prop).choose_spec

Premises used: Exists.choose_spec, IsLocalizedModule.exist_integer_multiples, Subtype.prop, IsLocalizedModule.integerMultiple