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✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
⊢ (ι →₀ R) ≃ₗ[R] M

Tactic:
refine LinearEquiv.ofBijective i ⟨?_, hi⟩
    -- By Nakayama's lemma, it suffices to show that `k ⊗ ker(i) = 0`.
    rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
      ← IsLocalRing.subsingleton_tensorProduct (R := R), subsingleton_iff_forall_eq 0]
    have : Function.Surjective (i.baseChange k) := i.lTensor_surjective _ hi
    -- By construction, `k ⊗ i : kᴵ → k ⊗ M` is bijective.
    have hi' : Function.Bijective (i.baseChange k) := by
      refine ⟨?_, this⟩
      rw [← LinearMap.ker_eq_bot (M := k ⊗[R] (ι →₀ R)) (f := i.baseChange k),
        ← Submodule.finrank_eq_zero (R := k) (M := k ⊗[R] (ι →₀ R)),
        ← Nat.add_right_inj (n := Module.finrank k (LinearMap.range <| i.baseChange k)),
        LinearMap.finrank_range_add_finrank_ker (V := k ⊗[R] (ι →₀ R)),
        LinearMap.range_eq_top.mpr this, finrank_top]
      simp only [Module.finrank_tensorProduct, Module.finrank_self,
        Module.finrank_finsupp_self, one_mul, add_zero]
      rw [Module.finrank_eq_card_basis bk]
    -- On the other hand, `m ⊗ M → M` injective => `Tor₁(k, M) = 0` => `k ⊗ ker(i) → kᴵ` injective.
    intro x
    refine lTensor_injective_of_exact_of_exact_of_rTensor_injective
      (N₁ := LinearMap.ker i) (N₂ := ι →₀ R) (N₃ := M)
      (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪)
      (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪)
      (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_
    · apply Module.Flat.lTensor_preserves_injective_linearMap
      exact Subtype.val_injective
    · apply hi'.injective
      rw [LinearMap.baseChange_eq_ltensor]
      erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp]
      rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]
      simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero]

Goal state after:
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✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r : R₁
r' r'' : R
f : (i : ι) → s i
⊢ tprodCoeff R (r • (r', f).1) (r', f).2 + tprodCoeff R (r • (r'', f).1) (r'', f).2 =
    tprodCoeff R (r • (r' + r'', f).1) (r' + r'', f).2

Tactic:
by simp [add_tprodCoeff']

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective ⇑(M.mulRightMap n)

Tactic:
mulRightMap_eq_mulMap_comp,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective
    ⇑(M.mulMap N ∘ₗ
        LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R R (↥M) ι).symm)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : 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)
z : R
f : (i : ι) → s i
⊢ tprodCoeff R z f = z • (tprod R) f

Tactic:
have : z = z • (1 : R) := by simp only [mul_one, smul_eq_mul]

Goal state after:
ι : 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)
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • (tprod R) f
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this :
  (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) x.snd) =
    (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯).symm (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd

Tactic:
cast_symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
this :
  (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) x.snd) =
    (cast R M ⋯) (GradedMonoid.GMul.mul x.snd (algebraMap₀ r))
⊢ (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd =
    (cast R M ⋯) (x * GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r)).snd
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
⊢ (r • x).snd = (cast R M ⋯).symm (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd

Tactic:
cast_symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
⊢ (r • x).snd = (cast R M ⋯) (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : 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)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
                  lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))).compMultilinearMap
              (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

Tactic:
simp only [map_add, LinearMap.compMultilinearMap_apply,
    lift.tprod, add_apply, LinearMap.add_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this✝ : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
this : Subsingleton (k ⊗[R] ↥l.ker)
⊢ Function.Injective ⇑l

Tactic:
rwa [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
        ← IsLocalRing.subsingleton_tensorProduct (R := R)]

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

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)

Tactic:
apply Cardinal.lift_injective.{max uM' uR'}

Goal state after:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

Tactic:
· exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy).mp h

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

Goal state before:
pp: case inr
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
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ 1

Tactic:
← hn,

Goal state after:
case inr
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
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ n.gcd (Fintype.card (ClassGroup R))
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
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ 1

Tactic:
← hn,

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
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n.gcd (Fintype.card (ClassGroup R))
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, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ↑((Units.map ↑(IsFractionRing.ringEquivOfRingEquiv f).toRingHom) v) = ↑I

Tactic:
rw [← 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, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ↑((Units.map ↑(IsFractionRing.ringEquivOfRingEquiv f).toRingHom) v) =
    ↑((Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
let U := f ⁻¹' {f y}

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y
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✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
⊢ IsLocalizedModule S (f.prodMap g)

Tactic:
let : Module (Localization S) M' := IsLocalizedModule.module S f

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this : Module (Localization S) M' := module S f
⊢ IsLocalizedModule S (f.prodMap g)
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
  classical
  apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
  intro x
  rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
  ext
  simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]

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:
eSp.nontrivial_congr,

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
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 (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
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
⊢ IsLocallyConstant fun x ↦ rankAtStalk M ↑x

Tactic:
refine (IsLocallyConstant.iff_exists_open _).mpr fun ⟨x, hx⟩ ↦ ?_

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
⊢ ∃ U, IsOpen U ∧ ⟨x, hx⟩ ∈ U ∧ ∀ x' ∈ U, rankAtStalk M ↑x' = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ ⊥

Tactic:
← hn,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ _root_.commutator G
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
h : rankAtStalk M = 0
p : PrimeSpectrum R
⊢ p ∉ support R M

Tactic:
rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_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
⊢ ∃ p, IsSplittingField F K p

Tactic:
by
  classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  refine fun x =>
    Algebra.subset_adjoin
      (Multiset.mem_toFinset.mpr <|
        (mem_roots <|
              mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

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
i : ↥S
x : A
hx : x ∈ ↑I
⊢ (LinearMap.mulRight R (r ↑i • a i)) x ∈ (Algebra.linearMap R A).range

Tactic:
by
      rw [← one_eq_range, ← I.mul_inv]; exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)

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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
refine fun X _ I hI hIX ↦ zorn_subset_nonempty {Y | Indep Y ∧ Y ⊆ X} ?_ I ⟨hI, hIX⟩

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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
⊢ ∀ c ⊆ {Y | Indep Y ∧ Y ⊆ X},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {Y | Indep Y ∧ Y ⊆ X}, ∀ s ∈ c, s ⊆ ub
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 → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
b : α
hb : b ∈ B₀ \ I
⊢ ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑⟨b, hb⟩) Ib)

Tactic:
exact htofin I b hI (hcon b ⟨hB₀B hb.1, hb.2⟩)

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

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E

Tactic:
by
  rw [isBasis'_iff_isBasis_inter_ground, freeOn_isBasis_iff, freeOn_ground,
    and_iff_left inter_subset_right]

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

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E).IsBase ((uniqueBaseOn (I ∩ E) E).E \ B) ↔ (uniqueBaseOn (E \ I) E).IsBase B

Tactic:
uniqueBaseOn_isBase_iff inter_subset_right,

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E).E \ B = I ∩ E ↔ (uniqueBaseOn (E \ I) E).IsBase B
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).IsBase (I ∩ E) ∧ (I ∩ E).Finite

Tactic:
uniqueBaseOn_isBase_iff inter_subset_right,

Goal state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ I ∩ E = I ∩ E ∧ (I ∩ E).Finite
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₁.toMatroid ≤r M₃.toMatroid

Tactic:
rw [h₁, restrict_restrict_eq _ (show R ⊆ R' from hR)]

Goal state after:
α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₃.toMatroid ↾ R ≤r M₃.toMatroid
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
⊢ N.IsBasis I X

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := hNM; rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

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

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).RankFinite

Tactic:
exact Matroid.IsBase.rankFinite_of_finite (by simpa) hfin

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
⊢ (N.comap f).Finitary

Tactic:
by
  refine ⟨fun I hI ↦ ?_⟩
  rw [comap_indep_iff, indep_iff_forall_finite_subset_indep]
  simp only [forall_subset_image_iff]
  refine ⟨fun J hJ hfin ↦ ?_,
    fun x hx y hy ↦ (hI _ (pair_subset hx hy) (by simp)).2 (by simp) (by simp)⟩
  obtain ⟨J', hJ'J, hJ'⟩ := (surjOn_image f J).exists_bijOn_subset
  rw [← hJ'.image_eq] at hfin ⊢
  exact (hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

Goal state after: