awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
h₂ :
  Membership.mem (γ := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
    (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)
⊢ ∃ (y : R),
    Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y ∧
      ∃ (z : ↥(Submonoid.powers a)),
        Eq.{u_2 + 1} (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
          (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)
          (mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y z)

Tactic:
rw [IsLocalization.mem_span_map (Submonoid.powers a)] at h₂

Premises used: IsLocalization.mem_span_map, Submonoid.powers
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
h₂ :
  ∃ (y : R),
    Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y ∧
      ∃ (z : ↥(Submonoid.powers a)),
        Eq.{u_2 + 1} (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
          (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)
          (mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y z)
obtain :
  ∀ (y : R) (hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y) (m : ℕ)
    (hyz :
      Eq.{u_2 + 1} (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
        (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)
        (mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
            ((fun (x : ℕ) ↦ a ^ x) m) ⋯))),
    a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)

Tactic:
obtain ⟨y, hy, ⟨-, m, rfl⟩, hyz⟩ := h₂

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y
m : ℕ
hyz :
  Eq.{u_2 + 1} (α := Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
    (mk'.{u_1, u_2} (R := R) (M := Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) 1 1)
    (mk' (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) y
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
        ((fun (x : ℕ) ↦ a ^ x) m) ⋯))
⊢ ∃ (c : ↥(Submonoid.powers a)),
    (↑c : R) *
        ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                ((fun (x : ℕ) ↦ a ^ x) m) ⋯) :
            R) *
          1) =
      (↑c : R) * ((↑1 : R) * y)

Tactic:
rw [IsLocalization.eq] at hyz

Premises used: IsLocalization.eq
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y
m : ℕ
hyz :
  ∃ (c : ↥(Submonoid.powers a)),
    (↑c : R) *
        ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                ((fun (x : ℕ) ↦ a ^ x) m) ⋯) :
            R) *
          1) =
      (↑c : R) * ((↑1 : R) * y)
obtain :
  ∀ (n : ℕ)
    (hc :
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                ((fun (x : ℕ) ↦ a ^ x) n) ⋯) :
            R) *
          ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                  ((fun (x : ℕ) ↦ a ^ x) m) ⋯) :
              R) *
            1) =
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                ((fun (x : ℕ) ↦ a ^ x) n) ⋯) :
            R) *
          ((↑1 : R) * y)),
    a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)

Tactic:
obtain ⟨⟨-, n, rfl⟩, hc⟩ := hyz

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y
m n : ℕ
hc :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x) ((fun (x : ℕ) ↦ a ^ x) n)
            ⋯) :
        R) *
      ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
              ((fun (x : ℕ) ↦ a ^ x) m) ⋯) :
          R) *
        1) =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
            ((fun (x : ℕ) ↦ a ^ x) n) ⋯) :
        R) *
      ((↑1 : R) * y)
⊢ a ^ n * a ^ m = a ^ n * y

Tactic:
simp only [OneMemClass.coe_one, one_mul, mul_one] at hc

Premises used: OneMemClass.coe_one, mul_one, one_mul
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
h : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) (a ^ (n + m))
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)

Tactic:
use n + m
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
s : Set R
hsone : Eq (α := Ideal R) (Ideal.span s) ⊤
Rₜ : (↑s : Type u_1) → Type u_2
inst_1 : (t : (↑s : Type u_1)) → CommRing (Rₜ t)
inst_2 : (t : (↑s : Type u_1)) → Algebra.{u_1, u_2} R (Rₜ t)
inst_3 : ∀ (t : (↑s : Type u_1)), Away.{u_1, u_2} (↑t : R) (Rₜ t)
p : (t : (↑s : Type u_1)) → Set (Rₜ t)
htone : ∀ (r : (↑s : Type u_1)), Eq (α := Ideal (Rₜ r)) (Ideal.span (p r)) ⊤
a : R
ha : a ∈ s
this : IsLocalization.{u_1, u_2} (Submonoid.powers a) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))
h₁ :
  LE.le (α := Ideal (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
    (Ideal.span
      ((⇑(algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha))) : (a_1 : R) → Rₜ ⟨a, ha⟩) ''
        Set.range (mulNumerator s (Rₜ := Rₜ) p)))
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) y
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
⊢ Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) (a ^ (n + m))

Tactic:
simpa [pow_add, hc] using Ideal.mul_mem_left _ _ hy

Premises used: pow_add, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.Away.Lemmas
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
⊢ Away e (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e}))

Tactic:
away_of_isIdempotentElem he Ideal.mk_ker Quotient.mk_surjective

Premises used: IsLocalization.away_of_isIdempotentElem, Quotient.mk_surjective, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
g : M →ₗ[R] Q
s : ↥S
rw :
  IsUnit (M := Module.End R Q)
    ((Algebra.lsmul R R Q : (a : A) → Module.End R Q) ((algebraMap R A : (a : R) → A) (↑s : R)) : Module.End R Q)
⊢ IsUnit (M := Module.End R Q) ((algebraMap R (Module.End R Q) : (a : R) → Module.End R Q) (↑s : R) : Module.End R Q)

Tactic:
rw [← (Algebra.lsmul R (A := A) R Q).commutes]

Premises used: Algebra.lsmul, AlgHom.commutes
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
g : M →ₗ[R] Q
s : ↥S
⊢ IsUnit (M := Module.End R Q)
    ((Algebra.lsmul R R Q : (a : A) → Module.End R Q) ((algebraMap R A : (a : R) → A) (↑s : R)) : Module.End R Q)

Tactic:
(IsLocalization.map_units A s).map _

Premises used: IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
g : M →ₗ[R] Q
s : ↥S
⊢ IsUnit (M := Module.End R Q)
    ((Algebra.lsmul R R Q : (a : A) → Module.End R Q) ((algebraMap R A : (a : R) → A) (↑s : R)) : Module.End R Q)

Tactic:
exact (IsLocalization.map_units A s).map _

Premises used: IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
g : M →ₗ[R] Q
obtain :
  ∀ (ℓ : M' →ₗ[R] Q) (h₂ : ∀ (y : M' →ₗ[R] Q), (fun (l : M' →ₗ[R] Q) ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ),
    ∃! g' : M' →ₗ[A] Q,
      (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type (max (max u_3 u_4) u_2)} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        ℓ ∘ₗ f
⊢ ∃! g' : M' →ₗ[A] Q,
    (↑R :
            {S : Type u_2} →
              {M : Type u_4} →
                {M₂ : Type (max (max u_3 u_4) u_2)} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        f =
      g

Tactic:
obtain ⟨ℓ, rfl, h₂⟩ := IsLocalizedModule.is_universal S f g fun s ↦ by
      rw [← (Algebra.lsmul R (A := A) R Q).commutes]; exact (IsLocalization.map_units A s).map _

Premises used: IsLocalizedModule.is_universal, rfl
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun (l : M' →ₗ[R] Q) ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
⊢ (fun (g' : M' →ₗ[A] Q) ↦
      (↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type (max (max u_3 u_4) u_2)} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        ℓ ∘ₗ f)
    (LinearMap.extendScalarsOfIsLocalization S A ℓ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x : AddCommMonoid Q
x_1 : Module R Q
x_2 : Module A Q
h : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun (l : M' →ₗ[R] Q) ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
refine :
  ∀ (g'' : M' →ₗ[A] Q)
    (h_1 :
      (fun (g' : M' →ₗ[A] Q) ↦
          (↑R :
                  {S : Type u_2} →
                    {M : Type u_4} →
                      {M₂ : Type (max (max u_3 u_4) u_2)} →
                        [inst : Semiring R] →
                          [inst_11 : Semiring S] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module R M] →
                                  [inst_15 : Module R M₂] →
                                    [inst_16 : Module S M] →
                                      [inst_17 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                g' ∘ₗ
              f =
            ℓ ∘ₗ f)
        g''),
    g'' = LinearMap.extendScalarsOfIsLocalization S A ℓ
⊢ ∃! g' : M' →ₗ[A] Q,
    (↑R :
            {S : Type u_2} →
              {M : Type u_4} →
                {M₂ : Type (max (max u_3 u_4) u_2)} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        f =
      ℓ ∘ₗ f

Tactic:
refine ⟨ℓ.extendScalarsOfIsLocalization S A, by simp, fun g'' h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
⊢ IsLocalizedModule S f ↔ IsBaseChange A f

Tactic:
⟨fun _ ↦ IsLocalizedModule.isBaseChange S A f, fun h ↦ ?_⟩

Premises used: IsLocalizedModule.isBaseChange, Iff.intro
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
refine : ∀ (h : IsBaseChange A f), IsLocalizedModule S f
⊢ IsLocalizedModule S f ↔ IsBaseChange A f

Tactic:
refine ⟨fun _ ↦ IsLocalizedModule.isBaseChange S A f, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
⊢ IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)

Tactic:
have : IsBaseChange A (LocalizedModule.mkLinearMap S M) := IsLocalizedModule.isBaseChange S A _
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
⊢ IsLocalizedModule S ((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M)

Tactic:
IsLocalizedModule.of_linearEquiv S (LocalizedModule.mkLinearMap S M) e

Premises used: LocalizedModule.mkLinearMap, IsLocalizedModule.of_linearEquiv
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R M'
inst_8 : Module A M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this_1 : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
h₁ : f = (↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M
⊢ IsLocalizedModule S f

Tactic:
convert! IsLocalizedModule.of_linearEquiv S (LocalizedModule.mkLinearMap S M) e

Premises used: LocalizedModule.mkLinearMap, IsLocalizedModule.of_linearEquiv