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

Goal state before:
pp: case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
⊢ a • (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (P.σ b) = a ⊗ₜ[R] b

Tactic:
have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
this : ∀ (y : P.Ring), (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) y = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) y
⊢ a • (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (P.σ b) = a ⊗ₜ[R] b
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

Tactic:
rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]

Goal state after:
case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Function.Surjective ⇑(pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm)
Module: Mathlib.Algebra.Module.Presentation.Finite

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = (Finsupp.linearCombination A var).ker
⊢ { var := var, linearCombination_var_relation := ⋯ }.IsPresentation

Tactic:
Relations.Solution.isPresentation_iff

Goal state after:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = (Finsupp.linearCombination A var).ker
⊢ Submodule.span A (Set.range { var := var, linearCombination_var_relation := ⋯ }.var) = ⊤ ∧
    { var := var, linearCombination_var_relation := ⋯ }.π.ker =
      Submodule.span A (Set.range { G := G, R := R, relation := relation }.relation)
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
⊢ Subsingleton ↥P.cotangentComplex.ker ↔ Function.Injective ⇑P.cotangentComplex

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Subsingleton ↥P.cotangentComplex.ker ↔ P.cotangentComplex.ker = ⊥
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ support R M ∩ zeroLocus ↑I

Tactic:
refine Set.subset_inter ?_ ?_
    · exact Module.support_subset_of_surjective _ (Submodule.mkQ_surjective _)
    · rw [support_eq_zeroLocus]
      apply PrimeSpectrum.zeroLocus_anti_mono_ideal
      rw [Submodule.annihilator_quotient]
      exact fun x hx ↦ Submodule.mem_colon.mpr fun p hp ↦ Submodule.smul_mem_smul hx hp

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

Goal state before:
pp: n : ℕ
k : Fin n
hn : Even n
⊢ Even k ↔ ↑k % 2 = 0

Tactic:
rw [even_iff_of_even hn]
  exact Nat.even_iff

Goal state after:
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N : Submodule R M
fg : N.FG
this✝ : Module 𝓀 (↥N ⧸ maximalIdeal R • ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R 𝓀 (↥N ⧸ maximalIdeal R • ⊤) := spanFinrank_eq_finrank_quotient._proof_1_7 N
⊢ Module.finrank 𝓀 (𝓀 ⊗[R] ↥N) = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)

Tactic:
let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) :=
    (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N : Submodule R M
fg : N.FG
this✝ : Module 𝓀 (↥N ⧸ maximalIdeal R • ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R 𝓀 (↥N ⧸ maximalIdeal R • ⊤) := spanFinrank_eq_finrank_quotient._proof_1_7 N
e : 𝓀 ⊗[R] ↥N ≃ₗ[𝓀] ↥N ⧸ maximalIdeal R • ⊤ :=
  LinearEquiv.extendScalarsOfSurjective ⋯ (quotTensorEquivQuotSMul (↥N) (maximalIdeal R))
⊢ Module.finrank 𝓀 (𝓀 ⊗[R] ↥N) = Module.finrank (R ⧸ maximalIdeal R) (↥N ⧸ maximalIdeal R • ⊤)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
⊢ Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂ → N₁ = N₂

Tactic:
intro hN
    have : N₂ ≤ 𝔪 • N₂ ⊔ N₁ := by
      simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge
    rw [sup_comm] at this
    exact h.antisymm (Submodule.le_of_le_smul_of_le_jacobson_bot h'
      (by rw [jacobson_eq_maximalIdeal]; exact bot_ne_top) this)

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) s = 1

Tactic:
by
  simpa [basis_repr_apply] using ιMultiDual_apply_diag R n b s

Goal state after:
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
⊢ Function.Injective ⇑i

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
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
⊢ i.ker = ⊥
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✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i✝ : ι
hi : i✝ ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
i : ↥(insert n✝ s)
⊢ a i j = if hi : ↑i ∈ insert n✝ s then a ⟨↑i, hi⟩ j else 0

Tactic:
dif_pos i.2

Goal state after:
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
n : ℕ
⊢ algebraMap₀ ↑(n + 1) = algebraMap₀ ↑n + GradedMonoid.GOne.one

Tactic:
by simp only [Nat.cast_succ, map_add, algebraMap₀_one]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
I : Ideal R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ ¬IsAssociatedPrime I M

Tactic:
rintro ⟨hI, x, hx⟩
  apply hI.ne_top
  simp [hx, Subsingleton.elim x 0]

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

Goal state before:
pp: case refine_1.refine_2
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 ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
this : map N₁.mkQ (A ∙ x) = map f (map (↑e.symm) (A ∙ 1))
⊢ N₂ ≤ A ∙ x ⊔ N₁.mkQ.ker

Tactic:
← comap_map_eq,

Goal state after:
case refine_1.refine_2
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 ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
this : map N₁.mkQ (A ∙ x) = map f (map (↑e.symm) (A ∙ 1))
⊢ N₂ ≤ comap N₁.mkQ (map N₁.mkQ (A ∙ x))
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:
← LinearMap.ker_eq_bot,

Goal state after:
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)
⊢ l.ker = ⊥
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: 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 : ℕ
y : M
hy : f y = b ^ n • x
⊢ b ∈ p

Tactic:
by_contra H

Goal state after:
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 : ℕ
y : M
hy : f y = b ^ n • x
H : b ∉ p
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal

Tactic:
by_contra hxp₂

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
⊢ False
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Polynomial.aeval ((Algebra.lmul A B) x)) f = 0
⊢ (Polynomial.aeval x) f = 0

Tactic:
aeval_algHom_apply

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Algebra.lmul A B) ((Polynomial.aeval x) f) = 0
⊢ (Polynomial.aeval x) f = 0
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 := ⋯
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := ⋯
Mₚ : Type (max uR uM) := ⋯
this✝¹ : Algebra (Localization S) Rₚ := ⋯
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
⊢ ∀ (x : ↥p.asIdeal.primeCompl), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R (Localization S)) p'.primeCompl

Tactic:
· rintro ⟨x, hx⟩
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
      refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
      rw [IsLocalization.mk'_eq_mul_mk'_one]
      exact Ideal.mul_mem_right _ _ H

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 := ⋯
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := ⋯
Mₚ : Type (max uR uM) := ⋯
this✝⁶ : Algebra (Localization S) Rₚ := ⋯
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := ⋯
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M := ⋯
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
⊢ ∀ (x : ↥p.asIdeal.primeCompl), ∃ m, m * ↑x ∈ Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl

Tactic:
· rintro ⟨x, hx⟩
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
      refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
      rw [IsLocalization.mk'_eq_mul_mk'_one]
      exact Ideal.mul_mem_right _ _ H

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
cases n

Goal state after:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
⊢ ∀ (a b : G), a * b = b * a

case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: 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 := ⋯ }
⊢ x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹

Tactic:
unfold x y z

Goal state after:
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 := ⋯ }
⊢ { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ } =
    { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ } *
        ⁅{ toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ },
          { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ } *
              { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ } *
            { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }⁻¹⁆ *
      { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }⁻¹
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ ↑(⨆ f, f.fieldRange).val x ∈ ⇑↑(⨆ f, f.fieldRange).val '' ↑(⨆ f, f.fieldRange)

Tactic:
RingHom.coe_coe,

Goal state after:
case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ⇑(⨆ f, f.fieldRange).val '' ↑(⨆ f, f.fieldRange)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
hL2 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hf
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) = 0

pp: case hg
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0

Tactic:
· rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]

Goal state after:
case hg
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
rw [show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1] at β_in_K

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : (x - y) • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯