awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
x : T
h : (g.comp f).IsIntegralElem x
p : R[X]
hp : p.Monic
hp' : eval₂ (g.comp f) x p = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hp' : eval₂ g x (Polynomial.map f p) = 0), eval₂ g x (Polynomial.map f p) = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
rwa [← eval₂_map] at hp'

Premises used: Polynomial.eval₂_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
h : (g.comp f).IsIntegral
⊢ g.IsIntegral

Tactic:
fun x ↦ RingHom.isIntegralElem.of_comp f g (h x)

Premises used: RingHom.isIntegralElem.of_comp, RingHom.IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h : Algebra.IsIntegral R T
apply : RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
⊢ ∀ (x : T), IsIntegral S x

Tactic:
apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)

Premises used: Algebra.algebraMap, RingHom.IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h : Algebra.IsIntegral R T
rw : RingHom.IsIntegral (algebraMap R T)
⊢ RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq R S T]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral (algebraMap R T)

Tactic:
h.isIntegral

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral, RingHom.IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral (algebraMap R T)

Tactic:
exact h.isIntegral

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x_1 : S ⧸ I
x : S
mk :
  ∀ (p : R[X]) (p_monic : p.Monic) (hpx : eval₂ f x p = 0),
    IsIntegralElem (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
⊢ IsIntegralElem (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)

Tactic:
obtain ⟨p, p_monic, hpx⟩ := hf x
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x_1 : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ IsIntegralElem (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)

Tactic:
⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩

Premises used: Ideal.Quotient.mk, RingHom.IsIntegralElem, And.intro, Exists.intro, Polynomial.map, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x_1 : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
mk :
  eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0
⊢ IsIntegralElem (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)

Tactic:
refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x_1 : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0

Tactic:
simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx

Premises used: Ideal.Quotient.mk, Polynomial.hom_eval₂, Polynomial.eval₂_map, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra A B
inst_6 : Algebra R B
f : R →+* S
g : S →+* T
inst_7 : Algebra R A
inst_8 : IsScalarTower R A B
I : Ideal A
inst_9 : Algebra.IsIntegral R A
⊢ Algebra.IsIntegral.{u_1, u_2} R (A ⧸ I)

Tactic:
Algebra.IsIntegral.trans A

Premises used: Algebra.IsIntegral.trans
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra A B
inst_6 : Algebra R B
f : R →+* S
g : S →+* T
inst_7 : Algebra R A
inst_8 : IsScalarTower R A B
I : Ideal A
inst_9 : Algebra.IsIntegral R A
⊢ Algebra.IsIntegral.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* A) (algebraMap R A) I))
    (A ⧸ I)

Tactic:
⟨RingHom.IsIntegral.quotient (algebraMap R A) Algebra.IsIntegral.isIntegral⟩

Premises used: Algebra.IsIntegral.isIntegral, Algebra.algebraMap, RingHom.IsIntegral.quotient, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
⊢ Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)

Tactic:
have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
    Ideal.quotientMap_comp_mk le_rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
⊢ RingHom.IsIntegral (Ideal.quotientMap I f ⋯) ↔ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)

Tactic:
⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩

Premises used: le_rfl, RingHom.IsIntegral.tower_top, Eq.rec, Iff.intro, Ideal.quotientMap
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
refine : ∀ (h : RingHom.IsIntegral (Ideal.quotientMap I f ⋯)), RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
⊢ RingHom.IsIntegral (Ideal.quotientMap I f ⋯) ↔ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)

Tactic:
refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
h : RingHom.IsIntegral (Ideal.quotientMap I f ⋯)
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)

Tactic:
this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h

Premises used: le_rfl, Eq.rec, RingHom.IsIntegral.trans, Ideal.quotientMap
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
h : RingHom.IsIntegral (Ideal.quotientMap I f ⋯)
refine : g.IsIntegral
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)

Tactic:
refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
h : RingHom.IsIntegral (Ideal.quotientMap I f ⋯)
⊢ g.IsIntegral

Tactic:
g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

Premises used: RingHom.isIntegral_of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal S
g : R →+* HasQuotient.Quotient R (B := Ideal R) (Ideal.comap f I) := Ideal.Quotient.mk (Ideal.comap f I)
this :
  Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f ⋯) g)
    (RingHom.comp (Ideal.Quotient.mk I) f)
h : RingHom.IsIntegral (Ideal.quotientMap I f ⋯)
⊢ g.IsIntegral

Tactic:
exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

Premises used: RingHom.isIntegral_of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_4} (M := S) ((f : (a : R) → S) a : S)
obtain : ∀ (p : R[X]) (p_monic : p.Monic) (hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0), IsUnit a
⊢ IsUnit a

Tactic:
obtain ⟨p, p_monic, hp⟩ := hf (ha.unit⁻¹ : _)

Premises used: Units.val, Inv.inv, IsUnit.unit
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_4} (M := S) ((f : (a : R) → S) a : S)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0
⊢ IsUnit a

Tactic:
.of_mul_eq_one (-p.reverse.divX.eval a) ?_

Premises used: Polynomial.eval, IsUnit.of_mul_eq_one, Polynomial.divX, Polynomial.reverse, Neg.neg
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_4} (M := S) ((f : (a : R) → S) a : S)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0
refine : a * -eval a p.reverse.divX = 1
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one (-p.reverse.divX.eval a) ?_
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_4} (M := S) ((f : (a : R) → S) a : S)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0
nth_rewrite : eval₂ f ((f : (a : R) → S) a) p.reverse = 0
⊢ a * -eval a p.reverse.divX = 1

Tactic:
nth_rewrite 1 [mul_neg, ← eval_X (x := a), ← eval_mul, ← p_monic, ← coeff_zero_reverse,
      ← add_eq_zero_iff_neg_eq, ← eval_C (a := p.reverse.coeff 0), ← eval_add, X_mul_divX_add,
      ← (injective_iff_map_eq_zero' _).mp inj, ← eval₂_hom]

Premises used: Polynomial.eval₂_hom, Polynomial.eval_C, Polynomial.eval_X, Polynomial.X_mul_divX_add, Polynomial.eval_mul, injective_iff_map_eq_zero', add_eq_zero_iff_neg_eq, Polynomial.eval_add, Iff.mp, Polynomial.coeff_zero_reverse, mul_neg
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
ha : IsUnit.{u_4} (M := S) ((f : (a : R) → S) a : S)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hp : eval₂ f (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ha.unit⁻¹ : S) _) p.reverse = 0),
    eval₂ f ((f : (a : R) → S) a) p.reverse = 0
⊢ eval₂ f ((f : (a : R) → S) a) p.reverse = 0

Tactic:
rwa [← eval₂_reverse_eq_zero_iff] at hp

Premises used: Polynomial.eval₂_reverse_eq_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : CommRing T
inst_5 : Algebra A B
inst_6 : Algebra R B
f : R →+* S
g : S →+* T
inst_7 : Algebra R A
inst_8 : IsScalarTower R A B
inst_9 : Algebra R S
inst_10 : Algebra.IsIntegral R S
inst_11 : FaithfulSMul R S
⊢ IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)

Tactic:
(algebraMap_isIntegral_iff.mpr ‹_›).isLocalHom (FaithfulSMul.algebraMap_injective R S)

Premises used: Iff.mpr, algebraMap_isIntegral_iff, RingHom.IsIntegral.isLocalHom, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
hRS : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
hS : IsField S
⊢ IsField R

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R S).mpr hRS
  IsLocalHom.isField hRS hS

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, IsLocalHom.isField
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsDomain S
hRS : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsField R ↔ IsField S

Tactic:
⟨isField_of_isIntegral_of_isField', isField_of_isIntegral_of_isField hRS⟩

Premises used: isField_of_isIntegral_of_isField, Iff.intro, isField_of_isIntegral_of_isField'
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
inst_2 : Algebra.IsIntegral ℤ R
I : Ideal R
inst_3 : I.IsMaximal
⊢ I ≠ ⊥

Tactic:
Ring.ne_bot_of_isMaximal_of_not_isField ‹_› fun h ↦ Int.not_isField
    (isField_of_isIntegral_of_isField (FaithfulSMul.algebraMap_injective ℤ R) h)

Premises used: Ring.ne_bot_of_isMaximal_of_not_isField, Int.not_isField, Int, isField_of_isIntegral_of_isField, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
k : Type u_6
inst_1 : Field k
inst_2 : Algebra R k
inst_3 : Algebra.IsIntegral R k
⊢ Ideal.IsMaximal.{u_6} (α := k) ⊥

Tactic:
have := Ideal.bot_isMaximal (K := k)
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
k : Type u_6
inst_1 : Field k
inst_2 : Algebra R k
inst_3 : Algebra.IsIntegral R k
this : Ideal.IsMaximal.{u_6} (α := k) ⊥
rw : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
⊢ Ideal.IsMaximal (RingHom.ker (F := R →+* k) (algebraMap R k))

Tactic:
rw [RingHom.ker, Ideal.Quotient.maximal_ideal_iff_isField_quotient]

Premises used: Ideal.Quotient.maximal_ideal_iff_isField_quotient, RingHom.ker
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
k : Type u_6
inst_1 : Field k
inst_2 : Algebra R k
inst_3 : Algebra.IsIntegral R k
this : Ideal.IsMaximal.{u_6} (α := k) ⊥
⊢ IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))

Tactic:
isField_of_isIntegral_of_isField Ideal.algebraMap_quotient_injective
    (Ideal.Quotient.field _).toIsField

Premises used: Ideal.algebraMap_quotient_injective, Field.toIsField, isField_of_isIntegral_of_isField
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
inst : CommRing R
k : Type u_6
inst_1 : Field k
inst_2 : Algebra R k
inst_3 : Algebra.IsIntegral R k
this : Ideal.IsMaximal.{u_6} (α := k) ⊥
⊢ IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))

Tactic:
exact isField_of_isIntegral_of_isField Ideal.algebraMap_quotient_injective
    (Ideal.Quotient.field _).toIsField

Premises used: Field.toIsField, isField_of_isIntegral_of_isField
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra (↥(integralClosure R A)) A) (integralClosure (↥(integralClosure R A)) A) ⊥

Tactic:
letI := (integralClosure R A).algebra
  eq_bot_iff.2 fun x hx ↦ Algebra.mem_bot.2
    ⟨⟨x, isIntegral_trans (A := integralClosure R A) x hx⟩, rfl⟩

Premises used: Iff.mpr, Algebra.mem_bot, isIntegral_trans, Subtype.mk, Exists.intro, eq_bot_iff, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
⊢ IsDomain.{u_2} ↥(integralClosure R S)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
f : R[X]
hf : f.Monic
a : S
ha : a ∈ f.aroots S
⊢ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a

Tactic:
⟨f, hf, (eval₂_eq_eval_map _).trans <| (mem_roots <| (hf.map _).ne_zero).1 ha⟩

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, Polynomial.mem_roots, And.intro, Exists.intro, Iff.mp, Polynomial.Monic.map, Polynomial.eval₂_eq_eval_map, Eq.trans, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : Finite M
inst_2 : IsLeftCancelMulZero M
a : M
ha : a ≠ 0
⊢ Bijective (β := M) fun (b : M) ↦ a * b

Tactic:
Finite.injective_iff_bijective.1 <| mul_right_injective₀ ha

Premises used: mul_right_injective₀, Finite.injective_iff_bijective, Iff.mp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : Finite M
inst_2 : IsRightCancelMulZero M
a : M
ha : a ≠ 0
⊢ Bijective (β := M) fun (b : M) ↦ b * a

Tactic:
Finite.injective_iff_bijective.1 <| mul_left_injective₀ ha

Premises used: mul_left_injective₀, Finite.injective_iff_bijective, Iff.mp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M_1 : Type u_1
inst : MonoidWithZero M_1
inst_1 : Finite M_1
M : Type u_2
inst_2 : MonoidWithZero M
inst_3 : IsLeftCancelMulZero M
inst_4 : DecidableEq M
inst_5 : Fintype M
inst_6 : Nontrivial M
⊢ Eq.{u_2 + 1} (α := M) (if h : Eq.{u_2 + 1} (α := M) 0 0 then 0 else bijInv ⋯ 1) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M_1 : Type u_1
inst : MonoidWithZero M_1
inst_1 : Finite M_1
M : Type u_2
inst_2 : MonoidWithZero M
inst_3 : IsLeftCancelMulZero M
inst_4 : DecidableEq M
inst_5 : Fintype M
inst_6 : Nontrivial M
a : M
ha : a ≠ 0
simp : a * bijInv ⋯ 1 = 1
⊢ (a * if h : a = 0 then 0 else bijInv ⋯ 1) = 1

Tactic:
simp only [dif_neg ha]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M_1 : Type u_1
inst : MonoidWithZero M_1
inst_1 : Finite M_1
M : Type u_2
inst_2 : MonoidWithZero M
inst_3 : IsLeftCancelMulZero M
inst_4 : DecidableEq M
inst_5 : Fintype M
inst_6 : Nontrivial M
a : M
ha : a ≠ 0
⊢ a * bijInv ⋯ 1 = 1

Tactic:
Fintype.rightInverse_bijInv _ _

Premises used: Fintype.rightInverse_bijInv
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
M_1 : Type u_1
inst : MonoidWithZero M_1
inst_1 : Finite M_1
M : Type u_2
inst_2 : MonoidWithZero M
inst_3 : IsLeftCancelMulZero M
inst_4 : DecidableEq M
inst_5 : Fintype M
inst_6 : Nontrivial M
a : M
ha : a ≠ 0
⊢ a * bijInv ⋯ 1 = 1

Tactic:
exact Fintype.rightInverse_bijInv _ _

Premises used: Fintype.rightInverse_bijInv
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ (d : R), a = d ^ n

Tactic:
exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h

Premises used: exists_eq_pow_of_mul_eq_pow, isUnit_of_dvd_one
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
refine : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1
⊢ ∃ (d : R), a = d ^ n

Tactic:
refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h

Premises used: exists_eq_pow_of_mul_eq_pow, isUnit_of_dvd_one
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
obtain : ∀ (x y : R) (hxy : x * a + y * b = 1), @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1

Tactic:
obtain ⟨x, y, hxy⟩ := cp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
rw : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ x * a + y * b
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1

Tactic:
rw [← hxy]
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ x * a + y * b

Tactic:
dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)

Premises used: dvd_mul_of_dvd_right, dvd_add
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ x * a + y * b

Tactic:
exact dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)

Premises used: dvd_mul_of_dvd_right, dvd_add
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
ι : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : GCDMonoid R
inst_2 : Subsingleton.{u_3 + 1} Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ f i * ∏ x ∈ s.erase i, f x = c ^ n

Tactic:
rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod

Premises used: Finset.prod_insert, Finset.notMem_erase, Finset.insert_erase