awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
simp_rw₄ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
simp_rw₅ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂))))
simp_rw₆ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (s • t₂ • m₁ + s • t₁ • m₂) (s * (t₁ * (s * t₂))))
simp_rw₇ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂))))
simp_rw₈ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * (s * t₂)))
    (mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂))))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left s]

Premises used: LocalizedModule.mk_add_mk, LocalizedModule.liftOn_mk, mul_assoc, LocalizedModule.mk_cancel_common_left, mul_left_comm, mul_comm, SMulCommClass.smul_comm, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
s : ↥S
r : R
x : LocalizedModule S M
⊢ (r • x).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
x.induction_on (fun _ _ ↦ ?_)

Premises used: LocalizedModule.induction_on
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
s : ↥S
r : R
x : LocalizedModule S M
refine :
  ∀ (x : M) (x_1 : ↥S),
    (HSMul.hSMul (β := LocalizedModule S M) r (mk x x_1)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
      HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
        (liftOn (mk x x_1) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
⊢ (r • x).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
refine x.induction_on (fun _ _ ↦ ?_)
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
s : ↥S
r : R
x : LocalizedModule S M
x_1 : M
x_2 : ↥S
simp_rw :
  Eq (α := LocalizedModule S M) (mk (r • x_1) (x_2 * s))
    (mk (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x_1) (x_2 * s))
⊢ (HSMul.hSMul (β := LocalizedModule S M) r (mk x_1 x_2)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (liftOn (mk x_1 x_2) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
simp_rw [smul'_mk, liftOn_mk, smul'_mk]

Premises used: LocalizedModule.liftOn_mk, LocalizedModule.smul'_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
s : ↥S
r : R
x : LocalizedModule S M
x_1 : M
x_2 : ↥S
⊢ Eq (α := LocalizedModule S M) (mk (r • x_1) (x_2 * s))
    (mk (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x_1) (x_2 * s))

Tactic:
congr!
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    mk m t
rw₂ :
  Eq (α := LocalizedModule S M) (liftOn (mk ((↑s : R) • m) t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
    (mk m t)
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • m, t).1 (((↑s : R) • m, t).2 * s)) (mk m t)
rw₄ : Eq (α := LocalizedModule S M) (mk (s • m, t).1 ((s • m, t).2 * s)) (mk m t)
rw₅ rw₆ : Eq (α := LocalizedModule S M) (mk m (s • m, t).2) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)

Tactic:
rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]

Premises used: LocalizedModule.liftOn_mk, LocalizedModule.divBy_apply, LocalizedModule.mk_cancel_common_right, LocalizedModule.smul'_mk, Submonoid.smul_def, Module.algebraMap_end_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) =
    mk m t
rw₂ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk (m, t).1 ((m, t).2 * s)) = mk m t
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • (m, t).1) ((m, t).2 * s)) (mk m t)
rw₄ : Eq (α := LocalizedModule S M) (mk (s • (m, t).1) ((m, t).2 * s)) (mk m t)
rw₅ rw₆ : Eq (α := LocalizedModule S M) (mk (m, t).1 (m, t).2) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)

Tactic:
rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]

Premises used: LocalizedModule.liftOn_mk, LocalizedModule.divBy_apply, LocalizedModule.mk_cancel_common_right, LocalizedModule.smul'_mk, Submonoid.smul_def, Module.algebraMap_end_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h : c • x₁ = c • x₂
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (c • x₁) : M') ((f : (a : M) → M') (c • x₂) : M')

Tactic:
apply_fun f at h
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (c • x₁) : M') ((f : (a : M) → M') (c • x₂) : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₁ : M') :
      M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₂ : M') :
      M')

Tactic:
simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h

Premises used: Submonoid.smul_def, Module.algebraMap_end_apply, LinearMap.map_smul_of_tower
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h :
  Eq.{u_3 + 1} (α := M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₁ : M') :
      M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₂ : M') :
      M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')

Tactic:
((Module.End.isUnit_iff _).mp <| map_units f c).1 h

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h :
  Eq.{u_3 + 1} (α := M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₁ : M') :
      M')
    ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M')
        ((f : (a : M) → M') x₂ : M') :
      M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')

Tactic:
exact ((Module.End.isUnit_iff _).mp <| map_units f c).1 h

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
simp_rw :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔
    ∀ (c : ↥S), Function.Injective (β := M) fun (x : M) ↦ c • x
simp_rw₁ :
  (∀ ⦃a₁ a₂ : M⦄, Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') a₁ : M') ((f : (a : M) → M') a₂ : M') → a₁ = a₂) ↔
    ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
simp_rw₂ : (∀ ⦃a₁ a₂ : M⦄, (∃ (c : ↥S), c • a₁ = c • a₂) → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
simp_rw₃ : (∀ ⦃a₁ a₂ : M⦄ (x : ↥S), x • a₁ = x • a₂ → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔ ∀ (c : ↥S), IsSMulRegular M c

Tactic:
simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]

Premises used: forall_comm, IsSMulRegular, Function.Injective, IsLocalizedModule.eq_iff_exists, exists_imp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
h :
  ∀ (x : M''),
    Eq (α := M'') ((((algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) : End R M'') : (a : M'') → M'') x : M'')
      (((↑e : M' →ₗ[R] M'') ∘ₗ (algebraMap R (End R M') : (a : R) → End R M') (↑s : R) ∘ₗ (↑e.symm : M'' →ₗ[R] M') :
            (a : M'') → M'')
          x :
        M'')
⊢ (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) =
    (↑e : M' →ₗ[R] M'') ∘ₗ (algebraMap R (End R M') : (a : R) → End R M') (↑s : R) ∘ₗ (↑e.symm : M'' →ₗ[R] M')

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
x : M''
⊢ Eq (α := M'') ((((algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) : End R M'') : (a : M'') → M'') x : M'')
    (((↑e : M' →ₗ[R] M'') ∘ₗ (algebraMap R (End R M') : (a : R) → End R M') (↑s : R) ∘ₗ (↑e.symm : M'' →ₗ[R] M') :
          (a : M'') → M'')
        x :
      M'')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
rw :
  Function.Bijective.{u_3 + 1, u_3 + 1} (α := M') (β := M')
    (⇑((algebraMap R (End R M') : (a : R) → End R M') (↑s : R) : End R M') : (a : M') → M')
⊢ IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) : End R M'')

Tactic:
rw [show algebraMap R (Module.End R M'') s = e ∘ₗ (algebraMap R (Module.End R M') s) ∘ₗ e.symm
      by ext; simp, Module.End.isUnit_iff, LinearMap.coe_comp, LinearMap.coe_comp,
      LinearEquiv.coe_coe, LinearEquiv.coe_coe, EquivLike.comp_bijective, EquivLike.bijective_comp]

Premises used: Module.End.isUnit_iff, EquivLike.comp_bijective, LinearMap.coe_comp, EquivLike.bijective_comp, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ Function.Bijective.{u_3 + 1, u_3 + 1} (α := M') (β := M')
    (⇑((algebraMap R (End R M') : (a : R) → End R M') (↑s : R) : End R M') : (a : M') → M')

Tactic:
(Module.End.isUnit_iff _).mp <| hf.map_units s

Premises used: Module.End.isUnit_iff, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ Function.Bijective.{u_3 + 1, u_3 + 1} (α := M') (β := M')
    (⇑((algebraMap R (End R M') : (a : R) → End R M') (↑s : R) : End R M') : (a : M') → M')

Tactic:
exact (Module.End.isUnit_iff _).mp <| hf.map_units s

Premises used: Module.End.isUnit_iff, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
obtain :
  ∀ (p : Prod.{u_2, u_1} M ↥S)
    (h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1),
    ∃ (x_1 : Prod.{u_2, u_1} M ↥S), x_1.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x_1.1
⊢ ∃ (x_1 : Prod.{u_2, u_1} M ↥S), x_1.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x_1.1

Tactic:
obtain ⟨p, h⟩ := hf.surj (e.symm x)

Premises used: LinearEquiv.symm, DFunLike.coe, IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
rw :
  p.2 • x =
    Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑(↑e : M' →ₗ[R] M'') : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₁ : p.2 • x = Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := M') (⇑e : (a : M') → M'') (⇑f : (a : M) → M') p.1
rw₂ : p.2 • x = (e : (a : M') → M'') ((f : (a : M) → M') p.1 : M')
rw₃ : p.2 • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₄ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M'))
rw₅ : (↑p.2 : R) • x = (e : (a : M') → M'') (HSMul.hSMul (β := M') (↑p.2 : R) ((e.symm : (a : M'') → M') x : M'))
rw₆ : (↑p.2 : R) • x = HSMul.hSMul (β := M'') (↑p.2 : R) ((e : (a : M') → M'') ((e.symm : (a : M'') → M') x : M') : M'')
rw₇ rw₈ : (↑p.2 : R) • x = (↑p.2 : R) • x
⊢ p.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') p.1

Tactic:
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]

Premises used: Submonoid.smul_def, LinearMap.coe_comp, LinearEquiv.apply_symm_apply, LinearEquiv.congr_arg, Function.comp_apply, LinearEquiv.coe_coe, map_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : Prod.{u_2, u_1} M ↥S
h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1
⊢ ∃ (x_1 : Prod.{u_2, u_1} M ↥S), x_1.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x_1.1

Tactic:
exact ⟨p, by rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁ x₂ : M
h :
  Eq.{u_4 + 1} (α := M'') (((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x₁ : M'')
    (((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x₂ : M'')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      EmbeddingLike.apply_eq_iff_eq] at h

Premises used: EmbeddingLike.apply_eq_iff_eq, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁ x₂ : M
h : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
⊢ ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
hf.exists_of_eq h

Premises used: IsLocalizedModule.exists_of_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁ x₂ : M
h : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
⊢ ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
exact hf.exists_of_eq h

Premises used: IsLocalizedModule.exists_of_eq