mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support then r i * x i else 0) = (r • { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } x) i

Tactic:
refine dite_eq_left_iff.mpr fun h ↦ ?_

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support
⊢ 0 = r i * x i
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 : α), le a c → le b c → le (sup a b) c

Tactic:
intro _ _ _ hac 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 : α), le a b → le a c → le a (inf b c)

Tactic:
intro _ _ _ hac 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.Topology.Sets.OpenCover

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
⊢ IsPreirreducible s

Tactic:
by
  rcases s.eq_empty_or_nonempty with he | hne
  · rw [he]; exact isPreirreducible_empty
  · choose x hx using hne
    choose i hi using mem_iUnion.mp <| hsU hx
    rcases exists_mem_irreducibleComponents_subset_of_isIrreducible (U i).carrier ⟨⟨x, hi⟩, h i⟩
      with ⟨u, hu, hUu⟩
    by_cases huniv : s ⊆ u
    · exact hu.1.2.open_subset hs huniv
    · have huo : IsOpen uᶜ :=
        IsClosed.isOpen_compl (self := isClosed_of_mem_irreducibleComponents u hu)
      rcases not_subset.mp huniv with ⟨a, ⟨ha₁, ha₂⟩⟩
      choose j haj using mem_iUnion.mp <| hsU ha₁
      have hji : j ≠ i := fun hji' ↦ ha₂ <| hUu <| hji' ▸ haj
      rcases inter_nonempty_iff_exists_left.mp
        ((h j) (U i) uᶜ (U i).isOpen huo
        (not_disjoint_iff_nonempty_inter.mp (by simpa using hn hji)) ⟨a, ⟨haj, ha₂⟩⟩).right
        with ⟨x, hx₁, hx₂⟩
      exfalso; exact hx₂ <| hUu hx₁

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ i, f i)

Tactic:
simp_rw [noetherianSpace_set_iff] at hf ⊢

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
⊢ ∀ t ⊆ ⋃ i, f i, IsCompact t
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
⊢ IsOpen[inst✝] U → IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
⊢ IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
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)
⊢ IsEmbedding f

Tactic:
by
  wlog hU' : iSup U = ⊤
  · let f₀ : X → Set.range f := fun x ↦ ⟨f x, ⟨x, rfl⟩⟩
    suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
    have hU'' : (⨆ i, (U i).comap ⟨Subtype.val, continuous_subtype_val⟩ :
        Opens (Set.range f)) = ⊤ := by
      rw [← top_le_iff]
      simpa [Set.range_subset_iff, SetLike.le_def] using hU
    refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
    · fun_prop
    · rw [hU'']; simp
    · exact hV
    · exact fun i ↦ IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (hV' i)
  rw [(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h]
  intro i
  let f' := (Subtype.val ∘ (f ⁻¹' U i).restrictPreimage (iV i))
  have : IsEmbedding f' :=
    IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)
  have hf' : Set.range f' = f ⁻¹' U i := by
    simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i
  let e := this.toHomeomorph.trans (Homeomorph.setCongr hf')
  refine IsEmbedding.of_comp (by fun_prop) continuous_subtype_val ?_
  convert! ((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding
  ext x
  obtain ⟨x, rfl⟩ := e.surjective x
  simp
  rfl

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
⊢ IsOpen[inst✝] U → IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU'

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝] U
⊢ IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
⊢ IsOpen[inst✝¹] U → IsCompact U → V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
⊢ IsCompact U → V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : 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 α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
h : ∃ x, ∃ (_ : x ∈ s), ¬IsOpen[inst✝¹] x
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
obtain ⟨t, ht, hno⟩ := h

Goal state after:
case inr
α : 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 α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
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 ×ˢ interior ↑L.toCompacts).Nonempty

Tactic:
exact K.interior_nonempty.prod L.interior_nonempty

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
⊢ ∀ {a b : TopologicalSpace.IrreducibleCloseds α},
    { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
rintro ⟨s, hs, hs'⟩ ⟨t, ht, ht'⟩
    refine specializes_iff_closure_subset.trans ?_
    simp
    rfl

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ QuasiSober ↑(W ∩ V)

Tactic:
refine QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' (W ∩ V))
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case a
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ ⋃ i ∈ ↑σ, U i ∩ s ⊆ s

Tactic:
exact Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp }
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : PrimeSpectrum.comap (algebraMap R S) P = { asIdeal := p, isPrime := hp }
⊢ p = Ideal.under R P.asIdeal
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))

Tactic:
have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
    rw [RingHom.algebraMap_toAlgebra]
    exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this✝ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this : IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
⊢ Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
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:
rintro ⟨f, hf⟩; ext x; exact sub_add_cancel (f x) (algebraMap A B x)

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

Goal state before:
pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ p ≠ q

Tactic:
contrapose h'

Goal state after:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ CompactSpace (PrimeSpectrum R)

Tactic:
refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
  choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
  simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
  exact CompleteLattice.IsCompactElement.exists_finset_of_le_iSup _
    Ideal.isCompactElement_top _ S_empty

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

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : (Algebra.TensorProduct.lmul' R).Flat
⊢ (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).Flat

Tactic:
by
  rw [← CommRingCat.flat_ofHom_iff] at h ⊢
  apply MorphismProperty.of_isPushout _ h
  · exact CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T)
      (IsScalarTower.toAlgHom R S A)).toRingHom
  · exact CommRingCat.ofHom
      (RingHom.comp (Algebra.TensorProduct.includeLeft (S := R)).toRingHom (algebraMap S T))
  · refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_
    · exact (CommRingCat.isPushout_tensorProduct R S S).isoPushout.symm
    · exact pushout.congrHom (by simp [IsScalarTower.algebraMap_eq R S T])
          (by simp [IsScalarTower.algebraMap_eq R S A]) ≪≫
        (CommRingCat.isPushout_tensorProduct R T A).isoPushout.symm
    · exact (CommRingCat.isPushout_tensorProduct S T A).isoPushout.symm
    all_goals ext <;> simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
⊢ (↑e.symm).compDer ((↑e).compDer.toFun D) = D

Tactic:
ext a; exact e.symm_apply_apply (D a)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen (f ^ n)) = ↑(basicOpen f)

Tactic:
by simpa using zeroLocus_singleton_pow f n hn

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

Goal state before:
pp: case neg.inr
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 : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -((a ^ n.natAbs) ^ 2)⁻¹ • n.natAbs • a ^ (n.natAbs - 1) • D a = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a

Tactic:
← pow_mul,

Goal state after:
case neg.inr
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 : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -(a ^ (n.natAbs * 2))⁻¹ • n.natAbs • a ^ (n.natAbs - 1) • D a = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
⊢ (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
by
  let := (mapRingHom (algebraMap R (Away c))).toAlgebra
  have := Polynomial.isLocalization (.powers c) (Away c)
  rw [Submonoid.map_powers] at this
  have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) :=
    Polynomial.map_surjective _ Ideal.Quotient.mk_surjective
  rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]
  simp [Polynomial.ker_mapRingHom, Ideal.map_span]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ Submonoid.powers g

Tactic:
rw [mem_powers_iff_mem_zpowers]

Goal state after:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ zpowers g
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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
key : ¬exponent G ∣ exponent G / p
⊢ ∃ g, g ^ (exponent G / p) ≠ 1

Tactic:
by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key

Goal state after:
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 ^ (exponent G).factorization p = 1

Tactic:
← pow_mul,

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.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
h : ¬(k % ↑(Nat.find hex)).natAbs = 0
⊢ k % ↑(Nat.find hex) < ↑(Nat.find hex)

Tactic:
exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1)

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

Goal state before:
pp: case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ (m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
← pow_mul,

Goal state after:
case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ g ^ (Fintype.card α / n.gcd (Fintype.card α) * (m / (Fintype.card α / n.gcd (Fintype.card α)))) = x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

Tactic:
by
      let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
      have hm0 : 0 < m :=
        Nat.pos_of_ne_zero fun hm0 => by
          rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
          exact hm.elim' 1
      simp only [Set.toFinset_card, SetLike.coe_sort_coe]
      rw [Fintype.card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg,
        Nat.card_eq_fintype_card]
      nth_rw 2 [hm]; nth_rw 3 [hm]
      rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm,
        Nat.mul_div_cancel _ hm0]
      exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one,

Goal state after:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ Finset.univ.lcm orderOf
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
g : G
⊢ g ^ p ^ n = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one,

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
g : G
⊢ orderOf g ∣ p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : (↑g ^ p ^ j) ^ p ^ k = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
← pow_mul,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ (p ^ j * p ^ k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑(Ideal.span ↑s))ᶜ

Tactic:
zeroLocus_span

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑s)ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑I)

Tactic:
rintro x (hx : I.comap f ≤ x.asIdeal)
    obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx
    obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁
    let p'' : PrimeSpectrum S := ⟨p', hp'⟩
    apply isClosed_closure.stableUnderSpecialization ((le_iff_specializes
      (comap f ⟨p', hp'⟩) x).mp hq₂) (subset_closure (by exact ⟨_, hp'', rfl⟩))

Goal state after: