awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
hu : Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u hu).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u hu).1
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x
have obtain : ∀ (v : R) (hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u)
  (hx :
    HMul.hMul (β := Sₘ) x
        ((algebraMap S Sₘ : (a : S) → Sₘ)
            (↑(s,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u sorry).2 :
              S) :
          Sₘ) =
      (algebraMap S Sₘ : (a : S) → Sₘ)
        (s,
            Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u
              sorry).1),
  RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) sorry) x
Tactic: obtain ⟨v, hv⟩ := hu
Cleared hypotheses: hu, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x
have obtain : ∀ (v' : Rₘ)
  (hv' :
    HMul.hMul (β := Rₘ) v' ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v sorry) : R) : Rₘ) =
      1),
  RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) sorry) x
Tactic: obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
v' : Rₘ
hv' :
  HMul.hMul (β := Rₘ) v' ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v ⋯) : R) : Rₘ) = 1
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x
have refine_1 : HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) = 1
Tactic: refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
v' : Rₘ
hv' :
  HMul.hMul (β := Rₘ) v' ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v ⋯) : R) : Rₘ) = 1
refine_1 :
  HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) =
    1
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x
have refine_2 : IsIntegral Rₘ (HMul.hMul (β := Sₘ) x ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ))
Tactic: refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
v' : Rₘ
hv' :
  HMul.hMul (β := Rₘ) v' ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v ⋯) : R) : Rₘ) = 1
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) =
    1
have hv'₁ : Eq.{u_4 + 1} (α := Sₘ)
  ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ)
      (HMul.hMul (β := Rₘ) v'
        ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v sorry) : R) : Rₘ)) :
    Sₘ)
  ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) 1 : Sₘ)
Tactic: replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
v' : Rₘ
hv' :
  Eq.{u_4 + 1} (α := Sₘ)
    ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ)
        (HMul.hMul (β := Rₘ) v'
          ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v ⋯) : R) : Rₘ)) :
      Sₘ)
    ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) 1 : Sₘ)
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) =
    1
have hv'₁ : HMul.hMul (α := Sₘ) (β := Sₘ)
    ((IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) sorry : (a : Rₘ) → Sₘ) v' : Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ)
        ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v sorry) : R) : S) :
      Sₘ) =
  1
Tactic: rw [map_mul, map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ (↑M : Set R) ∧ (algebraMap R S : (a : R) → S) v = u
hx :
  HMul.hMul (β := Sₘ) x
      ((algebraMap S Sₘ : (a : S) → Sₘ)
          (↑(s,
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                    u ⋯).2 :
            S) :
        Sₘ) =
    (algebraMap S Sₘ : (a : S) → Sₘ)
      (s, Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x) u ⋯).1
v' : Rₘ
hv' :
  HMul.hMul (β := Rₘ) v' ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) v ⋯) : R) : Rₘ) = 1
⊢ IsIntegral Rₘ (HMul.hMul (β := Sₘ) x ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ))
have refine_2 : ∀ (p : R[X]) (hp : p.Monic ∧ eval₂ (algebraMap R S) s p = 0),
  IsIntegral Rₘ (HMul.hMul (β := Sₘ) x ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ))
Tactic: obtain ⟨p, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
⊢ Membership.mem (γ := Subsemiring Rₘ[X]) (lifts (algebraMap R Rₘ))
    (p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R)))
have rw : ∀ (n : ℕ),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    ((p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).coeff n)
Tactic: rw [Polynomial.lifts_iff_coeff_lifts]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    ((p.scaleRoots ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R))).coeff n)
have rw : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (p.coeff n *
    HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
      (p.natDegree - n))
Tactic: rw [Polynomial.coeff_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos : ∀ (h₁ : n ∈ p.support),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: by_cases h₁ : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
pos :
  ∀ (h₁ : n ∈ p.support),
    Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
      (p.coeff n *
        HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
          (p.natDegree - n))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have neg : ∀ (h₁ : n ∉ p.support),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: by_cases h₁ : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos : ∀ (h₂ : n = p.natDegree),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: by_cases h₂ : n = p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
pos :
  ∀ (h₂ : n = p.natDegree),
    Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
      (p.coeff n *
        HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
          (p.natDegree - n))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have neg : ∀ (h₂ : ¬n = p.natDegree),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: by_cases h₂ : n = p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos : ∀ (h₂ : n = p.natDegree),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: on_goal 1 => by_cases h₂ : n = p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
pos :
  ∀ (h₂ : n = p.natDegree),
    Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
      (p.coeff n *
        HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
          (p.natDegree - n))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have neg : ∀ (h₂ : ¬n = p.natDegree),
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
Tactic: on_goal 1 => by_cases h₂ : n = p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (p.coeff p.natDegree *
    HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
      (p.natDegree - p.natDegree))
Tactic: rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
pos :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff p.natDegree *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos₁ : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (p.leadingCoeff *
    HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
      (p.natDegree - p.natDegree))
Tactic: rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
p : Rₘ[X]
hp : Membership.mem (γ := Subring Rₘ) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R Rₘ)) p.leadingCoeff
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
pos :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff p.natDegree *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
pos₁ :
  Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.leadingCoeff *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - p.natDegree))
⊢ Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
    (p.coeff n *
      HPow.hPow (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ)
        (p.natDegree - n))
have pos₂ : Membership.mem (γ := Set Rₘ) (Set.range.{u_3, u_1 + 1} (ι := R) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ))
  (p.leadingCoeff *
    HPow.hPow (α := Rₘ) (β := ℕ) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(commonDenom M p.support p.coeff) : R) : Rₘ) 0)
Tactic: rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]