awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 : IsDomain S
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsTorsionFree S T
inst_8 : Nontrivial T
inst_9 : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
have rw : RingHom.IsIntegral (algebraMap R T)
Tactic: rw [← IsScalarTower.algebraMap_eq R S T]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ g x (Polynomial.map f p) = 0
have rwa : ∀ (hp' : eval₂ g x (Polynomial.map f p) = 0), eval₂ g x (Polynomial.map f p) = 0
Tactic: rwa [← eval₂_map] at hp'
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ ∀ (x : T), IsIntegral S x
have apply : RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
Tactic: apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
have rw : RingHom.IsIntegral (algebraMap R T)
Tactic: rw [← IsScalarTower.algebraMap_eq R S T]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ IsIntegralElem (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
have mk : ∀ (p : R[X]) (p_monic : p.Monic) (hpx : eval₂ f x p = 0),
  IsIntegralElem (Ideal.quotientMap I f sorry) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
Tactic: obtain ⟨p, p_monic, hpx⟩ := hf x
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
have mk : eval₂ (Ideal.quotientMap I f sorry) (Quot.mk (⇑(quotientRel I) : S → S → Prop) x)
    (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
  0
Tactic: refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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)
⊢ RingHom.IsIntegral (Ideal.quotientMap I f ⋯) ↔ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
have this : Eq (α := RingHom.{u_1, u_4} R (S ⧸ I)) (RingHom.comp (Ideal.quotientMap I f sorry) 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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
have refine : ∀ (h : RingHom.IsIntegral (Ideal.quotientMap I f sorry)), RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
Tactic: refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
have refine : g.IsIntegral
Tactic: refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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)
⊢ IsUnit a
have obtain : ∀ (p : R[X]) (p_monic : p.Monic) (hp : eval₂ f (↑ha.unit⁻¹ : S) p = 0), IsUnit a
Tactic: obtain ⟨p, p_monic, hp⟩ := hf (ha.unit⁻¹ : _)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
have refine : a * -eval a p.reverse.divX = 1
Tactic: refine .of_mul_eq_one (-p.reverse.divX.eval a) ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ a * -eval a p.reverse.divX = 1
have nth_rewrite : eval₂ f ((f : (a : R) → S) a) p.reverse = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ eval₂ f ((f : (a : R) → S) a) p.reverse = 0
have 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
Tactic: rwa [← eval₂_reverse_eq_zero_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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 (RingHom.ker (F := R →+* k) (algebraMap R k))
have this : Ideal.IsMaximal.{u_6} (α := k) ⊥
Tactic: have := Ideal.bot_isMaximal (K := k)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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) ⊥
⊢ Ideal.IsMaximal (RingHom.ker (F := R →+* k) (algebraMap R k))
have rw : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
Tactic: rw [RingHom.ker, Ideal.Quotient.maximal_ideal_iff_isField_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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 * if h : a = 0 then 0 else bijInv ⋯ 1) = 1
have simp : a * bijInv sorry 1 = 1
Tactic: simp only [dif_neg ha]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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
have refine : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1
Tactic: refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1
have obtain : ∀ (x y : R) (hxy : x * a + y * b = 1), @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ 1
Tactic: obtain ⟨x, y, hxy⟩ := cp
Cleared hypotheses: cp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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 ∣ 1
have rw : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ x * a + y * b
Tactic: rw [← hxy]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (hypothesis)
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
⊢ ∃ (d : R), f i = d ^ n
have hprod₁ : f i * ∏ x ∈ s.erase i, f x = c ^ n
Tactic: rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
Cleared hypotheses: hprod, hi
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ (d : R), f i = d ^ n
have fun : ∀ (j : ι) (hj : j ∈ s.erase i) (hij : i = j), False
Tactic: refine
      exists_eq_pow_of_mul_eq_pow_of_coprime
        (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (hypothesis)
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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : i = j
⊢ False
have hj₁ : j ∈ s.erase j
Tactic: rw [hij] at hj
Cleared hypotheses: hj, hij
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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
intro intro₁ : ∀ (i : ι) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
⊢ ∀ i ∈ s, ∃ (d : R), f i = d ^ n
have intro₂ : ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
Tactic: classical
    intro i hi
    rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
    refine
      exists_eq_pow_of_mul_eq_pow_of_coprime
        (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
    rw [hij] at hj
    exact (s.notMem_erase _) hj
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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
intro intro₁ : ∀ (i : ι) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
intro₂ : ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
⊢ ∀ i ∈ s, ∃ (d : R), f i = d ^ n
have intro₃ : ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s) (j : ι) (hj : j ∈ s.erase i) (hij : i = j), False
Tactic: classical
    intro i hi
    rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
    refine
      exists_eq_pow_of_mul_eq_pow_of_coprime
        (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
    rw [hij] at hj
    exact (s.notMem_erase _) hj
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
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
intro intro₁ : ∀ (i : ι) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
intro₂ : ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s), ∃ (d : R), f i = d ^ n
intro₃ :
  ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s) (j : ι) (hj : j ∈ s.erase i) (hij : i = j), False
⊢ ∀ i ∈ s, ∃ (d : R), f i = d ^ n
have intro₄ : ∀ (i : ι) (hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n) (hi : i ∈ s) (j : ι) (hj : j ∈ s.erase j) (hij : i = j), False
Tactic: classical
    intro i hi
    rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
    refine
      exists_eq_pow_of_mul_eq_pow_of_coprime
        (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
    rw [hij] at hj
    exact (s.notMem_erase _) hj
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Finite R
⊢ IsField R
have intro : ∀ (val : Fintype R), IsField R
Tactic: cases nonempty_fintype R
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
inst_4 : DecidableEq G
f : G →* R
hf : Injective.{u_2 + 1, u_1 + 1} (α := G) (β := R) (⇑f : (a : G) → R)
n : ℕ
hn : 0 < n
g₀ : G
⊢ card.{u_2} (α := G) {g : G | g ^ n = g₀} ≤
    Multiset.card.{u_1} (α := R) (nthRoots n ((f : (a : G) → R) g₀) : Multiset R)
have haveI : ∀ (this : DecidableEq R),
  card.{u_2} (α := G) {g : G | g ^ n = g₀} ≤
    Multiset.card.{u_1} (α := R) (nthRoots n ((f : (a : G) → R) g₀) : Multiset R)
Tactic: haveI : DecidableEq R := Classical.decEq _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Finite G
f : G →* R
hf : Injective.{u_2 + 1, u_1 + 1} (α := G) (β := R) (⇑f : (a : G) → R)
⊢ IsCyclic G
have intro : ∀ (val : Fintype G), IsCyclic G
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Finite G
f : G →* R
hf : Injective.{u_2 + 1, u_1 + 1} (α := G) (β := R) (⇑f : (a : G) → R)
val : Fintype G
⊢ IsCyclic G
have intro : ∀ (n : ℕ), 0 < n → card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n
Tactic: apply isCyclic_of_card_pow_eq_one_le
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Finite G
f : G →* R
hf : Injective.{u_2 + 1, u_1 + 1} (α := G) (β := R) (⇑f : (a : G) → R)
⊢ IsCyclic G
have intro : ∀ (val : Fintype G), IsCyclic G
Tactic: classical
    cases nonempty_fintype G
    apply isCyclic_of_card_pow_eq_one_le
    intro n hn
    exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Finite G
f : G →* R
hf : Injective.{u_2 + 1, u_1 + 1} (α := G) (β := R) (⇑f : (a : G) → R)
intro : ∀ (val : Fintype G), IsCyclic G
⊢ IsCyclic G
have intro₁ : ∀ (val : Fintype G) (n : ℕ), 0 < n → card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n
Tactic: classical
    cases nonempty_fintype G
    apply isCyclic_of_card_pow_eq_one_le
    intro n hn
    exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
⊢ ∃ (q : R[X]) (r : R[X]),
    r.degree < g.degree ∧
      HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
          ((algebraMap R[X] K : (a : R[X]) → K) g : K) =
        HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) r : K)
            ((algebraMap R[X] K : (a : R[X]) → K) g : K))
have refine_1 : (f %ₘ g).degree < g.degree
Tactic: refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
refine_1 : (f %ₘ g).degree < g.degree
⊢ ∃ (q : R[X]) (r : R[X]),
    r.degree < g.degree ∧
      HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
          ((algebraMap R[X] K : (a : R[X]) → K) g : K) =
        HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) q : K)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) r : K)
            ((algebraMap R[X] K : (a : R[X]) → K) g : K))
have refine_2 : HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) =
  HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      ((algebraMap R[X] K : (a : R[X]) → K) g : K))
Tactic: refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((algebraMap R[X] K : (a : R[X]) → K) g : K) =
    HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
        ((algebraMap R[X] K : (a : R[X]) → K) g : K))
have hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
Tactic: have hg' : algebraMap R[X] K g ≠ 0 :=
      (map_ne_zero_iff _ (IsFractionRing.injective R[X] K)).mpr (Monic.ne_zero hg)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
      ((algebraMap R[X] K : (a : R[X]) → K) g : K) =
    HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
        ((algebraMap R[X] K : (a : R[X]) → K) g : K))
have refine_2 : (algebraMap R[X] K : (a : R[X]) → K) f =
  HAdd.hAdd (β := K)
    (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
      ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
    ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
⊢ (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
      ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
have refine_2 : (algebraMap R[X] K : (a : R[X]) → K) f =
  HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
    (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
      ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
Tactic: rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
refine_2 :
  (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
⊢ (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
      ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
have refine_2₁ : (algebraMap R[X] K : (a : R[X]) → K) f =
  HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
    ((algebraMap R[X] K : (a : R[X]) → K) (g * (f /ₘ g)) : K)
Tactic: rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
refine_2 :
  (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
refine_2₁ :
  (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      ((algebraMap R[X] K : (a : R[X]) → K) (g * (f /ₘ g)) : K)
⊢ (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
      ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
have refine_2₂ : Eq.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
  ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g + g * (f /ₘ g)) : K)
Tactic: rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]