awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hprod₁ : f i * ∏ x ∈ s.erase i, f x = c ^ n
⊢ i ∈ s

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

Premises used: Finset.prod_insert, Finset.notMem_erase, Finset.insert_erase
-- 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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ (d : R), f i = d ^ n

Tactic:
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

Premises used: exists_eq_pow_of_mul_eq_pow_of_coprime, Finset.erase_subset, IsCoprime.prod_right
-- 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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
fun : ∀ (j : ι) (hj : j ∈ s.erase i) (hij : i = j), False
⊢ ∃ (d : R), f i = d ^ n

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

Premises used: exists_eq_pow_of_mul_eq_pow_of_coprime, Finset.erase_subset, IsCoprime.prod_right
-- 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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : i = j
⊢ j ∈ s.erase j

Tactic:
rw [hij] at hj
-- 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)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : i = j
hj₁ : j ∈ s.erase j
⊢ i = j

Tactic:
rw [hij] at hj
-- 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)
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:
(s.notMem_erase _) hj

Premises used: Finset.notMem_erase
-- 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)
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:
exact (s.notMem_erase _) hj

Premises used: Finset.notMem_erase
-- 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
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
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
⊢ ∀ 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
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Finite R
intro : ∀ (val : Fintype R), IsField R
⊢ IsField R

Tactic:
cases nonempty_fintype R

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Finite R
val : Fintype R
⊢ IsField R

Tactic:
@Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)

Premises used: Field.toIsField
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Finite R
val : Fintype R
⊢ IsField R

Tactic:
exact @Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)

Premises used: Field.toIsField
-- Module: Mathlib.RingTheory.IntegralDomain
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
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)
⊢ 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 _
-- Module: Mathlib.RingTheory.IntegralDomain
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
this : DecidableEq R
⊢ Set.MapsTo (⇑f : (a : G) → R) (↑{g : G | g ^ n = g₀} : Set G)
    (↑(Multiset.toFinset (nthRoots n ((f : (a : G) → R) g₀)) : Finset R) : Set R)

Tactic:
aesop (add safe unfold Set.MapsTo)

Premises used: Set.MapsTo
-- Module: Mathlib.RingTheory.IntegralDomain
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
this : DecidableEq R
⊢ card.{u_1} (α := R) (Multiset.toFinset (nthRoots n ((f : (a : G) → R) g₀)) : Finset R) ≤
    Multiset.card.{u_1} (α := R) (nthRoots n ((f : (a : G) → R) g₀) : Multiset R)

Tactic:
(nthRoots n (f g₀)).toFinset_card_le

Premises used: Multiset.toFinset_card_le, Polynomial.nthRoots, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralDomain
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
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:
calc
    _ ≤ #(nthRoots n (f g₀)).toFinset :=
      card_le_card_of_injOn f (by aesop (add safe unfold Set.MapsTo)) hf.injOn
    _ ≤ _ := (nthRoots n (f g₀)).toFinset_card_le

Premises used: Multiset.toFinset, Function.Injective.injOn, Multiset.toFinset_card_le, Finset.card_le_card_of_injOn, Polynomial.nthRoots, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralDomain
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

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.IntegralDomain
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
intro : ∀ (n : ℕ), 0 < n → card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n
⊢ IsCyclic G

Tactic:
apply isCyclic_of_card_pow_eq_one_le

Premises used: isCyclic_of_card_pow_eq_one_le
-- Module: Mathlib.RingTheory.IntegralDomain
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
n : ℕ
hn : 0 < n
⊢ card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n

Tactic:
le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Premises used: Polynomial.card_nthRoots, card_nthRoots_subgroup_units, OfNat.ofNat, DFunLike.coe, le_trans
-- Module: Mathlib.RingTheory.IntegralDomain
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
n : ℕ
hn : 0 < n
⊢ card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n

Tactic:
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Premises used: Polynomial.card_nthRoots, card_nthRoots_subgroup_units, OfNat.ofNat, DFunLike.coe, le_trans
-- Module: Mathlib.RingTheory.IntegralDomain
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
intro₁ intro₂ : ∀ (val : Fintype G) (n : ℕ) (hn : 0 < n), card.{u_2} (α := G) {a : G | a ^ n = 1} ≤ n
⊢ 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))

Premises used: nonempty_fintype, isCyclic_of_card_pow_eq_one_le
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Finite.{u_1 + 1} Rˣ
⊢ IsCyclic.{u_1} Rˣ

Tactic:
isCyclic_of_injective_ringHom (Units.coeHom R) Units.val_injective

Premises used: Units.coeHom, Units.val_injective, isCyclic_of_injective_ringHom
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
S : Subgroup Rˣ
inst_3 : Finite.{u_1 + 1} ↥S
⊢ ∀ (x y : ↥S), (↑(↑(x * y) : Rˣ) : R) = (↑(↑x : Rˣ) : R) * (↑(↑y : Rˣ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralDomain
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))

Tactic:
⟨f /ₘ g, f %ₘ g, ?_, ?_⟩

Premises used: Polynomial.divByMonic, Polynomial.modByMonic, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.IntegralDomain
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
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))
⊢ ∃ (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))

Tactic:
refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩
-- Module: Mathlib.RingTheory.IntegralDomain
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
⊢ (f %ₘ g).degree < g.degree

Tactic:
degree_modByMonic_lt _ hg

Premises used: Polynomial.degree_modByMonic_lt
-- Module: Mathlib.RingTheory.IntegralDomain
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
⊢ (f %ₘ g).degree < g.degree

Tactic:
exact degree_modByMonic_lt _ hg

Premises used: Polynomial.degree_modByMonic_lt
-- Module: Mathlib.RingTheory.IntegralDomain
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
⊢ 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)
-- Module: Mathlib.RingTheory.IntegralDomain
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)
      (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)
⊢ 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:
field_simp
-- Module: Mathlib.RingTheory.IntegralDomain
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)
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)
refine_2₃ 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 : 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)

Tactic:
rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]

Premises used: map_add, add_comm, map_mul, Polynomial.modByMonic_add_div
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
obtain :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y),
    Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0

Tactic:
obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits)

Premises used: IsCyclic.exists_monoid_generator
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
rw : (↑(↑x : Rˣ) : R) ≠ 1
⊢ (↑(↑x : Rˣ) : R) - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
contrapose : ∀ (hf : (↑(↑x : Rˣ) : R) = 1), f = 1
⊢ (↑(↑x : Rˣ) : R) ≠ 1

Tactic:
contrapose hf
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hf : (↑(↑x : Rˣ) : R) = 1
h : ∀ (g : G), Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)
⊢ f = 1

Tactic:
ext g
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hf : (↑(↑x : Rˣ) : R) = 1
g : G
h :
  ∀ (n : ℕ)
    (hn :
      Eq.{u_1 + 1} (α := ↥f.toHomUnits.range) ((fun (x_1 : ℕ) ↦ x ^ x_1) n : ↥f.toHomUnits.range)
        (Subtype.mk (p := fun (x : Rˣ) ↦ x ∈ f.toHomUnits.range) ((f.toHomUnits : (a : G) → Rˣ) g) ⋯ :
          ↥f.toHomUnits.range)),
    Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)

Tactic:
obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩

Premises used: MonoidHom.toHomUnits, Subtype.mk, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hf : (↑(↑x : Rˣ) : R) = 1
g : G
n : ℕ
hn :
  Eq.{u_1 + 1} (α := ↥f.toHomUnits.range) ((fun (x_1 : ℕ) ↦ x ^ x_1) n : ↥f.toHomUnits.range)
    (Subtype.mk (p := fun (x : Rˣ) ↦ x ∈ f.toHomUnits.range) ((f.toHomUnits : (a : G) → Rˣ) g) ⋯ : ↥f.toHomUnits.range)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)

Tactic:
simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm

Premises used: Units.ext_iff, Subtype.ext_iff, Eq.symm
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
⊢ (↑(↑x : Rˣ) : R) - 1 ≠ 0

Tactic:
have hx1 : (x.1 : R) - 1 ≠ 0 := by
      rw [sub_ne_zero]
      contrapose hf
      ext g
      obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
      simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g)
    (∑ u ∈ image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ,
      card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} • (↑u : R))

Tactic:
sum_comp ((↑) : Rˣ → R) f.toHomUnits

Premises used: Units.val, MonoidHom.toHomUnits, Finset.sum_comp, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R)
    (∑ u ∈ image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ,
      card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} • (↑u : R))
    (∑ u ∈ image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ, c • (↑u : R))

Tactic:
(sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)

Premises used: HSMul.hSMul, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ ∀ (x : Rˣ),
    Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) x ↔
      x ∈ f.toHomUnits.range

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ ∑ b : ↥f.toHomUnits.range, c • (↑(↑b : Rˣ) : R) = HSMul.hSMul (β := R) c (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R))

Tactic:
smul_sum.symm

Premises used: Finset.smul_sum, Eq.symm
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ HSMul.hSMul (β := R) c (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) = HSMul.hSMul (β := R) c 0

Tactic:
congr_arg₂ _ rfl ?_

Premises used: rfl, congr_arg₂
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ HSMul.hSMul (β := R) c 0 = 0

Tactic:
smul_zero _

Premises used: smul_zero