awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ Ne.{u_7 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) p.leadingCoeff : Rₘ) (0 : Rₘ)

Tactic:
refine fun hfp => zero_ne_one
      (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ eval₂ (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x)
      (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])) =
    0

Tactic:
eval₂_mul_eq_zero_of_left _ _ _ ?_

Premises used: Polynomial.eval₂_mul_eq_zero_of_left
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
neg : eval₂ (IsLocalization.map Sₘ f ⋯) ((algebraMap S Sₘ : (a : S) → Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0
⊢ eval₂ (IsLocalization.map Sₘ f ⋯ : Rₘ →+* Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x)
      (HMul.hMul (α := Rₘ[X]) (β := Rₘ[X]) (Polynomial.map (algebraMap R Rₘ) p) ((C : (a : Rₘ) → Rₘ[X]) b : Rₘ[X])) =
    0

Tactic:
refine eval₂_mul_eq_zero_of_left _ _ _ ?_

Premises used: Polynomial.eval₂_mul_eq_zero_of_left
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
neg : Eq.{u_8 + 1} (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (eval₂ f x p) : Sₘ) (0 : Sₘ)
⊢ eval₂ (IsLocalization.map Sₘ f ⋯) ((algebraMap S Sₘ : (a : S) → Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0

Tactic:
rw [eval₂_map, IsLocalization.map_comp, ← hom_eval₂ _ f (algebraMap S Sₘ) x]

Premises used: Algebra.algebraMap, Polynomial.hom_eval₂, IsLocalization.map_comp, Polynomial.eval₂_map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ Eq.{u_8 + 1} (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (eval₂ f x p) : Sₘ) (0 : Sₘ)

Tactic:
_root_.trans (congr_arg (algebraMap S Sₘ) hf) (map_zero _)

Premises used: trans, Algebra.algebraMap, map_zero, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
inst_4 : Algebra R Rₘ
inst_5 : IsLocalization M Rₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬Eq.{u_7 + 1} (α := Rₘ) 1 0
this : Nontrivial Rₘ
b : Rₘ
hb :
  HMul.hMul (α := Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) p.leadingCoeff hM) : R) : Rₘ) b =
    1
⊢ Eq.{u_8 + 1} (α := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) (eval₂ f x p) : Sₘ) (0 : Sₘ)

Tactic:
exact _root_.trans (congr_arg (algebraMap S Sₘ) hf) (map_zero _)

Premises used: trans, Algebra.algebraMap, map_zero, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ
x : S
p : R[X]
hp : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
hM : p.leadingCoeff ∈ M
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ) (A := Sₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯ : Rₘ →+* Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)

Tactic:
haveI : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ :=
    inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ)
  (algebraMap R S).isIntegralElem_localization_at_leadingCoeff x p hp M hM

Premises used: Algebra.algebraMap, RingHom.isIntegralElem_localization_at_leadingCoeff, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ
obtain :
  ∀ (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
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x

Tactic:
obtain ⟨⟨s, ⟨u, hu⟩⟩, hx⟩ := surj (Algebra.algebraMapSubmonoid S M) x

Premises used: IsLocalization.surj, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.Localization.Integral
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
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 ⋯).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
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x

Tactic:
obtain ⟨v, hv⟩ := hu
-- Module: Mathlib.RingTheory.Localization.Integral
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
obtain :
  ∀ (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
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x

Tactic:
obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩)

Premises used: Subtype.mk, And.left, Iff.mp, IsLocalization.map_units, isUnit_iff_exists_inv'
-- Module: Mathlib.RingTheory.Localization.Integral
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

Tactic:
@IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_

Premises used: IsIntegral.of_mul_unit, IsIntegral
-- Module: Mathlib.RingTheory.Localization.Integral
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
refine_2 : IsIntegral Rₘ (HMul.hMul (β := Sₘ) x ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ))
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯) x

Tactic:
refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_

Premises used: IsIntegral.of_mul_unit
-- Module: Mathlib.RingTheory.Localization.Integral
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
⊢ 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ₘ)

Tactic:
replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
-- Module: Mathlib.RingTheory.Localization.Integral
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ₘ)
      ((IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯ : (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 ⋯) : R) : S) :
        Sₘ) =
    1

Tactic:
rw [map_mul, map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'

Premises used: IsLocalization.map_eq, map_mul, map_one, localizationAlgebraMap_def
-- Module: Mathlib.RingTheory.Localization.Integral
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 (α := Sₘ) (β := Sₘ)
      ((IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯ : (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 ⋯) : R) : S) :
        Sₘ) =
    1
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) =
    1

Tactic:
hv.2 ▸ hv'

Premises used: Eq.rec, And.right
-- Module: Mathlib.RingTheory.Localization.Integral
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 (α := Sₘ) (β := Sₘ)
      ((IsLocalization.map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯ : (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 ⋯) : R) : S) :
        Sₘ) =
    1
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) v' : Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ) =
    1

Tactic:
exact hv.2 ▸ hv'
-- Module: Mathlib.RingTheory.Localization.Integral
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_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ₘ))
⊢ IsIntegral Rₘ (HMul.hMul (β := Sₘ) x ((algebraMap S Sₘ : (a : S) → Sₘ) u : Sₘ))

Tactic:
obtain ⟨p, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) s

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.Localization.Integral
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
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:
hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)

Premises used: Eq.rec, Submonoid.one_mem, And.right, And.left, Eq.symm, is_integral_localization_at_leadingCoeff
-- Module: Mathlib.RingTheory.Localization.Integral
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
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:
exact hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)