mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
⊢ IsBaseChange S (Finsupp.mapRange.linearMap ε)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (Algebra.TensorProduct.comm R (ResidueField R) S).trans
    (AlgEquiv.restrictScalars R (quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm)
⊢ Nontrivial (ResidueField R ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
⊢ ∃ r ∉ p, ∃ s, r • x = s ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : p.Fiber S
r : R
hr : r ∉ p
s : S
e : r • (Algebra.TensorProduct.comm R p.ResidueField S) x = s ⊗ₜ[R] 1
⊢ r • x = 1 ⊗ₜ[R] s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : p.Fiber S
⊢ ∃ r ∉ p, ∃ s, r • x = 1 ⊗ₜ[R] s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization p.primeCompl)) =
    map (↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv)
      (map includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p)))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ ∀ (r : S),
    ((map includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p))).quotientEquiv
            (map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
              (IsLocalRing.maximalIdeal (Localization p.primeCompl)))
            (Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv ⋯).toFun
        ((algebraMap S
            (S ⊗[R] Localization.AtPrime p ⧸ map includeRight (IsLocalRing.maximalIdeal (Localization.AtPrime p))))
          r) =
      (algebraMap S
          (Localization (algebraMapSubmonoid S p.primeCompl) ⧸
            map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
              (IsLocalRing.maximalIdeal (Localization p.primeCompl))))
        r

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ p ∈ freeLocus R M ↔ Free Rₚ Mₚ

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ p ∈ freeLocus R M ↔ Free Rₚ Mₚ

Tactic:
by
  set e := (IsLocalization.algEquiv p.asIdeal.primeCompl
      (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
  apply Module.Free.iff_of_equiv (σ := e)
  refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }
  intro r x
  obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl r
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1
  simp [e, ← map_smul, ← smul_assoc]

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
inst✝² : CommRing Rₚ
inst✝¹ : Algebra R Rₚ
inst✝ : IsLocalization.AtPrime Rₚ p.asIdeal
⊢ p ∈ freeLocus R M ↔ Free Rₚ (Rₚ ⊗[R] M)

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ freeLocus R M = freeLocus R M'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
this : Algebra S (p.Fiber S) := rightAlgebra
⊢ map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization p.primeCompl)) =
    map (algebraMap S (Localization (algebraMapSubmonoid S p.primeCompl))) (map (algebraMap R S) p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : p.IsPrime
q : Ideal (p.Fiber S)
inst✝ : q.IsPrime
this✝¹ : Algebra S (p.Fiber S) := rightAlgebra
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
pS : Ideal S := map (algebraMap R S) p
SpS : Type u_2 := S ⧸ pS
r : Ideal S := comap includeRight q
Sr : Type u_2 := Localization.AtPrime r
e₁ : p.Fiber S ≃ₐ[S] Sp ⧸ map (algebraMap S Sp) pS := algEquivAux₁ p
q' : Ideal (Sp ⧸ map (algebraMap S Sp) pS) := comap e₁.symm q
this✝ : (under SpS q').LiesOver r
this : algebraMapSubmonoid SpS r.primeCompl = (under SpS q').primeCompl
⊢ IsLocalization (algebraMapSubmonoid SpS r.primeCompl) (Localization.AtPrime q')

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ comap includeRight.toRingHom q ∈ comap (algebraMap R S) ⁻¹' {p}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
x y : M × N
x✝ : Fin n → M × N
⊢ ((bN.det.compLinearMap (LinearMap.snd R M N)).smulRight (x + y).1) x✝ =
    ((bN.det.compLinearMap (LinearMap.snd R M N)).smulRight x.1 +
        (bN.det.compLinearMap (LinearMap.snd R M N)).smulRight y.1)
      x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
c : R
x : M × N
x✝ : Fin n → M × N
⊢ ((bN.det.compLinearMap (LinearMap.snd R M N)).smulRight (c • x).1) x✝ =
    ((RingHom.id R) c • (bN.det.compLinearMap (LinearMap.snd R M N)).smulRight x.1) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
m : M
⊢ (cofactorToLeft bN) ((ιMulti R (n + 1)) (Fin.cons (m, 0) fun i ↦ (0, bN i))) = m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩)
      ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        q) =
    q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := ⋯.some
⊢ rankAtStalk M 𝔭 = 1

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom (comap (algebraMap R A) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
⊢ algebraMap R Aₚ = (algebraMap Rₚ Aₚ).comp (algebraMap R Rₚ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
⊢ finrank R (M × N) = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
⊢ finrank R ↥(⋀[R]^(n + 1) (M × N)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
e : R ≃ₗ[R] ↥(⋀[R]^(n + 1) (M × N)) := ⋯.some
bN : Basis (Fin n) R N := finBasis R N
f : R →ₗ[R] M := exteriorPower.cofactorToLeft bN ∘ₗ ↑e
x : M
⊢ f (e.symm ((exteriorPower.ιMulti R (n + 1)) (Fin.cons (x, 0) fun i ↦ (0, bN i)))) = x

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ comap (algebraMap R A) ⁻¹' freeLocus R M ⊆ freeLocus A (A ⊗[R] M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
⊢ Free R M

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Algebra.lmul A B) ((Polynomial.aeval x) f) = 0
⊢ (Algebra.lmul A B) ((Polynomial.aeval x) f) = (Algebra.lmul A B) 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
⊢ (minpoly A x).natDegree ≤ ⊤.spanFinrank

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : Module.Finite A B
x : B
inst✝ : Module.Free A B
⊢ (minpoly A x).natDegree ≤ Module.finrank A B

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : α
⊢ (e.viaEmbedding ι) (ι x) = ι (e x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : β
hx : ¬x ∈ Set.range ⇑ι
⊢ (e.viaEmbedding ι) x = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : α ↪ β
⊢ Function.Injective ⇑(viaEmbeddingHom ι)

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝¹ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
x : R
s : ↥S
hx : IsLocalization.mk' (Localization S) x s ∈ p.asIdeal.primeCompl
⊢ (algebraMap R (Localization S)) x =
    (algebraMap R (Localization S)) ↑s * ↑⟨IsLocalization.mk' (Localization S) x s, hx⟩

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this : IsScalarTower R (Localization S) Rₚ
⊢ IsLocalization.AtPrime Rₚ p.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (fun q ↦
        {
          asIdeal :=
            RingHom.ker
              (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                  (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
          isPrime := ⋯ })
      ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q) =
    q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ (derivedSeries G n).Normal

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ (derivedSeries G n).Characteristic

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Subsingleton G
⊢ ⊤ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
⊢ IsSolvable G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : IsSolvable ↥H ∧ IsSolvable (G ⧸ H)
left✝ : IsSolvable ↥H
right✝ : IsSolvable (G ⧸ H)
⊢ (QuotientGroup.mk' H).ker ≤ H.subtype.range

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G < ⊤

Tactic:
by
  rw [lt_top_iff_ne_top]
  obtain ⟨n, hn⟩ := hG
  contrapose! hn
  refine ne_of_eq_of_ne ?_ top_ne_bot
  induction n with
  | zero => exact derivedSeries_zero G
  | succ n h => rwa [derivedSeries_succ, h]

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁶ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
x : R
s : ↥S
hx : IsLocalization.mk' (Localization S) x s ∈ p.asIdeal.primeCompl
⊢ (algebraMap R (Localization S)) x =
    (algebraMap R (Localization S)) ↑s * ↑⟨IsLocalization.mk' (Localization S) x s, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ ⁅H, H⁆ < H

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
hx : 1 ⊗ₜ[R] s ∈ ((preimageEquivFiber R S p) q₁).asIdeal
e : r • x = 1 ⊗ₜ[R] s
⊢ s ∈ (↑q₁).asIdeal

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁴ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝³ : IsScalarTower R (Localization S) Rₚ
this✝² : IsLocalization.AtPrime Rₚ p.asIdeal
this✝¹ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝ : IsScalarTower R (Localization S) Mₚ
this : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
⊢ IsLocalizedModule p.asIdeal.primeCompl l

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
⊢ freeLocus (Localization S) (LocalizedModule S M) = comap (algebraMap R (Localization S)) ⁻¹' freeLocus R M

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ freeLocus R M = Set.univ ↔ Projective R M

Tactic:
by

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ freeLocus R M = Set.univ ↔ Projective R M

Tactic:
by
  simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]
  exact ⟨fun H ↦ Module.projective_of_localization_maximal fun I hI ↦
    have := H ⟨I, hI.isPrime⟩; .of_free, fun H x ↦ Module.free_of_flat_of_isLocalRing⟩

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
⊢ freeLocus R M = Set.univ

Tactic:
by

Goal state after: