awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_6 : DecidableEq M
s : Finset M'
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')
⊢ (⇑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')

Tactic:
rw [Finset.coe_image]

Premises used: Finset.coe_image
-- 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
inst_6 : DecidableEq M
s : Finset M'
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')
⊢ 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:
ext
-- 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
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')
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
⊢ 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
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : ↥s
h : commonDenom S f s id • id (↑x : M') ∈ commonDenomOfFinset S f s • (↑s : Set M')
⊢ 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')

Tactic:
rw [map_integerMultiple]

Premises used: IsLocalizedModule.map_integerMultiple
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : ↥s
⊢ commonDenom S f s id • id (↑x : M') ∈ commonDenomOfFinset S f s • (↑s : Set M')

Tactic:
Set.mem_image_of_mem _ x.prop

Premises used: Set.Mem, Set.mem_image_of_mem, Subtype.prop
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : ↥s
⊢ commonDenom S f s id • id (↑x : M') ∈ commonDenomOfFinset S f s • (↑s : Set M')

Tactic:
exact Set.mem_image_of_mem _ x.prop

Premises used: Set.mem_image_of_mem, Subtype.prop
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : M'
hx : x ∈ (↑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)))
    ((fun (x : M') ↦ (↑(commonDenomOfFinset S f s) : R) • x) x)

Tactic:
⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s id _⟩

Premises used: Set.Mem, setOf, Finset.mem_attach, id, Subtype.mk, And.intro, Exists.intro, Set.image, IsLocalizedModule.map_integerMultiple, rfl
-- 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
inst_6 : DecidableEq M
s : Finset M'
x : M'
hx : x ∈ (↑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)))
    ((fun (x : M') ↦ (↑(commonDenomOfFinset S f s) : R) • x) x)

Tactic:
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple S f s 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
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
⊢ 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
-- 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
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)
⊢ 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₁

Premises used: congrArg, Submodule.span
-- 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
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)))
⊢ 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₁

Premises used: Submodule.span_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
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))
⊢ 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
-- 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
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'))
⊢ 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

Premises used: LinearMap.map_smul, Submodule.map_span
-- 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
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')
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)
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)

Tactic:
obtain ⟨x', hx', hx''⟩ := hx
-- 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
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')
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)
⊢ ∃ (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''

Premises used: Iff.mp, IsLocalizedModule.eq_iff_exists
-- 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
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
h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) ((a * y) • x)
⊢ ∃ (m : ↥S), Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) (m • x)

Tactic:
use a * y
-- 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
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 : R) • x')

Tactic:
(Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s : Set M)).smul_mem a hx'

Premises used: IsLocalizedModule.finsetIntegerMultiple, SetLike.coe, Submodule.span, Subtype.val, Submodule.smul_mem
-- 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
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
h : (a * y) • x = (↑a : R) • x'
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑(finsetIntegerMultiple S f s) : Set M)) ((a * y) • x)

Tactic:
convert!
    (Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s : Set M)).smul_mem a hx'
      using 1

Premises used: IsLocalizedModule.finsetIntegerMultiple, SetLike.coe, Submodule.span, Subtype.val, Submodule.smul_mem
-- 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
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 : R) • x = a • x'

Tactic:
ha.symm

Premises used: Eq.symm
-- 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
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
h : (a * y) • x = a • (↑y : R) • x
⊢ (a * y) • x = (↑a : R) • x'

Tactic:
convert! ha.symm using 1

Premises used: Eq.symm
-- 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
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 • (↑y : R) • x

Tactic:
simp only [Submonoid.smul_def, ← smul_smul]

Premises used: smul_smul, Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
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ₛ
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
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)) ↔
    IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

Tactic:
rw [isLocalizedModule_iff, isLocalization_iff]

Premises used: isLocalizedModule_iff, isLocalization_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
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

Tactic:
and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))

Premises used: forall₂_congr, forall_congr', and_congr