mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R I.ResidueField) x = 0 ↔ x ∈ I

Tactic:
by
  rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
    IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff]
  exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

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

Goal state before:
pp: case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩

Tactic:
· refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]

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

Goal state before:
pp: case 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, I ≤ x.asIdeal ∧ comap f x = p

Tactic:
refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩

Goal state after:
case refine_2.refine_1
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 : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

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
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p
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
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes → p ∈ Ideal.under R ⁻¹' J.minimalPrimes

pp: case mpr
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
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes

Tactic:
· intro hp
    have := hp.isPrime
    refine ⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.le⟩, ?_⟩
    rintro I hI e
    have hI' : Disjoint (S : Set R) I := Set.disjoint_of_subset_right e
      ((IsLocalization.isPrime_iff_isPrime_disjoint S A _).mp hp.isPrime).2
    refine (Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_
    · exact IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'
    · exact IsLocalization.under_map_of_isPrime_disjoint S A hI.1 hI'

Goal state after:
case mpr
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
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ (∃ i, ∃ (_ : i ∈ Us), x ∈ i) ↔ ∃ u ∈ Us, x ∈ u

Tactic:
exists_prop

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
introv H hU hU'
    obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
    refine ⟨t, Set.Subset.trans ht ?_⟩
    rw [coe_finset_sup, Finset.sup_eq_iSup]
    rfl

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
have : IsEmbedding f' :=
    IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)

Goal state after:
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
⊢ IsEmbedding ((U i).carrier.restrictPreimage f)
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 X
U : Opens X
⊢ (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U) =
    U

Tactic:
apply le_antisymm

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U) ≤
    U

case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ U ≤
    (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.inr.hs
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ IsCompact (⋂₀ a)

Tactic:
apply this (hf.subset (by grind)) ha

Goal state after:
case inr.inr.hs.ho
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t

case inr.inr.hs.hc
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsCompact t

case inr.inr.hs.h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := ⋯
b : Set (Set α) := ⋯
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ a, IsOpen[inst✝¹] t
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (interior (K.toCompacts ×ˢ L.toCompacts).carrier).Nonempty

Tactic:
simp only [Compacts.carrier_eq_coe, Compacts.coe_prod, interior_prod_eq]
        exact K.interior_nonempty.prod L.interior_nonempty

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ IsGenericPoint (↑H.genericPoint) t

Tactic:
apply le_antisymm

Goal state after:
case h.a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ closure {↑H.genericPoint} ⊆ t

case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure {↑H.genericPoint}
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
⊢ Module.FaithfullyFlat R S ↔ Module.FaithfullyFlat R S

Tactic:
congr!

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).toAlgebra = inst✝
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case singleton
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).last.asIdeal
⊢ ∃ L,
    L.length = (RelSeries.singleton {(a, b) | a < b} q).length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) =
          (RelSeries.singleton {(a, b) | a < b} q).toList

Tactic:
use RelSeries.singleton _ ⟨P, inferInstance⟩

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).last.asIdeal
⊢ (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).length =
      (RelSeries.singleton {(a, b) | a < b} q).length ∧
    (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).last = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S))
          (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).toList =
        (RelSeries.singleton {(a, b) | a < b} q).toList
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat

Tactic:
change ((Algebra.TensorProduct.map f (AlgHom.id R D)).restrictScalars R).Flat

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ (AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D))).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), zeroLocus ↑I ⊆ zeroLocus ↑(x ⊓ y) → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
subset_zeroLocus_iff_le_vanishingIdeal,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      x ⊓ y ≤ vanishingIdeal (zeroLocus ↑I) → x ≤ vanishingIdeal (zeroLocus ↑I) ∨ y ≤ vanishingIdeal (zeroLocus ↑I)) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Bijective (comap (Ideal.Quotient.mk I))

Tactic:
refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩
  simpa [← Set.range_eq_univ, range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective,
    zeroLocus_eq_univ_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
x : PrimeSpectrum R
⊢ x ∈ ↑(basicOpen r) ↔ x ∈ (zeroLocus {r})ᶜ

Tactic:
simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
    Set.singleton_subset_iff]

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⟩
    exact isOpen_basicOpen

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ D (a / b) = b⁻¹ • D a

Tactic:
simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]
  rw [← mul_self_mul_inv b⁻¹, inv_inv]
  ring_nf

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ (if h : ∃ n, 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then Nat.find h else 0) =
    if h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find h else 0

Tactic:
congr!

Goal state after:
case h₂
G : Type u
inst✝ : Monoid G
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

case h₁
G : Type u
inst✝ : Monoid G
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ =
    zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
localization_away_comap_range _ (C c)

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (↑(basicOpen (C c)))ᶜ = zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a, ∃ (_ : a ∈ H), zpowers a = H) ↔ ∃ g, zpowers g = H

Tactic:
exists_prop

Goal state after:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ g, zpowers g = H
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
⊢ zpowers a = ⊤

Tactic:
eq_top_iff

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
⊢ ⊤ ≤ zpowers a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ t.succ = 1

Tactic:
← ht,

Goal state after:
case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (exponent G).factorization p = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal

Tactic:
by
  simp_rw [← isMax_iff, StableUnderSpecialization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]
  exact ⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s✝
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
e : (zeroLocus ↑I)ᶜ = s✝
⊢ (zeroLocus ↑s)ᶜ = s✝

Tactic:
by simpa [hs.symm] using e

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

Goal state before:
pp: case refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ ∃ t, n = ↑(↑n).val + ↑(Nat.card α) * t

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ ∃ t, n = ↑(↑n).val + ↑(Fintype.card α) * t
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 ↑(Nat.card α)]
⊢ y = ↑n

Tactic:
Nat.card_eq_fintype_card,

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 [ZMOD ↑(Fintype.card α)]
⊢ y = ↑n
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
⊢ p ∣ orderOf g

Tactic:
by
  have ⟨k, hk⟩ := hG.exists_orderOf_eq_pow g
  rw [hk]
  refine dvd_pow_self _ fun hk0 ↦ hg ?_
  rw [← orderOf_eq_one_iff, hk, hk0, pow_zero]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ p.Coprime (orderOf (t ^ p ^ k))

Tactic:
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)

Goal state after:
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 : ℕ := ⋯
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ ¬p ∣ orderOf (t ^ p ^ k)
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)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h✝ : IsClopen s
e f : R
h : e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
exact ⟨e, f, by simp only [h, and_self]⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = univ.lcm fun x ↦ exponent (M x)

Tactic:
refine dvd_antisymm ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) ∣ univ.lcm fun x ↦ exponent (M x)

case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x ↦ exponent (M x)) ∣ exponent ((i : ι) → M i)
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c.cast • x ∈ K

Tactic:
exact zsmul_mem hx (cast c)

Goal state after: