awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1

Tactic:
⟨(z' : R) • y + (z : R) • y',
          Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Subtype.val, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp : mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • ((↑z' : R) • y + (↑z : R) • y')
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1

Tactic:
refine
        ⟨(z' : R) • y + (z : R) • y',
          Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', ?_⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S 1 z • y + mk' S 1 z' • y' =
    HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y +
      HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
⊢ mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • ((↑z' : R) • y + (↑z : R) • y')

Tactic:
rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ←
        IsScalarTower.algebraMap_smul S (z' : R), smul_smul, smul_smul]

Premises used: smul_smul, IsScalarTower.algebraMap_smul, Subtype.val, smul_add
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp : mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ : mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y +
      HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
mp₃ : mk' S (HMul.hMul (α := R) 1 1) z • y = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) 1 : S) • y
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z • y = (mk' S 1 z * 1) • y
mp₅ : mk' S 1 z • y = (mk' S 1 z * 1) • y
mp₆ mp₇ : mk' S 1 z • y = mk' S 1 z • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y

Tactic:
rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]

Premises used: mul_assoc, map_one, mul_one, OfNat.ofNat, IsLocalization.mk'_spec, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    (HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) (↑z : R) : S) * mk' S 1 z') • y'
mp₃ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) 1 : S) (mk' S 1 z') • y'
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z' • y' = (1 * mk' S 1 z') • y'
mp₅ : mk' S 1 z' • y' = (1 * mk' S 1 z') • y'
mp₆ mp₇ : mk' S 1 z' • y' = mk' S 1 z' • y'
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'

Tactic:
rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]

Premises used: map_one, mul_right_comm, mul_one, OfNat.ofNat, one_mul, IsLocalization.mk'_spec, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a_1 : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a_1) x
a : S
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a_1) (mk' S 1 z • y)
mp :
  ∀ (y' : R) (z' : ↥M),
    ∃ (y_1 : N),
      Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y_1 ∧
        ∃ (z_1 : ↥M), mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y_1 ∧ ∃ (z_1 : ↥M), a • mk' S 1 z • y = mk' S 1 z_1 • y_1

Tactic:
obtain ⟨y', z', rfl⟩ := exists_mk'_eq M a

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : R
z' : ↥M
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1

Tactic:
⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, HSMul.hSMul, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : R
z' : ↥M
mp : mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1

Tactic:
refine ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₁ :
  (mk' S y' z' * mk' S 1 z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₂ :
  mk' S (y' * 1) (z' * z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₃ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (β := S) (mk' S 1 (z' * z)) ((algebraMap R S : (a : R) → S) y' : S) • y
mp₄ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y' : S) (mk' S 1 (z' * z)) • y
mp₅ mp₆ : mk' S (y' * 1) (z' * z) • y = mk' S (y' * 1) (z' * z) • y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y

Tactic:
rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul]

Premises used: smul_smul, IsScalarTower.algebraMap_smul, IsLocalization.mk', mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
a : Set N
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
⊢ Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)

Tactic:
Submodule.smul_mem _ _ (Submodule.span_subset_span R S _ hy)

Premises used: Submodule.span_subset_span, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
a : Set N
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
⊢ Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)

Tactic:
exact Submodule.smul_mem _ _ (Submodule.span_subset_span R S _ hy)

Premises used: Submodule.span_subset_span, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
⊢ Membership.mem (γ := Ideal S) (Ideal.span ((⇑(algebraMap R S) : (a : R) → S) '' a)) x ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
(mem_span_iff M).trans ?_

Premises used: Set.Mem, Iff.trans, IsLocalization.mem_span_iff
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
refine :
  (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
⊢ Membership.mem (γ := Ideal S) (Ideal.span ((⇑(algebraMap R S) : (a : R) → S) '' a)) x ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
refine (mem_span_iff M).trans ?_

Premises used: Iff.trans, IsLocalization.mem_span_iff
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
mp :
  (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) →
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
mpr :
  (∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z) →
    ∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y
⊢ (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
mp :
  (∃ (y : S), Membership.mem (γ := Submodule R S) (coeSubmodule S (Ideal.span a)) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y) →
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
⊢ (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) →
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
rw [← coeSubmodule_span]

Premises used: IsLocalization.coeSubmodule_span
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
⟨y, hy, z, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : x = mk' S y z
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z

Tactic:
refine ⟨y, hy, z, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₂ : HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₃ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z) = mk' S y z
mp₄ : mk' S (y * 1) z = mk' S y z
mp₅ mp₆ : mk' S y z = mk' S y z
⊢ x = mk' S y z

Tactic:
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

Premises used: Algebra.linearMap_apply, mul_comm, smul_eq_mul, mul_one, IsLocalization.mul_mk'_eq_mk'_of_mul
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
⊢ ∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, ?_⟩

Premises used: Algebra.algebraMap, And.intro, Exists.intro, Submodule.map_mem_span_algebraMap_image, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
⊢ ∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
refine ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₁ : mk' S y z = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₂ : mk' S y z = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z)
mpr₃ : mk' S y z = mk' S (y * 1) z
mpr₄ mpr₅ : mk' S y z = mk' S y z
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

Premises used: mul_comm, smul_eq_mul, mul_one, IsLocalization.mul_mk'_eq_mk'_of_mul
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I J : Ideal R
⊢ LE.le (α := Submodule R K) (coeSubmodule K I) (coeSubmodule K J) ↔ I ≤ J

Tactic:
IsLocalization.coeSubmodule_le_coeSubmodule le_rfl

Premises used: le_rfl, IsLocalization.coeSubmodule_le_coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ StrictMono.{u_3, u_4} (α := Ideal R) (β := Submodule R K) (coeSubmodule K)

Tactic:
strictMono_of_le_iff_le fun _ _ => coeSubmodule_le_coeSubmodule.symm

Premises used: strictMono_of_le_iff_le, IsFractionRing.coeSubmodule_le_coeSubmodule, Iff.symm
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := Ideal R) (β := Submodule R K) (coeSubmodule K)

Tactic:
.of_eq_imp_le fun hl => coeSubmodule_le_coeSubmodule.mp hl.le

Premises used: Eq.le, IsFractionRing.coeSubmodule_le_coeSubmodule, Iff.mp, Function.Injective.of_eq_imp_le
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
K : Type u_4
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : Ideal R
⊢ Submodule.IsPrincipal (coeSubmodule K I) ↔ Submodule.IsPrincipal I

Tactic:
IsLocalization.coeSubmodule_isPrincipal _ le_rfl

Premises used: le_rfl, IsLocalization.coeSubmodule_isPrincipal
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : LT.lt (α := Prop) ((fun (x : m) ↦ x ≠ k) j) ((fun (x : m) ↦ x ≠ k) i)
⊢ i ≠ k ∧ j = k

Tactic:
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp, not_not] at lt

Premises used: lt_iff_not_ge, Classical.not_not, Classical.not_imp, le_Prop_eq
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
rw :
  Eq.{u_2 + 1} (α := S)
    ((of : (a : m → m → S) → Matrix m m S)
        (fun (i j : m) ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0)
        i j :
      S)
    (0 : S)
rw₁ : (if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) = 0
rw₂ : Eq.{u_2 + 1} (α := S) (if i = k then 1 else 0) 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) 0 0
⊢ auxMat M k i j = 0

Tactic:
rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]

Premises used: Matrix.of_apply, if_pos, And.right, And.left, if_neg, Algebra.Norm.Transitivity.auxMat
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
a :
  ∀ (i j : { a : m // (a ≠ k) = True }),
    (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) True i j =
      HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a ≠ k) = True } { a : m // (a ≠ k) = True } S) (M k k) 1 i j
⊢ (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) True =
    HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a ≠ k) = True } { a : m // (a ≠ k) = True } S) (M k k) 1

Tactic:
ext i j