awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ length B (B ⊗[A] M) =
    (↑(s.length (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
        ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : ∀
  (k :
    Fin
      (s.length (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
        1)),
  length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            k)) =
    (↑(↑k : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: suffices ∀ k, length B ((s k).baseChange B) =
        k * length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            0)) =
    (↑(↑0 : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : length B ↥⊥ =
  (↑(↑0 : ℕ) : ℕ∞) *
    length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: rw [← RelSeries.head, hs_bot, baseChange_bot]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
k :
  Fin
    (s.length (r :=
        {x : Submodule A M × Submodule A M |
          match (motive := Submodule A M × Submodule A M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
      1)
⊢ length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            k)) =
    (↑(↑k : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have pos : length B
    ↥(Submodule.baseChange B
        (s.toFun (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          0)) =
  (↑(↑0 : ℕ) : ℕ∞) *
    length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot, baseChange_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_baseChange B
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
⊢ ¬IsFiniteLength B (B ⊗[A] M)
have contrapose! : ∀ (h : IsFiniteLength B (B ⊗[A] M)), IsFiniteLength A M
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength B (B ⊗[A] M)
⊢ IsFiniteLength A M
have rw : ∀ (h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)), IsNoetherian A M ∧ IsArtinian A M
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)
⊢ IsNoetherian A M ∧ IsArtinian A M
have this : FaithfullyFlat A B
Tactic: have : FaithfullyFlat A B := FaithfullyFlat.of_flat_of_isLocalHom
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have this : ¬IsFiniteLength B (B ⊗[A] M)
Tactic: have : ¬ IsFiniteLength B (B ⊗[A] M) := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      have : FaithfullyFlat A B := FaithfullyFlat.of_flat_of_isLocalHom
      exact h.imp IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
        IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
this : ¬IsFiniteLength B (B ⊗[A] M)
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have h₁ : length A M = ⊤
Tactic: rw [← length_ne_top_iff, not_ne_iff] at h this
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
this : ¬IsFiniteLength B (B ⊗[A] M)
h₁ : length A M = ⊤
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have this₁ : length B (B ⊗[A] M) = ⊤
Tactic: rw [← length_ne_top_iff, not_ne_iff] at h this
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (hypothesis)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have ne : length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0
Tactic: have ne : length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) ≠ 0 := by
      simpa [← pos_iff_ne_zero, length_pos_iff] using (map_maximalIdeal_lt_top (algebraMap A B)).ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
ne : length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have neg : length B (B ⊗[A] M) =
  ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: rw [h, this, ENat.top_mul ne]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
ne : length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0
neg :
  length B (B ⊗[A] M) =
    ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have neg₁ : ⊤ = ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
Tactic: rw [h, this, ENat.top_mul ne]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Length (goal)
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
ne : length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0
neg :
  length B (B ⊗[A] M) =
    ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
neg₁ :
  ⊤ = ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
have neg₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [h, this, ENat.top_mul ne]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : IsLocalRing R
inst_4 : Nontrivial S
f : R →+* S
⊢ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) =
    (↑(map f { toSubring := ⊤, isLocalRing := ⋯ : LocalSubring R }).toSubring : Set S)
have h : ∀ (x : S),
  x ∈ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) ↔
    x ∈ (↑(map f { toSubring := ⊤, isLocalRing := sorry : LocalSubring R }).toSubring : Set S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
⊢ Localization.AtPrime P ≃ₐ[↥A] ↥(ofPrime A P).toSubring
have refine : Function.Injective.{u_3 + 1, u_3 + 1} (α := Localization.AtPrime P) (β := K)
  (⇑(IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
          Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) sorry :
        Localization.AtPrime P →ₐ[↥A] K) :
    (a : Localization.AtPrime P) → K)
Tactic: refine AlgEquiv.ofInjective (IsLocalization.liftAlgHom (M := P.primeCompl)
    (S := Localization.AtPrime P) (f := Algebra.ofId A K) _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x y : Localization.AtPrime P
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        x :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        y :
      K)
⊢ x = y
have obtain : ∀ (x : ↥A) (s : ↥P.primeCompl)
  (e :
    Eq (α := K)
      (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) sorry :
              Localization.AtPrime P →ₐ[↥A] K) :
            (a : Localization.AtPrime P) → K)
          (IsLocalization.mk' (Localization.AtPrime P) x s) :
        K)
      (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) sorry :
              Localization.AtPrime P →ₐ[↥A] K) :
            (a : Localization.AtPrime P) → K)
          y :
        K)),
  IsLocalization.mk' (Localization.AtPrime P) x s = y
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x
Cleared hypotheses: x, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
y : Localization.AtPrime P
x : ↥A
s : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        y :
      K)
⊢ IsLocalization.mk' (Localization.AtPrime P) x s = y
have obtain : ∀ (y : ↥A) (t : ↥P.primeCompl)
  (e :
    Eq (α := K)
      (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) sorry :
              Localization.AtPrime P →ₐ[↥A] K) :
            (a : Localization.AtPrime P) → K)
          (IsLocalization.mk' (Localization.AtPrime P) x s) :
        K)
      (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
                Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) sorry :
              Localization.AtPrime P →ₐ[↥A] K) :
            (a : Localization.AtPrime P) → K)
          (IsLocalization.mk' (Localization.AtPrime P) y t) :
        K)),
  Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
    (IsLocalization.mk' (Localization.AtPrime P) y t)
Tactic: obtain ⟨y, t, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl y
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
⊢ Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
    (IsLocalization.mk' (Localization.AtPrime P) y t)
have H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
Tactic: have H : ∀ x : P.primeCompl, x.1 ≠ 0 := by rintro ⟨x, hx⟩ rfl; aesop
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
⊢ Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
    (IsLocalization.mk' (Localization.AtPrime P) y t)
have this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
Tactic: have : x.1 = y.1 * t.1.1⁻¹ * s.1.1 := by
    simpa [IsLocalization.lift_mk', Algebra.ofId_apply, H,
      Algebra.algebraMap_ofSubsemiring_apply, IsUnit.coe_liftRight] using congr($e * s.1.1)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
⊢ Eq (α := Localization.AtPrime P) (IsLocalization.mk' (Localization.AtPrime P) x s)
    (IsLocalization.mk' (Localization.AtPrime P) y t)
have rw : Eq (α := Localization.AtPrime P)
  ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑t : ↥A) * x) :
    Localization.AtPrime P)
  ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑s : ↥A) * y) :
    Localization.AtPrime P)
Tactic: rw [IsLocalization.mk'_eq_iff_eq]