mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det.coeff 1 = M.trace

Tactic:
simp only [← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero,
    coeff_derivative, zero_add, Nat.cast_zero, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
r : R
M : Matrix n n R
⊢ (1 + r • M).det = 1 + M.trace * r + eval r (1 + X • M.map ⇑C).det.divX.divX * r ^ 2

Tactic:
simpa [eval_det, ← smul_eq_mul_diagonal] using congr_arg (eval r) (Matrix.det_one_add_X_smul M)

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
i : R
hi : f i = p.coeff k
⊢ f i = (erase n p).coeff k

Tactic:
simp only [hi, hk, erase_ne, Ne, not_false_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
⊢ M.charpoly.coeff i = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
⊢ M.charpoly.natDegree < i
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ M.charmatrix.det.coeff k ∈ I ^ (Fintype.card n - k)

Tactic:
rw [Matrix.det_apply, finsetSum_coeff]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ ∑ b, (Equiv.Perm.sign b • ∏ i, M.charmatrix (b i) i).coeff k ∈ I ^ (Fintype.card n - k)
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ ((X + 1) ^ (m + n)).coeff k = ((X + 1) ^ m * (X + 1) ^ n).coeff k

Tactic:
rw [pow_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (taylor (-r)) ((taylor r) f) = f

Tactic:
taylor_taylor,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (taylor (-r + r)) f = f
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ M.charpolyRev.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
have hcharpolyRev : M.charpolyRev = det (1 + (X : R[X]) • (-M).map C) := by
    simp only [charpolyRev, sub_eq_add_neg]
    congr 2
    rw [Matrix.map_neg C (map_neg C) M, smul_neg]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
⊢ M.charpolyRev.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i f).Splits

Tactic:
by
  induction hf using Submonoid.closure_induction <;> aesop

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).natDegree = p.natDegree

Tactic:
simp [natDegree]

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

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
n : ℕ
hx : IsIntegral R (mk' Sₘ x ⟨(fun x ↦ r ^ x) n, ⋯⟩)
⊢ (algebraMap S Sₘ) x = (algebraMap S Sₘ) (r ^ n) * mk' Sₘ x ⟨(fun x ↦ r ^ x) n, ⋯⟩

Tactic:
exact (mk'_spec'_mk ..).symm

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

Goal state before:
pp: case left.inr.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' }

pp: case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
· exact False.elim (hJ.ne_top h.right)

Goal state after:
case left.inr.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inr { asIdeal := J', isPrime := hJ' }
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ Minimal (fun q ↦ q.IsPrime ∧ ⊥ ≤ q) x.asIdeal

Tactic:
simp only [IsMin, Minimal, x.2, bot_le, and_self, and_true, true_and]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
by
  by_cases h : Function.Injective (algebraMap R S)
  · have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance
  rw [← Polynomial.map_injective_iff] at h
  exact Algebra.isAlgebraic_of_not_injective h

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ ↑R (AlgebraTensorModule.map LinearMap.id f) = 0

Tactic:
show (0 :  S ⊗[R] N →ₗ[R] S ⊗[R] N') = (0 : S ⊗[R] N →ₗ[S] S ⊗[R] N').restrictScalars R by rfl,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ ↑R (AlgebraTensorModule.map LinearMap.id f) = ↑R 0
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂

Tactic:
smul_smul_smul_comm

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ • t₁) • r₂ • t₂ = (r₁ • t₁) • r₂ • t₂
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
by
    simp_rw [(· ≤ ·), mul_add, mul_comm a.1.2, ← mul_assoc,
      (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq, ← mul_add, a.2.2, mul_one]

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p

Tactic:
classical
  cases nonempty_fintype ι
  let e (i) : Π i, R i := Function.update 1 i 0
  have H : ∏ i, e i = 0 := by
    ext j
    rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]
    simp [e]
  obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by
    simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem
  let h₁ : Function.Surjective (Pi.evalRingHom R i) := RingHomSurjective.is_surjective
  have h₂ : RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal := by
    intro x hx
    convert! p.asIdeal.mul_mem_left x hi
    ext j
    by_cases hj : i = j
    · subst hj; simpa [e]
    · simp [e, Function.update_of_ne (.symm hj)]
  have : (p.asIdeal.map (Pi.evalRingHom R i)).comap (Pi.evalRingHom R i) = p.asIdeal := by
    rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
  exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩

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

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }).asIdeal ↔ x ∈ p.asIdeal

Tactic:
comap_asIdeal,

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ Ideal.comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal ↔ x ∈ p.asIdeal
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ ↑(Finset.image f' t), b i ⊆ U

Tactic:
· apply Set.iUnion₂_subset
    rintro i hi
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
    rw [e]
    exact Set.subset_iUnion (b ∘ f') j

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ↑Uᶜ = interior (↑U)ᶜ

Tactic:
by
  rw [← interior_compl, coe_interior]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
isOpenEmbedding_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsEmbedding f ∧ IsOpen[inst✝] (range f) ↔
    ∀ (i : ι),
      IsEmbedding ((U i).carrier.restrictPreimage f) ∧
        IsOpen[instTopologicalSpaceSubtype] (range ((U i).carrier.restrictPreimage f))
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁

Tactic:
obtain ⟨x, hx⟩ := hU₂Z
    use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
induction s using Finset.cons_induction with

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
induction s using Finset.cons_induction with

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : CompactSpace X
hs : IsRetrocompact s
⊢ IsCompact s

Tactic:
by
  simpa using hs CompactSpace.isCompact_univ

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
induction s using Finset.cons_induction with

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S

Tactic:
simp only [FaithfullyFlat]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Module.FaithfullyFlat R S ↔ Module.FaithfullyFlat R S
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

Tactic:
by
  rw [← prod_factorization_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
    factorizationLCMRight, ← prod_mul]
  congr; ext p n; split_ifs <;> simp

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b

Tactic:
← prod_factorization_pow_eq_self hb

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S

Tactic:
refine ((primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ?_).symm
  refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing
  · rw [continuous_sum_dom]
    simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨continuous_comap _, continuous_comap _⟩
  · simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
⊢ IsLocalization.AtPrime (Localization.Away f) p.asIdeal

Tactic:
by
    refine .of_le_of_exists_dvd (.powers f) _
      (Submonoid.powers_le.mpr <| by apply h ▸ Set.mem_singleton p) fun r hr ↦ ?_
    contrapose! hr
    simp_rw [← Ideal.mem_span_singleton] at hr
    have ⟨q, prime, le, disj⟩ := Ideal.exists_le_prime_disjoint (Ideal.span {r})
      (.powers f) (Set.disjoint_right.mpr hr)
    have : ⟨q, prime⟩ ∈ (basicOpen f).1 := Set.disjoint_right.mp disj (Submonoid.mem_powers f)
    rw [h, Set.mem_singleton_iff] at this
    rw [← this]
    exact not_not.mpr (q.span_singleton_le_iff_mem.mp le)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
i j : R
⊢ IsCompact (↑(basicOpen i) ∩ ↑(basicOpen j))

Tactic:
simpa [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul, -basicOpen_eq_zeroLocus_compl]
      using isCompact_basicOpen _

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = 1 ↔ Subsingleton G

Tactic:
refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩

Goal state after:
case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a = b

case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1

case ge
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 1 ≤ exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1

Tactic:
exact hG

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ IsClosed (comap f '' comap f ⁻¹' s)

Tactic:
apply isClosed_image_of_stableUnderSpecialization _ _ hsc

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ StableUnderSpecialization (comap f '' comap f ⁻¹' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ DenseRange (comap f) → ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
intro H I hI
    have : I ∈ (RingHom.ker f).minimalPrimes := by
      rw [denseRange_comap_iff_ker_le_nilRadical] at H
      simp only [Set.mem_ofPred, Ideal.IsMinimalPrime] at hI ⊢
      convert! hI using 2 with p
      exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩
    obtain ⟨p, hp, _, rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) I this
    exact ⟨⟨p, hp⟩, rfl⟩

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑n]

Tactic:
← ZMod.intCast_eq_intCast_iff

Goal state after:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ↑⋯.choose = ↑k
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : n ≡ ↑y.val [ZMOD ↑(Fintype.card α)]
⊢ y = ↑n

Tactic:
← ZMod.intCast_eq_intCast_iff

Goal state after:
case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : ↑n = ↑↑y.val
⊢ y = ↑n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G

Tactic:
by
  have := center_nontrivial hG
  exact
      bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ ↑(basicOpen x) ⊆ s

Tactic:
· rw [basicOpen_eq_zeroLocus_compl, Set.compl_subset_comm, ← hI']
      exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr <| Ideal.pow_le_self hnz hx)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p ↥ϕ.ker
h : ↑P ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup p ↥Q
hle : comap ϕ ↑P ≤ Q
⊢ Q = comap ϕ ↑P

Tactic:
show Q = P.1.comap ϕ
      rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
      exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm

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

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
⊢ IsMulCommutative G

Tactic:
refine ⟨⟨fun a b ↦ ?_⟩⟩
  let ⟨⟨x, y, (hxy : f y = x)⟩, (hx : ∀ a : f.range, a ∈ zpowers _)⟩ :=
    IsCyclic.exists_generator (α := f.range)
  let ⟨m, hm⟩ := hx ⟨f a, a, rfl⟩
  let ⟨n, hn⟩ := hx ⟨f b, b, rfl⟩
  have hm : x ^ m = f a := by simpa [Subtype.ext_iff] using hm
  have hn : x ^ n = f b := by simpa [Subtype.ext_iff] using hn
  have ha : y ^ (-m) * a ∈ center G :=
    hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel])
  have hb : y ^ (-n) * b ∈ center G :=
    hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel])
  calc
    a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) := by simp [mul_assoc]
    _ = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) := by rw [mem_center_iff.1 ha]
    _ = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) := by simp [mul_assoc]
    _ = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) := by rw [mem_center_iff.1 hb]
    _ = b * a := by group

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

Goal state before:
pp: G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ IsCyclic G ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
← isAddCyclic_additive_iff,

Goal state after:
G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ IsAddCyclic (Additive G) ↔ Nonempty (G ≃*o Multiplicative ℤ)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Finite N
ZN : Type := ZMod (Nat.card N)
this : IsAddCyclic (ZMod (Nat.card N) × ZN)
⊢ False

Tactic:
exact Finite.one_lt_card (α := N).ne' (by simpa [ZN] using coprime_card_of_isAddCyclic_prod ZN ZN)

Goal state after: