mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul.tmul
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
x✝ y✝ : P.Ring
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝))

Tactic:
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply,
        map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
        Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Exact ⇑h1Cotangentι ⇑P.cotangentComplex

Tactic:
rw [LinearMap.exact_iff]
  exact (Submodule.range_subtype _).symm

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
x : P.toExtension.Ring
i : ι
⊢ (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (D R P.toExtension.Ring) x)) i = (aeval P.val) ((pderiv i) x)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
⊢ Injective ⇑(rTensor N M'.subtype)

Tactic:
apply (injective_iff_map_eq_zero _).mpr
  rintro x hx
  obtain ⟨s, rfl⟩ := exists_finset x
  rw [← Finset.sum_attach]
  apply sum_tmul_eq_zero_of_vanishesTrivially
  simp only [map_sum, rTensor_tmul, coe_subtype] at hx
  have e := (Fintype.equivFin s).symm
  rw [← Finset.sum_coe_sort, ← e.sum_comp] at hx
  have := hMN hx
  rw [← e.vanishesTrivially_comp]
  unfold VanishesTrivially at this ⊢
  convert! this
  symm
  convert! (injective_iff_map_eq_zero' _).mp (injective_subtype M') _
  simp

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal) →
    Submodule.span R s ≤ (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M).ker

Tactic:
Submodule.span_le,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal) → s ⊆ ↑(LocalizedModule.mkLinearMap p.asIdeal.primeCompl M).ker
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

Tactic:
clear hx hss' s

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
x : N
s' : Finset N
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨s, hs, e₁⟩ := H₁ m'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : Flat R M
K : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
x✝ : K
⊢ ((x ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ f) x✝ = 0 x✝

Tactic:
simpa [comp_assoc] using congr($h _)

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
⊢ Even k

Tactic:
rcases k.val.even_or_odd with hk | hk

Goal state after:
case inl
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even ↑k
⊢ Even k

case inr
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd ↑k
⊢ Even k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
⊢ Odd k

Tactic:
rcases k.val.even_or_odd with hk | hk

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Even ↑k
⊢ Odd k

case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ((fun φ' ↦ φ'.compMultilinearMap (tprod R))
        ((fun φ ↦
            let __src := liftAux φ;
            { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
          φ))
      x✝ =
    φ x✝

Tactic:
simp [liftAux_tprod, LinearMap.compMultilinearMap]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : (a * b) • y ∈ ⊥
ha : a • y ∉ ⊥
H₁ : ⊥.colon {y} ≤ ⊥.colon {a • y}
⊢ a • b • y ∈ ⊥

Tactic:
smul_smul

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : (a * b) • y ∈ ⊥
ha : a • y ∉ ⊥
H₁ : ⊥.colon {y} ≤ ⊥.colon {a • y}
⊢ (a * b) • y ∈ ⊥
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
⊢ p ∈ associatedPrimes R M''

Tactic:
refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩

Goal state after:
case neg.refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
hb : b ∈ p
⊢ b ∈ (⊥.colon {g x}).radical

case neg.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n ∈ ⊥.colon {g x}
⊢ b ∈ p
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
⊢ ↑{ val := spanSingleton R⁰ ↑1, inv := spanSingleton R⁰ (↑1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = ↑1

Tactic:
simp only [spanSingleton_one, Units.val_one]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
      ⟨i, _hi, rfl⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x * i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI : Submodule.IsPrincipal (I ^ n)
hI0 : ¬I = 0
⊢ Submodule.IsPrincipal I

Tactic:
rw [← ClassGroup.mk0_eq_one_iff (pow_mem (mem_nonZeroDivisors_of_ne_zero hI0) n)] at hI

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ Submodule.IsPrincipal I
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
by
  rw [← preimage_image_eq s inj, preimage_preimage]
  exact h (g '' s)

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

pp: case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
· rw [h, commutator_bot_left]

Goal state after:
case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ Function.Bijective ⇑(curry ↑e)

Tactic:
have : curry e.toLinearMap = ((TensorProduct.lid R N).congrLeft _ R ≪≫ₗ e.congrRight) ∘ₗ
      rTensorHom N ∘ₗ (ringLmapEquivSelf R R M).symm.toLinearMap := by
    rw [← LinearEquiv.toLinearMap_symm_comp_eq]; ext
    simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]
  simpa [this] using! (rTensorEquiv R M <| TensorProduct.comm R N M ≪≫ₗ e).bijective

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N = ↑((LinearEquiv.rTensor N (linearEquivDual e)).symm ≪≫ₗ e)

Tactic:
rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)) = ↑e
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ rankAtStalk R = 1

Tactic:
by
  simp

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
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:
rw [rankAtStalk, e.finrank_eq]

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✝³ : 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:
rw [rankAtStalk, e.finrank_eq]

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)
      (Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl 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
p q : PrimeSpectrum R
hpq : p ≤ q
S : Type uR := Localization.AtPrime q.asIdeal
⊢ p ∈ Set.range (comap (algebraMap R S))

Tactic:
rw [PrimeSpectrum.localization_comap_range S q.asIdeal.primeCompl]

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
p q : PrimeSpectrum R
hpq : p ≤ q
S : Type uR := Localization.AtPrime q.asIdeal
⊢ p ∈ {p | Disjoint ↑q.asIdeal.primeCompl ↑p.asIdeal}
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
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
⊢ rankAtStalk (M ⊗[R] N) = rankAtStalk M * rankAtStalk N

Tactic:
by
  ext p
  let e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
      (Localization.AtPrime p.asIdeal ⊗[R] M) ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N) :=
    (AlgebraTensorModule.assoc _ _ _ _ _ _).symm ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm
  rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]

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
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ Submodule.span F (Set.range ⇑s) ≤ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K))

Tactic:
Submodule.span_le,

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ Set.range ⇑s ⊆ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)))
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_2
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, f.fieldRange

Tactic:
· exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Goal state before:
pp: ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
a : MvPolynomial ι F
⊢ ↑(hx.aevalEquivField ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) a)) = (aeval x) a

Tactic:
by
  simp

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
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
⊢ Normal F ↥(⨅ i, t i)

Tactic:
by
  refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }
  · let f := inclusion (iInf_le t hι.some)
    exact Algebra.IsAlgebraic.of_injective f f.injective
  · have hx : ∀ i, Splits ((minpoly F x).map (algebraMap F (t i))) := by
      intro i
      rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
      exact (h i).splits' (inclusion (iInf_le t i) x)
    simp only [splits_iff_mem (Splits.of_isScalarTower K (hx hι.some))] at hx ⊢
    rintro y hy - ⟨-, ⟨i, rfl⟩, rfl⟩
    exact hx i y hy

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Nonempty (↥↑(I * J) ≃ₗ[R] ↥↑I ⊗[R] ↥↑J)

Tactic:
exact ⟨(tensorEquivMul I J).symm⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J ∪ I

Tactic:
rw [union_eq_self_of_subset_right hIJ]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep (J ∪ I)

Tactic:
rw [union_eq_self_of_subset_right hIJ]

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep J
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 ∩ Jᶜ ⊆ B'

Tactic:
← sdiff_eq,

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'' ∩ X) \ J ⊆ B'
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'ᶜ) ⊆ J

Tactic:
← sdiff_eq,

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'' ∩ (X \ B') ⊆ J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } ≤ { toMatroid := M' } ↔ M ≤r M'

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } < { toMatroid := M' } ↔ M <r M'

Tactic:
by
  simp

Goal state after: