mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M✶✶.RankPos ↔ ∃ K, M✶✶.IsCocircuit K

Tactic:
dual_rankPos_iff_exists_isCircuit,

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∃ C, M✶.IsCircuit C) ↔ ∃ K, M✶✶.IsCocircuit K
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)

Tactic:
have hf := closure_exchange he

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X : B' ⊆ X
⊢ B ⊆ X

Tactic:
← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)

Goal state after:
α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X : B' ⊆ X
⊢ B' ⊆ X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case pos
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
he : M.Indep (insert e I)
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

Tactic:
simp [he, and_comm, insert_subset_iff, hIR, (he.subset_ground (mem_insert ..)),
      imp_or_left_iff_true]

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ range x = s

Tactic:
have := H.2 (f '' s)
    ((algebraicIndependent_image h.injOn).mp ((AlgHom.algebraicIndependent_iff f h).mpr hs))
    (by rw [Set.range_comp]; exact Set.image_mono hs')

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
this : range (⇑f ∘ x) = ⇑f '' s
⊢ range x = s
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure (f '' (f ⁻¹' X ∩ M.E)) = (M.map f hf).closure (f '' I)

Tactic:
← (hI.map hf).closure_eq_closure

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure (f '' I) = (M.map f hf).closure (f '' I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
⊢ M.Indep (insert x I)

Tactic:
have hrw := image_insert_eq ▸ hJI

Goal state after:
case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' J)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Function.Injective ⇑i1

Tactic:
rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Function.Injective ⇑((algebraMap K (AlgebraicClosure K)).comp (algebraMap (MvPolynomial ι F) K))
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ (f.aroots (AlgebraicClosure F)).toFinset.card ≤ (g.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ (𝓝 1).HasBasis (fun V ↦ V ∈ B) id

Tactic:
rw [B.nhds_one_eq]

Goal state after:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.filter.HasBasis (fun V ↦ V ∈ B) id
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F E

Tactic:
rw [← isSeparable_top, ← (isSplittingField_iff_intermediateField.mp sp).2,
    isSeparable_adjoin_iff_isSeparable]
  exact fun x hx ↦ hp.of_dvd (minpoly.dvd F x (aeval_eq_zero_of_mem_rootSet hx))

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
⊢ IsGalois F E

Tactic:
by
  apply of_fixedField_eq_bot
  have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup Gal(E/F))) E := finrank_pos
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (algebraMap R S) ((minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1)) +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum

Tactic:
simp [minpoly.eq_zero hx, trace_gen_eq_zero hx, aroots_def]

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
⊢ FixedPoints.intermediateField G ≤ ⊥

Tactic:
exact Algebra.IsInvariant.isInvariant

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

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
x✝ : Nat.Prime p ∨ p = 0
⊢ False

Tactic:
cases CharP.char_is_prime_or_zero K p with

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
⊢ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum * ↑↑a ^ k - 1 * (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0

Tactic:
← h_multiset_map_sum,

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum - 1 * (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x, x ^ i = ∑ x ∈ univ \ {0}, x ^ i

Tactic:
by
        rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]

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

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ (frobenius K p ^ (n + 1)) x = x ^ p ^ (n + 1)

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
⊢ (Ideal.span {↑n}).IsRadical ↔ Squarefree n ∨ n = 0

Tactic:
← isRadical_iff_span_singleton,

Goal state after:
n : ℕ
⊢ IsRadical ↑n ↔ Squarefree n ∨ n = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p

Tactic:
rintro p (hpa | hpb)

Goal state after:
case neg.refine_1.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hpa : p ∈ normalizedFactors a
⊢ Prime p

case neg.refine_1.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hpb : p ∈ normalizedFactors b
⊢ Prime p
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsOpen[inst✝] (closure[inst✝] Z \ Z)ᶜ → (Z ∩ closedPoints X).Nonempty

Tactic:
isOpen_compl_iff,

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsClosed[inst✝] (closure[inst✝] Z \ Z) → (Z ∩ closedPoints X).Nonempty
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : ¬IsFiniteLength B M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
have : ¬ IsFiniteLength A M := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      exact h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)
    rw [← length_ne_top_iff, not_ne_iff] at h this
    have ne : length (ResidueField A) (ResidueField B) ≠ 0 := by
      simpa [pos_iff_ne_zero] using Module.length_pos
    rw [h, this, ENat.top_mul ne]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
⊢ p.ramificationIdx' P ≠ 0

Tactic:
have hP0 : P ≠ ⊥ := by
    rintro rfl
    exact hp0 (le_bot_iff.mp le)

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
⊢ p.ramificationIdx' P ≠ 0
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
⊢ ∃ a, elem R S = a.sum fun i x ↦ x ⊗ₜ[R] b i

Tactic:
let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
⊢ ∃ a, elem R S = a.sum fun i x ↦ x ⊗ₜ[R] b i
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
i : A
⊢ ((f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift).comp
        (Ideal.Quotient.mkₐ R (RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2)))
      (X i) =
    (((Ideal.Quotient.mkₐ R I).comp l).comp
        (Ideal.Quotient.mkₐ R (RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2)))
      (X i)

Tactic:
change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l✝ : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l✝ ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
H : ∀ (x : P.Ring), (Ideal.Quotient.mk I) ((aeval (σ ∘ ⇑f)) x) = f ((algebraMap P.Ring A) x)
l : P.Ring ⧸ RingHom.ker (algebraMap P.Ring A) ^ 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ (RingHom.ker (algebraMap P.Ring A) ^ 2) (aeval (σ ∘ ⇑f)) ⋯
i : A
⊢ f ((algebraMap P.Ring A) (X i)) = (algebraMap B (B ⧸ I)) ((aeval (σ ∘ ⇑f)) (X i))
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
have : IsLocalizedModule p.primeCompl (.id (R := S) (M := Localization.AtPrime p)) :=
    ⟨IsLocalizedModule.map_units (Algebra.linearMap S (Localization.AtPrime p)),
      fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, p.primeCompl.one_mem⟩⟩
  have : Module.Finite R (Localization.AtPrime p) := .of_quasiFinite
  have : Module.Finite S (Localization.AtPrime p) := .of_restrictScalars_finite R _ _
  have : IsArtinianRing (Localization.AtPrime p) := .of_finite R _
  have : IsNoetherianRing S := Algebra.EssFiniteType.isNoetherianRing R S
  have : Module.FinitePresentation S (Localization.AtPrime p) :=
    Module.finitePresentation_of_finite _ _
  obtain ⟨r, hrp, H⟩ := IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation
    p.primeCompl (Algebra.linearMap S (Localization.AtPrime p))
  have : IsLocalization (.powers r) (Localization.AtPrime p) :=
    (isLocalizedModule_iff_isLocalization' _ _).mp H
  let φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
    IsLocalization.algEquiv (.powers r) _ _
  refine ⟨r, hrp, subset_antisymm (fun q hrq ↦ ?_) (Set.singleton_subset_iff.mpr hrp)⟩
  obtain ⟨q, rfl⟩ := (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r).ge hrq
  obtain ⟨q, rfl⟩ := (PrimeSpectrum.comapEquiv φ.toRingEquiv).symm.surjective q
  -- As Sₚ is an artinian local ring, its prime spectrum is a singleton.
  obtain rfl : q = IsLocalRing.closedPoint _ := Subsingleton.elim _ _
  ext1
  dsimp [-RingEquiv.symm_mk]
  rw [Ideal.comap_comap, ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
  exact IsLocalization.AtPrime.under_maximalIdeal _ _

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

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
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this✝ : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
x✝¹ : q'.IsPrime
hq' : q' ≠ q
x✝ : q'.LiesOver p
hxq' : x ∉ q'
⊢ e ⟨{ asIdeal := q', isPrime := x✝¹ }, ⋯⟩ ∈ ↑(PrimeSpectrum.basicOpen r)

Tactic:
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.preimageHomeomorphFiber,
    PrimeSpectrum.preimageOrderIsoFiber, Homeomorph.homeomorph_mk_coe, Set.mem_compl_iff,
    PrimeSpectrum.mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe, e]

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
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this✝ : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
x✝¹ : q'.IsPrime
hq' : q' ≠ q
x✝ : q'.LiesOver p
hxq' : x ∉ q'
⊢ r ∉
    ((PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ })
        ⟨{ asIdeal := q', isPrime := x✝¹ }, ⋯⟩).asIdeal
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
i : ι
⊢ ((Finsupp.single i 1).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) 1 = 0

Tactic:
simp only [Derivation.map_one_eq_zero, tmul_zero]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial.add
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
y₁ y₂ : MvPolynomial ι S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r) +
      ((monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)) =
    (monomial n) r • (δAux R Q) y₁ + (monomial n) r • (δAux R Q) y₂ +
      (y₁ • (δAux R Q) ((monomial n) r) + y₂ • (δAux R Q) ((monomial n) r))

Tactic:
abel

Goal state after: