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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
⊢ p ∈ support R M ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)

Tactic:
rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Skeleton

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
e : C ≌ D
inst✝ : F.Monoidal
hC : Skeletal C
hD : Skeletal D
x✝¹ : Monoid C := monoidOfSkeletalMonoidal hC
x✝ : Monoid D := monoidOfSkeletalMonoidal hD
⊢ C →* D

Tactic:
exact
  { toFun := F.obj
    map_one' := hD ⟨(Monoidal.εIso F).symm⟩
    map_mul' X Y := hD ⟨(Monoidal.μIso F X Y).symm⟩ }

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (liftAux φ) (r • tprodCoeff R z f) = r • (liftAux φ) (tprodCoeff R z f)

Tactic:
smul_tprodCoeff' r z f,

Goal state after:
case refine_1
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (liftAux φ) (tprodCoeff R (r • z) f) = r • (liftAux φ) (tprodCoeff R z f)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ (toPrincipalIdeal R K) x = I ↔ spanSingleton R⁰ ↑x = ↑I

Tactic:
by
  simp only [toPrincipalIdeal]; exact Units.ext_iff

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case succ
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
n : ℕ
ih : ∀ (h : n < s.length + 1), motive ↥(s.toFun ⟨n, h⟩)
h : n + 1 < s.length + 1
⊢ motive ↥(s.toFun ⟨n + 1, h⟩)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
I : Ideal A
inst✝ : FaithfulSMul A ↥I
this : ↑I ∩ ↑(nonZeroDivisors A) = ∅
⊢ False

Tactic:
exact (bot_lt_annihilator_of_disjoint_nonZeroDivisors
    (Set.disjoint_iff_inter_eq_empty.mpr this)).ne' <| by rwa [Module.annihilator_eq_bot]

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

Goal state before:
pp: case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ (ringEquivOfRingEquiv K L f).symm (spanSingleton S⁰ ↑u) = (↑(ringEquivOfRingEquiv K L f)).symm ↑I

Tactic:
hu

Goal state after:
case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ (ringEquivOfRingEquiv K L f).symm ↑I = (↑(ringEquivOfRingEquiv K L f)).symm ↑I
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g ↦ const X (g y)

Tactic:
ext; simp [h]

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:
simpa using congr((Algebra.TensorProduct.comm _ _ _).symm $e)

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

Goal state before:
pp: case inr
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)
⊢ Free R M

Tactic:
let n := Module.finrank R N

Goal state after:
case inr
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
⊢ Free R M
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : (derivedSeries G n).Normal
⊢ (derivedSeries G (n + 1)).Normal

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.GroupTheory.Solvable

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

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.GroupTheory.Solvable

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

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))

Tactic:
| succ n ih =>

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 : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
x : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageOrderIsoFiber R S p).toFun ((H.toHomeomorphOfSurjective ⋯) x) =
    (H.toHomeomorphOfSurjective ⋯).symm ((H.toHomeomorphOfSurjective ⋯) x)

Tactic:
simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]

Goal state after:
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 : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
x : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageOrderIsoFiber R S p) ((H.toHomeomorphOfSurjective ⋯) x) = x
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ derivedSeries G (n + 1).succ = _root_.commutator G

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ x ∈ derivedSeries (Perm (Fin 5)) (n + 1)

Tactic:
rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ x ∈ derivedSeries (Perm (Fin 5)) (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case intro
R : Type uR
inst✝⁵ : CommRing R
ι : Type u_1
inst✝⁴ : Finite ι
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Flat R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
p : PrimeSpectrum R
val✝ : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearMap.pi fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
this : ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk (M i) p

Tactic:
rankAtStalk,

Goal state after:
case intro
R : Type uR
inst✝⁵ : CommRing R
ι : Type u_1
inst✝⁴ : Finite ι
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Flat R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
p : PrimeSpectrum R
val✝ : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearMap.pi fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
this : ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
⊢ finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i)) =
    ∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (M i))
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
e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal] Localization.AtPrime p.asIdeal ⊗[R] M :=
  equivTensorProduct p.asIdeal.primeCompl M
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
rankAtStalk,

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal] Localization.AtPrime p.asIdeal ⊗[R] M :=
  equivTensorProduct p.asIdeal.primeCompl M
⊢ finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) =
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
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✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
this : Algebra (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal) :=
  AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
e : LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M :=
  equivTensorProduct p.asIdeal.primeCompl (S ⊗[R] M) ≪≫ₗ
        AlgebraTensorModule.cancelBaseChange R S (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl)
          M ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization p.asIdeal.primeCompl) M).symm ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl))
      (equivTensorProduct q.asIdeal.primeCompl M).symm
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
rankAtStalk,

Goal state after:
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
this : Algebra (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal) :=
  AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
e : LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M :=
  equivTensorProduct p.asIdeal.primeCompl (S ⊗[R] M) ≪≫ₗ
        AlgebraTensorModule.cancelBaseChange R S (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl)
          M ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization p.asIdeal.primeCompl) M).symm ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl))
      (equivTensorProduct q.asIdeal.primeCompl M).symm
⊢ finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M)) =
    rankAtStalk M (comap (algebraMap R S) p)
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✝³ : Flat R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
K : Type uR := FractionRing R
Rp : Type uR := Localization.AtPrime p
Mp : Type (max uR uM) := LocalizedModule.AtPrime p M
⊢ rankAtStalk M { asIdeal := p, isPrime := inst✝ } = finrank R M

Tactic:
rankAtStalk,

Goal state after:
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
K : Type uR := FractionRing R
Rp : Type uR := Localization.AtPrime p
Mp : Type (max uR uM) := LocalizedModule.AtPrime p M
⊢ finrank (Localization.AtPrime { asIdeal := p, isPrime := inst✝ }.asIdeal)
      (LocalizedModule { asIdeal := p, isPrime := inst✝ }.asIdeal.primeCompl M) =
    finrank R M
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝ : Free R M
a✝ : Nontrivial R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M →₀ R
this : Fintype.card (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
⊢ Fintype.card (Free.ChooseBasisIndex R M) = 1

Tactic:
by simpa using this

Goal state after:
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
hE : E ≤ ⨆ i, t i
this✝ : (Polynomial.map (algebraMap F ↥E) (minpoly F x)).Splits
this : (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits

Tactic:
Polynomial.map_map

Goal state after:
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
hE : E ≤ ⨆ i, t i
this✝ : (Polynomial.map (algebraMap F ↥E) (minpoly F x)).Splits
this : (Polynomial.map ((inclusion hE).comp (algebraMap F ↥E)) (minpoly F x)).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (Units.map ↑(spanSingleton R)).range
⊢ I ∈ (unitsToPic R A).ker

Tactic:
obtain ⟨x, rfl⟩ := h

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
⊢ (Units.map ↑(spanSingleton R)) x ∈ (unitsToPic R A).ker
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f =
    Polynomial.map (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α))

Tactic:
Polynomial.map_map

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f = Polynomial.map ((algebraMap (↥K) E).comp (algebraMap F ↥K)) (minpoly F α)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α) ∣ Polynomial.map (algebraMap F E) f

Tactic:
by
      convert! Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
      rw [Polynomial.map_map]; rfl

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ (unitsToPic R A).range = relPic R A

Tactic:
ext M

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
⊢ M ∈ (unitsToPic R A).range ↔ M ∈ relPic R A
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ⊆ B'

Tactic:
← union_sdiff_cancel hJX,

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ (J ∪ X \ J) ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M = freeOn M.E

Tactic:
simp [eq_freeOn_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
⊢ I.encard < B.encard

Tactic:
refine lt_of_not_ge fun hle ↦ ?_

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
⊢ False