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

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

Tactic:
IsLocalizedModule.lift_rank_eq R⁰ (IsScalarTower.toAlgHom R S S').toLinearMap le_rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap R K) z)⁻¹ • (algebraMap S L) (a * y) ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
exact (Submodule.span K _).smul_mem _ hy

Goal state after:
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
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
⊢ g.SurjectiveOnStalks

Tactic:
intro I hI
  have := hg I hI
  rw [Localization.localRingHom_comp (I.comap (g.comp f)) (I.comap g) _ _ rfl _ rfl,
    RingHom.coe_comp] at this
  exact this.of_comp

Goal state after:
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
⊢ 1 • 1 ∉ J

Tactic:
by rw [one_smul]; exact J.primeCompl.one_mem

Goal state after:
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 }
⊢ a ≤ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩

Tactic:
(· ≤ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * ((↑a).1 + (↑a).2 * (↑b).1) = (↑a).1
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:
(· ≤ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑b).1 * ((↑a).1 + (↑a).2 * (↑b).1) = (↑b).1
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).1 * ((↑a).1 + (↑a).2) = (↑b).1

Tactic:
a.2.2,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑b).1 * 1 = (↑b).1
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:
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.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ≤ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ ((↑a).1 + (↑a).2 * (↑b).1) * (↑c).1 = (↑a).1 + (↑a).2 * (↑b).1
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 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a

Tactic:
(· ≤ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(aᶜ ⊔ bᶜ)ᶜ).1 * (↑a).1 = (↑(aᶜ ⊔ bᶜ)ᶜ).1
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 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b

Tactic:
(· ≤ ·),

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

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

Tactic:
(· ≤ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑(bᶜ ⊔ cᶜ)ᶜ).1 = (↑a).1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i)) ⊆ Set.range (comap f)

Tactic:
exact Set.iUnion_subset fun _ ↦ Set.range_comp_subset_range _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S) ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
⊢ p ∈ Set.range (comap (algebraMap R S))

case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : p ∈ Set.range (comap (algebraMap R S))
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
⊢ False

Tactic:
have hI : algebraMap _ _ r = _ := congr_fun hr I

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ False
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
⊢ IsEmbedding f ∧ Function.Surjective f ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)

Tactic:
← isEmbedding_iff_restrictPreimage hU h,

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 ∧ Function.Surjective f ↔
    IsEmbedding f ∧ ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
i : ↑Us
hi : i ∈ t
x : X
hx : x ∈ ↑↑i
this : x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ }
⊢ f x ∈ U

Tactic:
exact this

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
by simpa only [left_eq_sup, principal_le_iff] using h

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
⊢ (↑K.toCompacts).Nonempty

Tactic:
exact K.nonempty

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : 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)
⊢ ∃ x, IsGenericPoint x t

Tactic:
use H.genericPoint

Goal state after:
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
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s ∩ t)

Tactic:
obtain ⟨U, hxU, hU, hsU⟩ := hs x

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s ∩ t)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ (s ∪ t))

Tactic:
obtain ⟨U, hxU, hU, hsU⟩ := hs x

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ (s ∪ t))
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 Y
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
x : X
U : Set Y
hxU : U ∈ 𝓝 (f x)
hU : IsOpen[inst✝] U
H : IsConstructible (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝¹] U ∧ IsConstructible (U ↓∩ f ⁻¹' s)

Tactic:
exact ⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
    (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩

Goal state after:
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)
⊢ IsLocallyConstructible s

Tactic:
intro x
  have ⟨i, hi⟩ := hU.exists_mem x
  have ⟨V, hVx, hV, hV'⟩ := H i ⟨x, hi⟩
  refine ⟨_, (U i).2.isOpenEmbedding_subtypeVal.image_mem_nhds.mpr hVx,
      (U i).2.isOpenMap_subtype_val _ hV, ?_⟩
  let e : V ≃ₜ Subtype.val '' V :=
    (Equiv.Set.image _ V Subtype.val_injective).toHomeomorphOfIsInducing
      ((U i).2.isOpenEmbedding_subtypeVal.restrict (by simp [MapsTo]) hV).isInducing
  convert! hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding
  ext ⟨_, x, hx, rfl⟩
  simp [e, Equiv.toHomeomorphOfIsInducing]

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

Goal state before:
pp: R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
algebraize_only [Localization.localRingHom (Ideal.comap f P) P f rfl]

Goal state after:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
⊢ Module.Flat R (Localization.AtPrime P)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0

Tactic:
intro p

Goal state after:
a b p : ℕ
⊢ p ∈ (a.lcm b).factorization.support →
    (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then 1 else i ^ (a.lcm b).factorization i) ≠ 0

Tactic:
intro p

Goal state after:
a b p : ℕ
⊢ p ∈ (a.lcm b).factorization.support →
    (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

Tactic:
intro p

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ a.factorization.support → p ∈ (a.lcm b).factorization.support
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support

Tactic:
intro p

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ b.factorization.support → p ∈ (a.lcm b).factorization.support
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
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Injective (comap (algebraMap R S))

Tactic:
intro p

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
⊢ ∀ ⦃a₂ : PrimeSpectrum S⦄, comap (algebraMap R S) p = comap (algebraMap R S) a₂ → p = a₂
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
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Injective (comap (algebraMap R S))

Tactic:
intro p q h
  replace h := _root_.congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h
  dsimp only [comap] at h
  rw [IsLocalization.map_under M S, IsLocalization.map_under M S] at h
  ext1
  exact h

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

Goal state before:
pp: case pos
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
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

pp: case neg
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
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
· simp [ha, zero_zpow n hn]

Goal state after:
case neg
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
⊢ D (a ^ n) = n • a ^ (n - 1) • D a
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ ↑n ∈ ⊥

Tactic:
rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]

Goal state after:
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ n • a +ᵥ b = b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
isCompact_isOpen_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ t, (zeroLocus ↑t)ᶜ = s) ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
⊢ exponent G ≠ 0

Tactic:
have htpos : 0 < t.prod id := by
      refine Finset.prod_pos fun a ha => ?_
      rw [← Finset.mem_coe, ht] at ha
      obtain ⟨k, rfl⟩ := ha
      exact h k

Goal state after:
case refine_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ exponent G ≠ 0
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
have := not_exists.mp h
    exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ comap f { asIdeal := p', isPrime := hp' } ∈ comap f '' zeroLocus ↑I

Tactic:
exact ⟨_, hp'', rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
⊢ rank H ≤ rank G

Tactic:
by
  classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ normalizer ↑P

Tactic:
simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]; exact Subtype.forall

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ x ∈ centralizer ↑↑(g • P)

Tactic:
rintro - ⟨z, hz, rfl⟩

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
⊢ Unique (Sylow p G)

Tactic:
refine { uniq := fun Q ↦ ?_ }
  obtain ⟨x, h1⟩ := exists_smul_eq G P Q
  obtain ⟨x, h2⟩ := exists_smul_eq G P default
  rw [smul_eq_of_normal] at h1 h2
  rw [← h1, ← h2]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ s₁ = s₂

Tactic:
classical
  apply toList_injective <|
    (List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup _).eq_of_pairwise'
    s₁.toList_sorted.pairwise s₂.toList_sorted.pairwise
  simpa only [Finset.ext_iff, List.mem_toFinset, RelSeries.mem_toList]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
i : ι
is : i ∈ S
⊢ ↑(⨅ i ∈ S, p i) ⊆ ↑(p i)

Tactic:
exact (iInf_le (fun i => ⨅ _ : i ∈ S, p i) i).trans (iInf_le _ is)

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
j : ℕ
m : M
⊢ (monomial i) r • single R j m = single R (i + j) (r • m)

Tactic:
by
  simp only [Module.End.mul_apply, Polynomial.aeval_monomial, Module.End.pow_apply,
    Module.algebraMap_end_apply, smul_def]
  induction i generalizing r j m with
  | zero =>
    rw [Function.iterate_zero, zero_add]
    exact congr(ofCoeff R $(Finsupp.smul_single r j m))
  | succ n hn =>
    rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
    congr 2
    rw [Nat.one_add]
    exact congr(ofCoeff R $(Finsupp.mapDomain_single))

Goal state after: