mathlib-initiative/mathlib-tactics huggingface dataset:
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)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
⊢ ∏ i, e i = 0

Tactic:
ext j

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
j : ι
⊢ (∏ i, e i) j = 0 j
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)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x = x * e i

Tactic:
ext j

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
⊢ x j = (x * e i) j
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ (∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) → x ∈ (mapToFractionRing K S B hS).range

Tactic:
rintro ⟨a, s, hs, rfl⟩

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a ⟨s, ⋯⟩ ∈ (mapToFractionRing K S B hS).range
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
reg : IsSMulRegular M x
p : Ideal R
hp : p ∈ (Module.annihilator R M).minimalPrimes
⊢ x ∉ p

Tactic:
by
  intro hx
  rcases Ideal.exists_mul_mem_of_mem_minimalPrimes hp hx with ⟨y, hy, hxy⟩
  rcases not_forall.mp (Module.mem_annihilator.not.mp hy) with ⟨m, hm⟩
  exact hm (reg.right_eq_zero_of_smul ((smul_smul x y m).trans (Module.mem_annihilator.mp hxy m)))

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.under R p ≤ I

Tactic:
refine (Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_

Goal state after:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ (Ideal.map (algebraMap R A) I).IsPrime

case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
s : Set (Opens β)
⊢ ↑{ carrier := ⇑f ⁻¹' ↑(sSup s), is_open' := ⋯ } = ↑(sSup ((fun s ↦ { carrier := ⇑f ⁻¹' ↑s, is_open' := ⋯ }) '' s))

Tactic:
by simp only [coe_sSup, preimage_iUnion, biUnion_image, coe_mk]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) = ↑z \ (↑x ⊔ ↑w) ⊔ (↑y ⊓ ↑z) \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
_root_.sdiff_eq,

Goal state after:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x ⊓ (↑y)ᶜ)ᶜ ⊓ (↑z ⊓ (↑w)ᶜ) ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ) =
    ↑z ⊓ (↑x ⊔ ↑w)ᶜ ⊔ ↑y ⊓ ↑z ⊓ (↑w)ᶜ ⊔ t.sup fun x ↦ ↑x.1 ⊓ (↑x.2)ᶜ
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔
    ∀ (U V : Set α), IsOpen[inst✝] U → IsCompact U → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
simp [IsQuasiSeparated]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ PrespectralSpace X

Tactic:
refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_
  simp only [Set.mem_iUnion, Set.mem_image, Set.mem_ofPred_eq, forall_exists_index, and_imp,
    forall_comm (α := Set _), forall_apply_eq_imp_iff₂]
  exact fun i V hV hV' ↦ hV'.image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ IsTopologicalBasis {U | IsOpen[inst✝²] U ∧ IsCompact U}

Tactic:
by
    apply isTopologicalBasis_of_isOpen_of_nhds (fun U hU ↦ hU.1) <| fun x U hx hU ↦ ?_
    obtain ⟨V, ⟨hoV, hcV⟩, hfx, hVf⟩ : ∃ V ∈ {V | IsOpen V ∧ IsCompact V}, f x ∈ V ∧ V ⊆ f '' U :=
      (PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩
    refine ⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩
    · exact hf.toIsInducing.isCompact_preimage' hcV <| Set.SurjOn.subset_range hVf
    · exact hf.injective.mem_set_image.mp (hVf hy)

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst✝] U
⊢ IsCompact (f ⁻¹' U)

Tactic:
hfemb.isCompact_iff,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst✝] U
⊢ IsCompact (f '' f ⁻¹' U)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s)

Tactic:
have ⟨V, hVx, hV, hV'⟩ := H i ⟨x, hi⟩

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
⊢ (Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d) = IsScalarTower.toAlgHom R A (B ⧸ I)

pp: case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦
    ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

Tactic:
· ext x; exact liftOfDerivationToSquareZero_mk_apply I hI d x

Goal state after:
case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦
    ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ (fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃+o Additive H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
by ext; simp

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

Goal state before:
pp: a b : ℕ
⊢ (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)

Tactic:
rw [factorizationLCMLeft, factorizationLCMRight]

Goal state after:
a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    ((a.lcm b).factorization.prod fun p n ↦ if b.factorization p ≤ a.factorization p then 1 else p ^ n)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).IsRadical

Tactic:
← vanishingIdeal_closure,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal (closure s)).IsRadical
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : zeroLocus ↑I = zeroLocus ↑J
⊢ I.radical = J.radical

Tactic:
← vanishingIdeal_zeroLocus_eq_radical,

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : zeroLocus ↑I = zeroLocus ↑J
⊢ vanishingIdeal (zeroLocus ↑I) = vanishingIdeal (zeroLocus ↑J)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
this : f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0
⊢ { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    x • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } y +
      y • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } x

Tactic:
simpa [sub_eq_zero, hf _]

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

Goal state before:
pp: case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen u

Tactic:
rintro _ ⟨r, rfl⟩

Goal state after:
case h_open
R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsOpen ((fun r ↦ ↑(basicOpen r)) r)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
⊢ ∃ n, 0 < n ∧ g ^ n = 1

Tactic:
peel 2 h

Goal state after:
case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1
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:
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:
by
    simpa [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul, -basicOpen_eq_zeroLocus_compl]
      using isCompact_basicOpen _

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
⊢ Pi.single i f * x = 0

Tactic:
ext j

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
j : ι
⊢ (Pi.single i f * x) j = 0 j
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ comap (Pi.evalRingHom R i) q = comap (Pi.evalRingHom R i) q

Tactic:
by ext; simp

Goal state after:
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
⊢ exponent G ≤ n % exponent G

Tactic:
apply exponent_min' _ h

Goal state after:
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 % exponent G) = 1
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:
pow_exponent_eq_one,

Goal state after:
G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ 1 = e 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
⊢ False

Tactic:
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
⊢ False
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₁ : M₁
⊢ f (m₁ ^ exponent M₁) = 1

Tactic:
pow_exponent_eq_one,

Goal state after:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
m₁ : M₁
⊢ f 1 = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
h1,

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : Nat.Coprime 0 H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∈ d.properDivisors
⊢ #{a | orderOf a = m} = φ m

Tactic:
simp only [mem_properDivisors] at hm

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ #{a | orderOf a = m} = φ m
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
S : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : FunLike F M M₁
inst✝⁴ : AddMonoidHomClass F M M₁
inst✝³ : Module (ZMod n) M
inst✝² : Module (ZMod n) M₁
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
⊢ toZModLinearMap n (f₁ + f₂) = toZModLinearMap n f₁ + toZModLinearMap n f₂

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ IsMulTorsion (G ⧸ (powMonoidHom n).range)

Tactic:
by
  simp only [IsMulTorsion, isOfFinOrder_iff_pow_eq_one]
  refine fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩
  rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff]
  simp

Goal state after: