awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)
⊢ Eq (α := Ideal S) (S ∙ e) (Ideal.span {1 - (1 - e)})

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)
⊢ IsLocalization.Away (1 - e) T

Tactic:
have := IsLocalization.away_of_isIdempotentElem he.one_sub (hfe.trans (by simp)) hf
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this_2 : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)
this : IsLocalization.Away (1 - e) T
⊢ IsStandardEtale R T

Tactic:
.of_isLocalizationAway (1 - e)

Premises used: HSub.hSub, OfNat.ofNat, Algebra.IsStandardEtale.of_isLocalizationAway
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this_2 : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)
this : IsLocalization.Away (1 - e) T
⊢ IsStandardEtale R T

Tactic:
exact .of_isLocalizationAway (1 - e)
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P : StandardEtalePresentation R S
inst_5 : IsStandardEtale R S
⊢ IsStandardEtale T (T ⊗[R] S)

Tactic:
⟨⟨Algebra.IsStandardEtale.nonempty_standardEtalePresentation.some.baseChange⟩⟩

Premises used: Nonempty.some, Nonempty.intro, StandardEtalePresentation.baseChange, Algebra.IsStandardEtale.mk, Algebra.IsStandardEtale.nonempty_standardEtalePresentation
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
obtain :
  ∀ (r : R) (hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r),
    p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0 ∧ r ≠ 0

Tactic:
mul_ne_zero_iff.mp (hr ▸ hp)

Premises used: Eq.rec, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)

Premises used: GCDMonoid.gcd, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ r ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)

Premises used: GCDMonoid.gcd, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
nth_rw :
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
    0
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
nth_rw 1 [hr]
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 rw : r ≠ 0
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
    0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Premises used: mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
r0
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
exact r0
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
obtain :
  ∀ (r : R) (hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r),
    q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0 ∧ r ≠ 0

Tactic:
mul_ne_zero_iff.mp (hr ▸ hq)

Premises used: Eq.rec, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)

Premises used: GCDMonoid.gcd, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ r ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)

Premises used: GCDMonoid.gcd, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
nth_rw :
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
    0
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0

Tactic:
nth_rw 1 [hr]
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 rw : r ≠ 0
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
    0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Premises used: mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
r0
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
exact r0
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ IsCoprime (p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q)
    (q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q)

Tactic:
(gcd_isUnit_iff _ _).1 <|
    isUnit_gcd_of_eq_mul_gcd
        (EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_left _ _).symm
        (EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_right _ _).symm <|
      gcd_ne_zero_of_right hq

Premises used: gcd_isUnit_iff, isUnit_gcd_of_eq_mul_gcd, Iff.mp, GCDMonoid.gcd_dvd_left, gcd_ne_zero_of_right, GCDMonoid.gcd_dvd_right, Eq.symm, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hpq : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ IsCoprime (p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q)
    (q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q)

Tactic:
(gcd_isUnit_iff _ _).1 <|
    isUnit_gcd_of_eq_mul_gcd
        (EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_left _ _).symm
        (EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_right _ _).symm <| hpq

Premises used: gcd_isUnit_iff, isUnit_gcd_of_eq_mul_gcd, Iff.mp, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right, Eq.symm, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : Associated (a * b) (a * b)
⊢ Associated (gcd a b * lcm a b) (a * b)

Tactic:
rw [EuclideanDomain.gcd_mul_lcm]

Premises used: EuclideanDomain.gcd_mul_lcm
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)

Tactic:
rfl
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
α : Type u_1
inst : EuclideanDomain α
inst_1 : DecidableEq α
x y : α
⊢ Eq (α := Ideal α) (span {gcd x y}) (span {x, y})

Tactic:
letI := EuclideanDomain.gcdMonoid α
  _root_.span_gcd x y

Premises used: span_gcd
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
α : Type u_1
inst : EuclideanDomain α
inst_1 : DecidableEq α
x y : α
⊢ IsUnit (gcd x y) ↔ IsCoprime x y

Tactic:
letI := EuclideanDomain.gcdMonoid α
  _root_.gcd_isUnit_iff x y

Premises used: gcd_isUnit_iff
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
α : Type u_1
inst : EuclideanDomain α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y

Tactic:
letI := Classical.decEq α
  letI := EuclideanDomain.gcdMonoid α
  _root_.isCoprime_of_dvd x y nonzero H

Premises used: isCoprime_of_dvd
-- Module: Mathlib.RingTheory.EuclideanDomain
Goal:
α : Type u_1
inst : EuclideanDomain α
x y : α
h : Irreducible x
⊢ x ∣ y ∨ IsCoprime x y

Tactic:
letI := Classical.decEq α
  letI := EuclideanDomain.gcdMonoid α
  _root_.dvd_or_isCoprime x y h

Premises used: dvd_or_isCoprime
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
⊢ IsScalarTower.{u_1, u, w} R₀ R P.Ring

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
R₁ : Type u_2
inst_7 : CommRing R₁
inst_8 : Algebra R₁ R
inst_9 : Algebra R₁ S
inst_10 : IsScalarTower R₁ R S
inst_11 : Algebra R₀ R₁
inst_12 : IsScalarTower R₀ R₁ R
rw :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
rw₁ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₁ R)) (algebraMap R₀ R₁))
rw₂ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ R) (algebraMap R₀ R₁)))
rw₃ rw₄ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
⊢ Eq (α := RingHom.{u_1, w} R₀ P.Ring) (algebraMap R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))

Tactic:
rw [IsScalarTower.algebraMap_eq R₀ R, IsScalarTower.algebraMap_eq R₁ R,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R₀ R₁ R]

Premises used: RingHom.comp_assoc, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
rw :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R)))
rw₁ :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp.{u, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R P.Ring))
      (algebraMap R₀ R))
rw₂ :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R₀ R))
rw₃ rw₄ : Eq (α := R₀ →+* S) (algebraMap R₀ S) (algebraMap R₀ S)
⊢ Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R₀ P.Ring))

Tactic:
rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

Premises used: RingHom.comp_assoc, Algebra.Extension.Ring, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
rw₁ rw₂ : x * y = x * y
⊢ P.σ x • y = x * y

Tactic:
rw [Algebra.smul_def, algebraMap_σ]

Premises used: Algebra.Extension.algebraMap_σ, Algebra.smul_def
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
e : P.σ x = P.σ y
rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = y
rw₁ :
  Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
rw₂ rw₃ :
  Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
⊢ x = y

Tactic:
rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]

Premises used: Algebra.Extension.algebraMap_σ
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
⊢ Function.Surjective.{w + 1, v + 1} (α := P.Ring) (β := S) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)

Tactic:
(⟨_, P.algebraMap_σ ·⟩)

Premises used: Algebra.Extension.algebraMap_σ, Exists.intro, Function.Surjective, Algebra.Extension.σ
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
⊢ ∀ (y : ↥(Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)),
    IsUnit.{u_1} (M := S')
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S) : (a : P.Ring) → S')
          (↑y : P.Ring) :
        S')

Tactic:
simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
this : Algebra.{w, u_1} (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :=
  RingHom.toAlgebra
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
h :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S')
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
⊢ IsScalarTower.{u, w, u_1} R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S'

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
s : S'
⊢ Membership.mem (γ := Submonoid P.Ring) (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
    (P.σ (↑(IsLocalization.sec M s).2 : S))

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
s : S'
⊢ (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :
        (a : Localization (Submonoid.comap (algebraMap P.Ring S) M)) → S')
      (Localization.mk (P.σ (IsLocalization.sec M s).1)
        (Subtype.mk (p := fun (x : P.Ring) ↦
          Membership.mem (γ := Submonoid P.Ring)
            (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M) x)
          (P.σ (↑(IsLocalization.sec M s).2 : S)) ⋯)) =
    s

Tactic:
simp [RingHom.algebraMap_toAlgebra, Localization.mk_eq_mk', IsLocalization.lift_mk',
      Units.mul_inv_eq_iff_eq_mul, IsUnit.coe_liftRight, IsLocalization.sec_spec]

Premises used: Localization.mk_eq_mk', Units.mul_inv_eq_iff_eq_mul, IsLocalization.lift_mk', IsUnit.coe_liftRight, IsLocalization.sec_spec, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
⊢ Eq (α := Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) (ker P.baseChange)
    (Ideal.map (F := P.Ring →+* TensorProduct.{u, u_1, w} R T P.Ring) (AlgHom.toRingHom TensorProduct.includeRight)
      P.ker)

Tactic:
Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
    P.algebraMap_surjective

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, IsScalarTower.toAlgHom, Algebra.Extension.algebraMap_surjective, Ideal.map, Algebra.Extension.Ring, Quotient, Ideal.comap, Algebra.TensorProduct.lTensor_ker, TensorProduct, AddCon.Quotient, RingHom.ker, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
x : R
simp :
  Eq (α := TensorProduct.{u, u_1, w} R T P.Ring)
    ((algebraMap R (TensorProduct.{u, u_1, w} R T P.Ring) : (a : R) → T ⊗[R] P.Ring) x :
      TensorProduct.{u, u_1, w} R T P.Ring)
    ((algebraMap R T : (a : R) → T) x ⊗ₜ[R] 1 : TensorProduct.{u, u_1, w} R T P.Ring)
⊢ Eq (α := Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((algebraMap R (Ring (R := T) (S := T ⊗[R] S) P.baseChange) : (a : R) → P.baseChange.Ring) x :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((algebraMap P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) : (a : P.Ring) → P.baseChange.Ring)
        ((algebraMap R P.Ring : (a : R) → P.Ring) x) :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
simp [baseChange, RingHom.algebraMap_toAlgebra]

Premises used: Algebra.Extension.baseChange, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Extension.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
x : R
⊢ Eq (α := TensorProduct.{u, u_1, w} R T P.Ring)
    ((algebraMap R (TensorProduct.{u, u_1, w} R T P.Ring) : (a : R) → T ⊗[R] P.Ring) x :
      TensorProduct.{u, u_1, w} R T P.Ring)
    ((algebraMap R T : (a : R) → T) x ⊗ₜ[R] 1 : TensorProduct.{u, u_1, w} R T P.Ring)

Tactic:
rfl