awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular.{u_3} (R := A)
    ((fun (x : R × ↥S) ↦
        (match (motive := R × ↥S → A) x with
          | (r, m) => IsLocalization.mk' A r m :
          A))
      (a, s))
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
have neg : ∀ (hc : IsRegular a) (m₁ : M) (t₁ : ↥S) (m₂ : M) (t₂ : ↥S)
  (hxy :
    Eq.{u_4 + 1} (α := N)
      ((fun (x : N) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := A)
            ((fun (x : R × ↥S) ↦
                (match (motive := R × ↥S → A) x with
                  | (r, m) => IsLocalization.mk' A r m :
                  A))
              (a, s))
            x)
        (Function.uncurry (mk' f) (m₁, t₁)))
      ((fun (x : N) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := A)
            ((fun (x : R × ↥S) ↦
                (match (motive := R × ↥S → A) x with
                  | (r, m) => IsLocalization.mk' A r m :
                  A))
              (a, s))
            x)
        (Function.uncurry (mk' f) (m₂, t₂))))
  (hS : ∀ s ∈ S, IsRegular s), Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
Tactic: rw [IsLocalization.isRegular_mk' hS] at hc
Cleared hypotheses: hc, m₁, t₁, m₂, t₂, hxy, hS
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
have this : ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y
Tactic: have (s : S) (x y : M) : s • x = s • y ↔ x = y := (hS _ s.2).isSMulRegular.eq_iff
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
this : ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
have neg : ∀ (hxy : t₁ • a • m₂ = t₂ • a • m₁), t₁ • m₂ = t₂ • m₁
Tactic: simp only [Function.uncurry_apply_pair, mk'_smul_mk', mk'_eq_mk'_iff, mul_smul, this,
      exists_const] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (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₁
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 :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk m s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
⊢ 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₁))
    (mk m s)
have hy₁ : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
Tactic: rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
⊢ 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₁))
    (mk m s)
have obtain : ∀ (a : R) (aS : a ∈ S)
  (ha :
    HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) ((h : (a : M₁) → M₂) m : M₂) =
      HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) 0),
  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₁))
    (mk m s)
Tactic: obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (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₁
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
ha :
  HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) ((h : (a : M₁) → M₂) m : M₂) =
    HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) 0
⊢ 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₁))
    (mk m s)
have ha₁ : Membership.mem (γ := Set M₁) (Set.range.{u_3, u_2 + 1} (ι := M₀) (⇑g : (a : M₀) → M₁)) (a • m)
Tactic: rw [smul_zero, mk_smul, ← map_smul, ex (a • m)] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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
ha : Membership.mem (γ := Set M₁) (Set.range.{u_3, u_2 + 1} (ι := M₀) (⇑g : (a : M₀) → M₁)) (a • m)
⊢ 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₁))
    (mk m s)
have rcases : ∀ (x : M₀) (hx : (g : (a : M₀) → M₁) x = a • m),
  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₁))
    (mk m s)
Tactic: rcases ha with ⟨x, hx⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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
⊢ 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₁))
    (mk m s)
have h₁ : 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: use mk x (⟨a, aS⟩ * s)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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
⊢ 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₁)
have 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₁)
Tactic: rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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₁)
⊢ 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₁)
have h₂ : Eq (α := LocalizedModule S M₁) (mk (a • m) (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s)) (mk m s)
Tactic: rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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)
⊢ 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₁)
have 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))
Tactic: rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
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))
⊢ 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₁)
have 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))
Tactic: rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
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₂)
have 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₂)
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Exact (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
⊢ ∀
    (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₂)
have 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₂)
Tactic: refine induction_on (fun m s hx ↦ ?_) x