mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0

Tactic:
hb₂,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ eval₂ g x (b • p) = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits

Tactic:
refine ⟨fun h ↦ ?_, and_imp.mpr .mul⟩
  generalize hp : f * g = p at *
  generalize hn : p.natDegree = n
  induction n generalizing p f g with
  | zero =>
    rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn
    exact ⟨.of_natDegree_eq_zero hn.1, .of_natDegree_eq_zero hn.2⟩
  | succ n ih =>
    obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)
    have := dvd_iff_isRoot.mpr ha
    rw [← hp, (prime_X_sub_C a).dvd_mul] at this
    wlog hf : X - C a ∣ f with hf2
    · exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf
    obtain ⟨f, rfl⟩ := hf
    rw [mul_assoc] at hp; subst hp
    rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
    have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
    aesop

Goal state after:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * X + C b).Splits

Tactic:
rw [← mul_inv_cancel_left₀ ha b, C_mul, ← mul_add]
    exact (X_add_C (a⁻¹ * b)).C_mul a

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ IsIntegral R (r • z)

Tactic:
simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I hIP

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (algebraMap R S) P' ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
⊢ IsIntegral R t

Tactic:
by
  nontriviality S
  let φ := aeval (R := R) s
  obtain ⟨q, hqm, hqt⟩ : φ.IsIntegralElem t := by
    obtain ⟨p, hpm, hpt⟩ := ht
    have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])
    obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)
    exact ⟨q, hqm, by rw [← eval_map, hqp, eval_map, hpt]⟩
  let N := q.support.sup (q.coeff · |>.natDegree)
  have hN (i : _) : (q.coeff i).natDegree ≤ N := by
    by_cases hi : i ∈ q.support
    · exact Finset.le_sup (f := (q.coeff · |>.natDegree)) hi
    · simp_all
  let q' := q.sum fun i r ↦ X ^ i * r.reflect N
  have (i : _) : aeval t (reflect N (q.coeff i)) = t ^ N * (aeval s (q.coeff i)) := by
    let : Invertible t := ⟨s, hst, (mul_comm _ _).trans hst⟩
    rw [aeval_def, ← eval₂_reflect_mul_pow _ _ N _ ((natDegree_reflect_le ..).trans (by simp [hN]))]
    simp +instances [mul_comm, this, aeval_def]
  refine ⟨q', ?_, ?_⟩
  · refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_
    · refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_
      grw [natDegree_mul_le, natDegree_pow_le, natDegree_X_le, natDegree_reflect_le]
      simp [max_eq_left (hN _), le_natDegree_of_mem_supp _ hi]
    · simp only [sum, finsetSum_coeff, coeff_X_pow_mul', coeff_reflect, q']
      rw [Finset.sum_eq_single q.natDegree]
      · simp [hqm.leadingCoeff]
      · intro i hi₁ hi₂
        have : N + i < q.natDegree + N :=
          add_comm N i ▸ add_lt_add_left ((le_natDegree_of_mem_supp _ hi₁).lt_of_ne hi₂) _
        simpa [(le_natDegree_of_mem_supp _ hi₁).trans, revAt, this.not_ge] using
          coeff_eq_zero_of_natDegree_lt (by grind)
      · simp +contextual
  · trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)
    · simp [φ, q', Polynomial.sum, ← aeval_def, this, mul_left_comm _ (t ^ N), ← Finset.mul_sum]
    · simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommRing R
R' : Type u_4
S : Type u
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : IsFractionRing R R'
inst✝⁹ : FaithfulSMul R S
inst✝⁸ : Algebra.IsAlgebraic R S
inst✝⁷ : NoZeroDivisors S
S' : Type v
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R S'
inst✝⁴ : Algebra S S'
inst✝³ : Module R' S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsFractionRing S S'
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)

Tactic:
IsLocalization.rank_eq R' R⁰ le_rfl,

Goal state after:
R : Type u_1
inst✝¹⁵ : CommRing R
R' : Type u_4
S : Type u
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : IsFractionRing R R'
inst✝⁹ : FaithfulSMul R S
inst✝⁸ : Algebra.IsAlgebraic R S
inst✝⁷ : NoZeroDivisors S
S' : Type v
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R S'
inst✝⁴ : Algebra S S'
inst✝³ : Module R' S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsFractionRing S S'
⊢ Cardinal.lift.{u, v} (Module.rank R S') = Cardinal.lift.{v, u} (Module.rank R S)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ c * (a + b) = c

Tactic:
add_ab,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ c * 1 = c
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
I✝ : Ideal R
inst✝² : I✝.IsPrime
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
f : A →ₐ[R] B
hf : I = comap f.toRingHom J
r : R
⊢ (↑↑(map I J (↑f) hf)).toFun ((algebraMap R I.ResidueField) r) = (algebraMap R J.ResidueField) r

Tactic:
simp [IsScalarTower.algebraMap_apply R A I.ResidueField,
      IsScalarTower.algebraMap_apply R B J.ResidueField]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hbc : (↑b).1 * (↑c).1 = (↑b).1
⊢ (↑a).1 * ((↑b).1 * (↑c).1) = (↑a).1 * (↑b).1

Tactic:
hbc

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hbc : (↑b).1 * (↑c).1 = (↑b).1
⊢ (↑a).1 * (↑b).1 = (↑a).1 * (↑b).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a).1 + (↑a).2 * ((↑b).1 * (↑c).1) = (↑a).1 + (↑a).2 * (↑b).1

Tactic:
hbc

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a).1 + (↑a).2 * (↑b).1 = (↑a).1 + (↑a).2 * (↑b).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hbc : ↑b * ↑c = ↑b
⊢ ↑a * (↑b * ↑c) = ↑a * ↑b

Tactic:
hbc

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hbc : ↑b * ↑c = ↑b
⊢ ↑a * ↑b = ↑a * ↑b
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this : q.IsPrime
⊢ p = comap f q

Tactic:
have := (Ideal.comap_mono hq').trans_eq h₃

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this✝ : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : OrderBot α
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ ⊥ ≤ x✝

Tactic:
simp [eq_bot, le_eq]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝ : α
⊢ ⊥ ≤ x✝

Tactic:
simp [eq_bot, le_eq]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : le a✝ b✝
⊢ le b✝ c✝ → le a✝ c✝

Tactic:
hbc

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : le a✝ b✝
hbc : le b✝ c✝
⊢ le a✝ c✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
⊢ le b✝ c✝ → le (sup a✝ b✝) c✝

Tactic:
hbc

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
hbc : le b✝ c✝
⊢ le (sup a✝ b✝) c✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
⊢ le a✝ c✝ → le a✝ (inf b✝ c✝)

Tactic:
hbc

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
hbc : le a✝ c✝
⊢ le a✝ (inf b✝ c✝)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)

Tactic:
apply monotone_nat_of_le_succ

Goal state after:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat R S
⊢ Function.Injective ⇑f

Tactic:
exact FaithfulSMul.algebraMap_injective R S

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
← Nat.card_zpowers,

Goal state after:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥(zpowers g) = Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = orderOf a

Tactic:
← Nat.card_zpowers,

Goal state after:
case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = Nat.card ↥(zpowers a)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ {e.symm a} ∩ {e.symm b} = ↑⊥

Tactic:
exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
by_cases hy : orderOf y = 0

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
by_cases hy : orderOf y = 0

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ e (g ^ exponent H) = e 1

Tactic:
by
    rw [map_pow, pow_exponent_eq_one, map_one]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
⊢ p ∣ orderOf g

Tactic:
rw [hk]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : IsPGroup p G
g : G
hg : g ≠ 1
k : ℕ
hk : orderOf g = p ^ k
⊢ p ∣ p ^ k
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ (QuotientGroup.mk' K).ker)

Tactic:
← Subgroup.comap_map_eq

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
· exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ f.IsIntegral

Tactic:
by rwa [Algebra.isIntegral_def] at this

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect (b.natDegree + (1 + c.natDegree)) (p * c)) = 0

Tactic:
← add_assoc,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect (b.natDegree + 1 + c.natDegree) (p * c)) = 0
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ Nat.card ↥(center G)

Tactic:
rw [hk]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : Nat.card ↥(center G) = p ^ k
⊢ p ∣ p ^ k
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Infinite N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases subsingleton_or_nontrivial M; · simp
      rw [(MulEquiv.prodComm ..).isCyclic] at h
      exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
⊢ Nat.card ↑↑(comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x)) =
    Nat.card ↥(H.subgroupOf (normalizer ↑H)) * orderOf x

Tactic:
← Nat.card_zpowers,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
⊢ Nat.card ↑↑(comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x)) =
    Nat.card ↥(H.subgroupOf (normalizer ↑H)) * Nat.card ↥(zpowers x)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ (m - 1 + 1) ∣ Nat.card G

Tactic:
tsub_add_cancel_of_le h0m.nat_succ_le

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ m ∣ Nat.card G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ p ^ (m - 1 + 1) = p ^ m

Tactic:
tsub_add_cancel_of_le h0m.nat_succ_le

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ p ^ m = p ^ m
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ iSupIndep fun i ↦ ↑(P ↑i)

Tactic:
apply independent_of_coprime_order hcomm

Goal state after:
case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ _root_.Pairwise fun i j ↦ (Fintype.card ↥↑(P ↑i)).Coprime (Fintype.card ↥↑(P ↑j))
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ v ∈ I j

Tactic:
rw [Finset.mem_cons, ← hi] at hj

Goal state after:
case refine_2.mpr.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j = i ∨ j ∈ t
ij : j ≠ i
⊢ v ∈ I j