mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mp
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
⊢ (∀ {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)

pp: case mpr
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
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
· intro h
    exact rTensor_injective_of_forall_vanishesTrivially R h

Goal state after:
case mpr
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
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mp
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
h : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
x✝ : M'.FG
⊢ Injective ⇑(rTensor N M'.subtype)

Tactic:
exact rTensor_injective_of_forall_vanishesTrivially R h M'

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

Goal state before:
pp: case mp
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
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)

Tactic:
intro h M' _
    exact rTensor_injective_of_forall_vanishesTrivially R h M'

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
t' : Finset R
hc : ↑t' ⊆ t
ht' : Ideal.span ↑t' = ⊤
this : ∀ (g : ↥t'), IsLocalization.Away (↑g) (Rₚ ⟨↑g, ⋯⟩)
⊢ Module.Finite R M

Tactic:
have (g : t') : IsLocalizedModule.Away g.val
    ((fun g ↦ f ⟨g.val, hc g.property⟩) g) := h₂ ⟨g.val, hc g.property⟩

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
t' : Finset R
hc : ↑t' ⊆ t
ht' : Ideal.span ↑t' = ⊤
this✝ : ∀ (g : ↥t'), IsLocalization.Away (↑g) (Rₚ ⟨↑g, ⋯⟩)
this : ∀ (g : ↥t'), IsLocalizedModule.Away (↑g) ((fun g ↦ f ⟨↑g, ⋯⟩) g)
⊢ Module.Finite R M
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)

Tactic:
let W := Submodule.span K (Set.range v)
  suffices ∃ b : Basis I K W, v = W.subtype ∘ b by
    obtain ⟨b, hb⟩ := this
    rw [hb, ← map_comp_ιMulti_family]
    exact LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))
  use Module.Basis.span hv
  ext i
  rw [Submodule.coe_subtype, Function.comp_apply, Basis.span_apply]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ (M.mulMap N).range = M * N

Tactic:
by
  refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)
  rintro _ ⟨x, rfl⟩
  induction x with
  | zero => rw [map_zero]; exact zero_mem _
  | tmul a b => exact mul_mem_mul a.2 b.2
  | add a b ha hb => rw [map_add]; exact add_mem ha hb

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f

Tactic:
rw [h₁, h₂]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i ((r • 1) • f i)) = tprodCoeff R (r • 1 * z) f
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
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
r✝ r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ (r✝ + r') • tprodCoeff R r f = r✝ • tprodCoeff R r f + r' • tprodCoeff R r f

Tactic:
simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
⊢ ∃ x', I = N.colon {x'}

Tactic:
have key : ∃ n ≠ 0, ∃ J : Ideal R, I ^ n * J ≤ ann ∧ ¬ J ≤ I := by
    -- let `n` be large enough so that `ann.radical ^ n ≤ ann` (uses Noetherian)
    obtain ⟨n, hn⟩ := ann.exists_radical_pow_le_of_fg ann.radical.fg_of_isNoetherianRing
    have hn0 : n ≠ 0 := by contrapose hn; simpa [hn, ann]
    -- then take `J` to be the product of the other minimal primes raised to the `n`th power
    have h := ann.finite_minimalPrimes_of_isNoetherianRing R
    rw [← ann.sInf_minimalPrimes, ← h.coe_toFinset, ← h.toFinset.inf_id_eq_sInf,
      ← Finset.insert_erase (h.mem_toFinset.mpr hI), Finset.inf_insert, id_eq] at hn
    grw [← Ideal.mul_le_inf, mul_pow] at hn
    refine ⟨n, hn0, ((h.toFinset.erase I).inf id) ^ n, hn, ?_⟩
    have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
      le_antisymm hKI (hI.2 hK.1 hKI)
    simpa [hI.isPrime.pow_le_iff hn0, hI.isPrime.inf_le', imp_not_comm, not_imp_not]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
⊢ ∃ x', I = N.colon {x'}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
⊢ ∃ s, s.head = ⊥ ∧ s.last = ⊤

Tactic:
refine WellFoundedGT.induction_top ⟨⊥, .singleton _ ⊥, rfl, rfl⟩ ?_

Goal state after:
A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
⊢ ∀ (N : Submodule A M), N ≠ ⊤ → (∃ s, s.head = ⊥ ∧ s.last = N) → ∃ M_1 > N, ∃ s, s.head = ⊥ ∧ s.last = M_1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
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
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
refine ⟨Units.mk0 x ?_, hx⟩
    rintro rfl
    simp [I.ne_zero.symm] at hx

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
c : ↥I.primeCompl
g : N →ₗ[R] M
⊢ ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      ((LocalizedModule.map I.primeCompl) g) =
    c • IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (((llcomp R N M N) f) g) c

Tactic:
IsLocalizedModule.mk'_cancel'

Goal state after:
case h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
c : ↥I.primeCompl
g : N →ₗ[R] M
⊢ ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      ((LocalizedModule.map I.primeCompl) g) =
    (LocalizedModule.map I.primeCompl) (((llcomp R N M N) f) g)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case e'_5
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
e_1✝ : ↑(bif false then C₁ else C₂) = ↑C₂
x : ↑(bif false then C₁ else C₂)
⊢ ∀ (h : ↑x ∈ C₁), f ⟨↑x, ⋯⟩ = g x

Tactic:
exact fun hx ↦ hfg x ⟨hx, x.prop⟩

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)))
      (map (algebraMap R (Localization.AtPrime p)) p) =
    map (algebraMap S (Localization (algebraMapSubmonoid S p.primeCompl))) (map (algebraMap R S) p)

Tactic:
map_map,

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
this : Algebra S (p.Fiber S) := rightAlgebra
⊢ map
      ((algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl))).comp
        (algebraMap R (Localization.AtPrime p)))
      p =
    map (algebraMap S (Localization (algebraMapSubmonoid S p.primeCompl))) (map (algebraMap R S) p)
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h'
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
H : x ∈ ↑p'
⊢ IsLocalization.mk' (Localization S) x s ∈ ↑p.asIdeal

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one]

Goal state after:
case h'
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
H : x ∈ ↑p'
⊢ (algebraMap R (Localization S)) x * IsLocalization.mk' (Localization S) 1 s ∈ ↑p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h'
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
H : x ∈ ↑p'
⊢ IsLocalization.mk' (Localization S) x s ∈ ↑p.asIdeal

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one]

Goal state after:
case h'
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
H : x ∈ ↑p'
⊢ (algebraMap R (Localization S)) x * IsLocalization.mk' (Localization S) 1 s ∈ ↑p.asIdeal
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case pos
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L'
y : K
hx : x ∈ (minpoly F y).rootSet L'
iy : IsIntegral F y
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

pp: case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L'
y : K
hx : x ∈ (minpoly F y).rootSet L'
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
· exact (h y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
          ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))

Goal state after:
case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L'
y : K
hx : x ∈ (minpoly F y).rootSet L'
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
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✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (SemimoduleCat.of R (Dual R M')) * toSkeleton (SemimoduleCat.of R M') = 1

Tactic:
← Skeleton.toSkeleton_tensorObj

Goal state after:
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✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (MonoidalCategoryStruct.tensorObj (SemimoduleCat.of R (Dual R M')) (SemimoduleCat.of R M')) = 1
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
⊢ B₁.encard = B₂.encard

Tactic:
by
  rw [← encard_sdiff_add_encard_inter B₁ B₂, exch.encard_sdiff_eq hB₁ hB₂, inter_comm,
    encard_sdiff_add_encard_inter]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: 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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑↑(piScalarRight R R A ↥S) ∘ ⇑(lTensor A f))
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑m

Tactic:
← coe_comp,

Goal state after:
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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective ⇑(↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f)
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑m
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : (B' \ I ∪ B \ I)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
← union_sdiff_distrib,

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : ((B' ∪ B) \ I)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B