awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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)
have 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
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]
-- 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'
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
⊢ ∃ (b : ↥S), ∀ i ∈ s, IsInteger f ((↑b : R) • g i)
have 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)
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]
-- 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
inst_6 : Finite ι
g : ι → M'
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)
have intro : ∀ (val : Fintype ι), ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)
Tactic: cases nonempty_fintype ι
-- 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
inst_6 : Finite ι
g : ι → M'
val : Fintype ι
⊢ ∃ (b : ↥S), ∀ (i : ι), IsInteger f ((↑b : R) • g i)
have 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)
Tactic: obtain ⟨b, hb⟩ := exist_integer_multiples S f Finset.univ g
-- 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
inst_6 : DecidableEq M
s : Finset M'
⊢ (⇑f : (a : M) → M') '' (↑(Finset.image (fun (t : ↥s) ↦ integerMultiple S f s id t) s.attach) : Set M) =
    commonDenomOfFinset S f s • (↑s : Set M')
have rw : Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
    ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)) =
  commonDenomOfFinset S f s • (↑s : Set M')
Tactic: rw [Finset.coe_image]
-- 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
inst_6 : DecidableEq M
s : Finset M'
⊢ Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
      ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)) =
    commonDenomOfFinset S f s • (↑s : Set M')
have h : ∀ (x : M'),
  Membership.mem (γ := Set M')
      (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
        ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset S f s • (↑s : Set M')
Tactic: ext
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : M'
⊢ Membership.mem (γ := Set M')
      (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
        ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset S f s • (↑s : Set M')
have h : Membership.mem (γ := Set M')
    (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
      ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
    x →
  x ∈ commonDenomOfFinset S f s • (↑s : Set M')
Tactic: constructor
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : M'
h :
  Membership.mem (γ := Set M')
      (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
        ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
      x →
    x ∈ commonDenomOfFinset S f s • (↑s : Set M')
⊢ Membership.mem (γ := Set M')
      (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
        ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset S f s • (↑s : Set M')
have h₁ : x ∈ commonDenomOfFinset S f s • (↑s : Set M') →
  Membership.mem (γ := Set M')
    (Set.image.{u_2, u_3} (α := M) (⇑f : (a : M) → M')
      ((fun (t : ↥s) ↦ integerMultiple S f s id t) '' (↑s.attach : Set ↥s)))
    x
Tactic: constructor
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : ↥s
⊢ Membership.mem (α := M') (commonDenomOfFinset S f s • (↑s : Set M'))
    ((f : (a : M) → M') ((fun (t : ↥s) ↦ integerMultiple S f s id t) x) : M')
have h : commonDenom S f s id • id (↑x : M') ∈ commonDenomOfFinset S f s • (↑s : Set M')
Tactic: rw [map_integerMultiple]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (hypothesis)
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
inst_6 : DecidableEq M
x : M
s : Finset M'
hx : Membership.mem (α := M') (γ := Submodule R M') (Submodule.span R (↑s : Set M')) ((f : (a : M) → M') x : M')
y : ↥S := commonDenomOfFinset S f s
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have hx₁ : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
Tactic: have hx₁ : y • (s : Set M') = f '' _ :=
    (IsLocalizedModule.finsetIntegerMultiple_image S f s).symm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (hypothesis)
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
inst_6 : DecidableEq M
x : M
s : Finset M'
hx : Membership.mem (α := M') (γ := Submodule R M') (Submodule.span R (↑s : Set M')) ((f : (a : M) → M') x : M')
y : ↥S := commonDenomOfFinset S f s
hx₁ : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have hx₂ : Eq (α := Submodule R M') (Submodule.span R (y • (↑s : Set M')))
  (Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)))
Tactic: apply congrArg (Submodule.span R) at hx₁
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (hypothesis)
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
inst_6 : DecidableEq M
x : M
s : Finset M'
hx : Membership.mem (α := M') (γ := Submodule R M') (Submodule.span R (↑s : Set M')) ((f : (a : M) → M') x : M')
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  Eq (α := Submodule R M') (Submodule.span R (y • (↑s : Set M')))
    (Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)))
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have hx₂ : HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
  Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
Tactic: rw [Submodule.span_smul] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (hypothesis)
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
inst_6 : DecidableEq M
x : M
s : Finset M'
hx : Membership.mem (α := M') (γ := Submodule R M') (Submodule.span R (↑s : Set M')) ((f : (a : M) → M') x : M')
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have hx₂ : HSMul.hSMul (β := M') (↑y : R) ((f : (a : M) → M') x : M') ∈
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M'))
Tactic: replace hx : _ ∈ y • Submodule.span R (s : Set M') := Set.smul_mem_smul_set hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Int (hypothesis)
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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
hx :
  HSMul.hSMul (β := M') (↑y : R) ((f : (a : M) → M') x : M') ∈
    HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M'))
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have hx₂ : Membership.mem (α := M') (Submodule.map f (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)))
  ((f : (a : M) → M') ((↑y : R) • x) : M')
Tactic: rw [hx₁, ← f.map_smul, ← Submodule.map_span f] at hx
Cleared hypotheses: hx
-- 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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
hx :
  Membership.mem (α := M') (Submodule.map f (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)))
    ((f : (a : M) → M') ((↑y : R) • x) : M')
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have obtain : ∀ (x' : M) (hx' : x' ∈ (↑(Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) : Set M))
  (hx'' : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x' : M') ((f : (a : M) → M') ((↑y : R) • x) : M')),
  ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
Tactic: obtain ⟨x', hx', hx''⟩ := hx
Cleared hypotheses: hx
-- 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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
x' : M
hx' : x' ∈ (↑(Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) : Set M)
hx'' : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x' : M') ((f : (a : M) → M') ((↑y : R) • x) : M')
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have obtain : ∀ (a : ↥S) (ha : a • x' = a • (↑y : R) • x),
  ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
Tactic: obtain ⟨a, ha⟩ := (IsLocalizedModule.eq_iff_exists S f).mp hx''
-- 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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
x' : M
hx' : x' ∈ (↑(Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) : Set M)
hx'' : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x' : M') ((f : (a : M) → M') ((↑y : R) • x) : M')
a : ↥S
ha : a • x' = a • (↑y : R) • x
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)
have h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) ((a * y) • x)
Tactic: use a * y
-- 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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
x' : M
hx' : x' ∈ (↑(Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) : Set M)
hx'' : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x' : M') ((f : (a : M) → M') ((↑y : R) • x) : M')
a : ↥S
ha : a • x' = a • (↑y : R) • x
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) ((a * y) • x)
have h : (a * y) • x = (↑a : R) • x'
Tactic: convert!
    (Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s : Set M)).smul_mem a hx'
      using 1
-- 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
inst_6 : DecidableEq M
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁_1 : y • (↑s : Set M') = (⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M)
hx₁ :
  HSMul.hSMul (β := Submodule R M') y (Submodule.span R (↑s : Set M')) =
    Submodule.span R ((⇑f : (a : M) → M') '' (↑(finsetIntegerMultiple S f s) : Set M))
x' : M
hx' : x' ∈ (↑(Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) : Set M)
hx'' : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x' : M') ((f : (a : M) → M') ((↑y : R) • x) : M')
a : ↥S
ha : a • x' = a • (↑y : R) • x
⊢ (a * y) • x = (↑a : R) • x'
have h : (a * y) • x = a • (↑y : R) • x
Tactic: convert! ha.symm using 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)) ↔
    IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
have rw : ((∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ∧
    (∀ (y : Aₛ),
        ∃ (x : Prod.{u_2, u_1} A ↥S),
          x.2 • y = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x.1) ∧
      ∀ {x₁ x₂ : A},
        Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₁ : Aₛ)
            ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₂ : Aₛ) →
          ∃ (c : ↥S), c • x₁ = c • x₂) ↔
  (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)) ∧
    (∀ (z : Aₛ),
        ∃ (x : A × ↥(Algebra.algebraMapSubmonoid A S)),
          HMul.hMul (β := Aₛ) z ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x.2 : A) : Aₛ) =
            (algebraMap A Aₛ : (a : A) → Aₛ) x.1) ∧
      ∀ {x y : A},
        Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) y : Aₛ) →
          ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * y
Tactic: rw [isLocalizedModule_iff, isLocalization_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
⊢ ((∀ (x : ↥S),
        IsUnit.{u_3} (M := Module.End R Aₛ)
          ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ∧
      (∀ (y : Aₛ),
          ∃ (x : Prod.{u_2, u_1} A ↥S),
            x.2 • y = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x.1) ∧
        ∀ {x₁ x₂ : A},
          Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₁ : Aₛ)
              ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₂ : Aₛ) →
            ∃ (c : ↥S), c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)),
        IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)) ∧
      (∀ (z : Aₛ),
          ∃ (x : A × ↥(Algebra.algebraMapSubmonoid A S)),
            HMul.hMul (β := Aₛ) z ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x.2 : A) : Aₛ) =
              (algebraMap A Aₛ : (a : A) → Aₛ) x.1) ∧
        ∀ {x y : A},
          Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) y : Aₛ) →
            ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * y
have refine_1 : (∀ (x : ↥S),
    IsUnit.{u_3} (M := Module.End R Aₛ)
      ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
  ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
Tactic: refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
⊢ ((∀ (x : ↥S),
        IsUnit.{u_3} (M := Module.End R Aₛ)
          ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ∧
      (∀ (y : Aₛ),
          ∃ (x : Prod.{u_2, u_1} A ↥S),
            x.2 • y = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x.1) ∧
        ∀ {x₁ x₂ : A},
          Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₁ : Aₛ)
              ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₂ : Aₛ) →
            ∃ (c : ↥S), c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)),
        IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)) ∧
      (∀ (z : Aₛ),
          ∃ (x : A × ↥(Algebra.algebraMapSubmonoid A S)),
            HMul.hMul (β := Aₛ) z ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x.2 : A) : Aₛ) =
              (algebraMap A Aₛ : (a : A) → Aₛ) x.1) ∧
        ∀ {x y : A},
          Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) y : Aₛ) →
            ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * y
have refine_2 : ∀ (x : Aₛ),
  (∃ (x_1 : Prod.{u_2, u_1} A ↥S),
      x_1.2 • x = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1.1) ↔
    ∃ (x_1 : A × ↥(Algebra.algebraMapSubmonoid A S)),
      HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x_1.2 : A) : Aₛ) =
        (algebraMap A Aₛ : (a : A) → Aₛ) x_1.1
Tactic: refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))