awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)))
⊢ 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)))
    ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)
have a₁ : Membership.mem (γ :=
  Submodule (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
  (Ideal.span (p (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)))
  ((algebraMap R (Rₜ (Subtype.mk (p := fun (x : R) ↦ x ∈ s) a ha)) : (a_1 : R) → Rₜ ⟨a, ha⟩) 1)
Tactic: apply h₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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)))
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have 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)
Tactic: have h₂ : IsLocalization.mk' (Rₜ ⟨a, ha⟩) 1 (1 : Submonoid.powers a) ∈ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) ''
        (Set.range <| IsLocalization.Away.mulNumerator s p)) := by
    rw [IsLocalization.mk'_one]
    apply h₁
    simp [htone]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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)
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have 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)
Tactic: rw [IsLocalization.mem_span_map (Submonoid.powers a)] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have 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) sorry))),
  a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
Tactic: obtain ⟨y, hy, ⟨-, m, rfl⟩, hyz⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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) ⋯))
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have 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) sorry) :
          R) *
        1) =
    (↑c : R) * ((↑1 : R) * y)
Tactic: rw [IsLocalization.eq] at hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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)
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have obtain : ∀ (n : ℕ)
  (hc :
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
              ((fun (x : ℕ) ↦ a ^ x) n) sorry) :
          R) *
        ((↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
                ((fun (x : ℕ) ↦ a ^ x) m) sorry) :
            R) *
          1) =
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers a) x)
              ((fun (x : ℕ) ↦ a ^ x) n) sorry) :
          R) *
        ((↑1 : R) * y)),
  a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
Tactic: obtain ⟨⟨-, n, rfl⟩, hc⟩ := hyz
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (hypothesis)
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 ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have hc₁ : a ^ n * a ^ m = a ^ n * y
Tactic: simp only [OneMemClass.coe_one, one_mul, mul_one] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Lemmas (goal)
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
⊢ a ∈ (↑(Ideal.radical (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p)))) : Set R)
have h : Membership.mem (γ := Ideal R) (Ideal.span (Set.range (mulNumerator s (Rₜ := Rₜ) p))) (a ^ (n + m))
Tactic: use n + m
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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) ((algebraMap R (Module.End R Q) : (a : R) → Module.End R Q) (↑s : R) : Module.End R Q)
have 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)
Tactic: rw [← (Algebra.lsmul R (A := A) R Q).commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ ∃! 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
have 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
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 _
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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 = ℓ
⊢ ∃! 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
have 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 ℓ
Tactic: refine ⟨ℓ.extendScalarsOfIsLocalization S A, by simp, fun g'' h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
have refine : ∀ (h : IsBaseChange A f), IsLocalizedModule S f
Tactic: refine ⟨fun _ ↦ IsLocalizedModule.isBaseChange S A f, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
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
⊢ IsLocalizedModule S f
have this₁ : IsBaseChange (N := LocalizedModule S M) A (LocalizedModule.mkLinearMap S M)
Tactic: have : IsBaseChange A (LocalizedModule.mkLinearMap S M) := IsLocalizedModule.isBaseChange S A _
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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 f
have h₁ : f = (↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M
Tactic: convert! IsLocalizedModule.of_linearEquiv S (LocalizedModule.mkLinearMap S M) e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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)
⊢ f = (↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M
have h₁ : ∀ (x : M),
  Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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)
x : M
⊢ Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
    (((↑e : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M') x : M')
have h₁ : Eq.{u_4 + 1} (α := M') ((f : (a : M) → M') x : M')
  (Function.comp (β := LocalizedModule S M) (⇑(↑e : LocalizedModule S M →ₗ[R] M') : (a : LocalizedModule S M) → M')
      (⇑(LocalizedModule.mkLinearMap S M) : (a : M) → LocalizedModule S M) x :
    M')
Tactic: rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]