mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.zero
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ Finsupp.single r (presB.π 0) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ ∀ (a : presB.G) (b : A) (f : presB.G →₀ A),
    a ∉ f.support →
      b ≠ 0 →
        Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r (presB.π (Finsupp.single a b + f)) ∈
            Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
· simp

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ ∀ (a : presB.G) (b : A) (f : presB.G →₀ A),
    a ∉ f.support →
      b ≠ 0 →
        Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single r (presB.π (Finsupp.single a b + f)) ∈
            Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial.isTrue
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
h✝ : a = 0
⊢ 0 = if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

pp: case a.convert_4.monomial.isFalse
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
h✝ : ¬a = 0
⊢ (if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0) = if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

Tactic:
· simp only [*, map_zero, ite_self]

Goal state after:
case a.convert_4.monomial.isFalse
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
h✝ : ¬a = 0
⊢ (if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0) = if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0
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
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j, a i j • y j
ham : ∀ (j : κ), ∑ i, a i j • m i = 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (j : Fin (Fintype.card κ)), ∑ i, (fun x ↦ a x ∘ ⇑e) i j • m i = 0

Tactic:
by
    rwa [← e.forall_congr_right] at ham

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 ι
i : ι
⊢ P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)

Tactic:
simp [cotangentSpaceBasis, toExtension]

Goal state after:
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
⊢ support R M ⊆ PrimeSpectrum.zeroLocus {1} ↔ Subsingleton M

Tactic:
← LocalizedModule.subsingleton_iff_support_subset,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Subsingleton (LocalizedModule.Away 1 M) ↔ Subsingleton M
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
i j : Fin n
hij : i ≤ j
⊢ (Equiv.symm σ) i ≤ (Equiv.symm σ) j

Tactic:
obtain ⟨i, rfl⟩ := σ.surjective i
    obtain ⟨j, rfl⟩ := σ.surjective j
    simp only [Equiv.symm_apply_apply]
    by_contra! h
    obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
    simp only [lt_self_iff_false] at h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

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.LinearDisjoint N ↔ (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M))

Tactic:
by
  simp only [linearDisjoint_iff, mulMap_op, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp]

Goal state after:
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)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ ↑p + ↑q = x + y

Tactic:
hp,

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)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ x + ↑q = x + y
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)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
⊢ (map fun i ↦ g i ∘ₗ f i) = map g ∘ₗ map f

Tactic:
by
  ext
  simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.coe_comp, Function.comp_apply]

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

Goal state before:
pp: case right.refine_2
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
x✝ : ι
⊢ 1 ⊗ₜ[R] v x✝ = (Basis.mk ⋯ ⋯) x✝

Tactic:
· simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.rTensor P (Submodule.subtype 𝔪))

Tactic:
← LinearMap.lTensor_inj_iff_rTensor_inj

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.lTensor P (Submodule.subtype 𝔪))
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
N₁ N₂ : Submodule A M
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x

Tactic:
let f := mapQ (N₁.submoduleOf N₂) N₁ N₂.subtype le_rfl

Goal state after:
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔ ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : IsUnit ↑I
a : R
K : Ideal R
ha0 : a ≠ 0
h : (↑I)⁻¹ = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ * ↑K
hIK : I * K = span {a}
⊢ Submodule.IsPrincipal (I * K)

Tactic:
simpa [hIK] using (inferInstance : (Ideal.span {a}).IsPrincipal)

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

Goal state before:
pp: case mpr.refine_1
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
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ ((FractionRing.algEquiv R K).symm x) =
    ↑((Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv) I)

pp: case mpr.refine_2
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
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ↑((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
        ((Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv) I)) =
    ↑I

Tactic:
· simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl

Goal state after:
case mpr.refine_2
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
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ↑((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
        ((Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv) I)) =
    ↑I
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
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hs : (s ∩ (U ∩ Uᶜ)).Nonempty
hxV : x ∈ Uᶜ
⊢ False

Tactic:
simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (finsuppLEquivDirectSum S M' ι).symm
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x)) =
    Finsupp.mapRange ⇑ε ⋯ x

Tactic:
LinearEquiv.symm_apply_eq

Goal state after:
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 ε
x : ι →₀ M
⊢ (LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x) =
    (finsuppLEquivDirectSum S M' ι) (Finsupp.mapRange ⇑ε ⋯ x)
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:
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.GroupTheory.Solvable

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

Tactic:
by
  induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _

Goal state after:
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:
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.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
⊢ z⁻¹ * (z * ⁅x, y * x * y⁻¹⁆) ∈ derivedSeries (Perm (Fin 5)) (n + 1)

Tactic:
inv_mul_cancel_left

Goal state after:
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, y * x * y⁻¹⁆ ∈ derivedSeries (Perm (Fin 5)) (n + 1)
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
this : Unique (Free.ChooseBasisIndex R M)
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
exact ⟨e ≪≫ₗ uniqueLinearEquiv R R default⟩

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
E E' : IntermediateField F K
inst✝¹ : Normal F ↥E
inst✝ : Normal F ↥E'
⊢ ∀ (i : Bool), Normal F ↥(Bool.rec E' E i)

Tactic:
rintro (_ | _) <;> infer_instance

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

Goal state before:
pp: case refine_2
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)
x : ↥(⨅ i, t i)
hx : ∀ (i : ι), (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨅ i, t i)) (minpoly F x)).Splits

Tactic:
simp only [splits_iff_mem (Splits.of_isScalarTower K (hx hι.some))] at hx ⊢

Goal state after:
case refine_2
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)
x : ↥(⨅ i, t i)
hx : ∀ (i : ι), ∀ x_1 ∈ (minpoly F x).rootSet K, x_1 ∈ t i
⊢ ∀ x_1 ∈ (minpoly F x).rootSet K, x_1 ∈ ⨅ i, t i
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✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β : E
hK : P K
⊢ P (IntermediateField.restrictScalars F (↥K)⟮β⟯)

Tactic:
obtain ⟨α, hK⟩ := hK

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P (IntermediateField.restrictScalars F (↥K)⟮β⟯)
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
α : E
hprim : F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Tactic:
have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)

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
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥F⟮α⟯
⊢ FiniteDimensional F E
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(finrank F E)

Tactic:
by
  rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]
  exact minpoly.ne_zero_of_finite F α

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
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = J ∩ M.E ∩ X

Tactic:
inter_eq_self_of_subset_left hJ.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = J ∩ X