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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.closure (B \ {e}) ⊆ M.E

Tactic:
apply closure_subset_ground

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)

Tactic:
cRk_union_closure_left_eq,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (X ∪ {e}) = M.cRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ∀ J ∈ range Is, J ⊆ ⋃ i, Is i

Tactic:
simp [subset_iUnion]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.RankFinite ↔ M.cRank < ℵ₀

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩

Goal state after:
case refine_1
α : Type u
M : Matroid α
h : M.RankFinite
⊢ M.cRank < ℵ₀

case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
⊢ ∃ B, M.IsBase B ∧ B.Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
rw [h.closure_eq, isBasis_ground_iff] at hB'

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
⊢ f x ∈ M.E →
    (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x)

Tactic:
hxE

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ minpoly F (i x) ≠ 0 ↔ minpoly F x ≠ 0

Tactic:
minpoly.algHom_eq i i.injective

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
⊢ AlgebraicIndependent S x

Tactic:
refine algebraicIndependent_of_finite_type'
    (Algebra.IsAlgebraic.injective_tower_top S hx.algebraMap_injective) fun t fin ind i hi ↦ ?_

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
⊢ b ∈ s

Tactic:
let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : ⟨g, g_fixing⟩ • a = b
⊢ b ∈ s
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ finSepDegree F F = 1

Tactic:
rw [finSepDegree, Nat.card_eq_one_iff_unique]
  constructor <;> infer_instance

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n)) (X - C (-g.coeff 0))

Tactic:
map_neg,

Goal state after:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n)) (X - -C (g.coeff 0))
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = B.N x₀

Tactic:
by
  apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)
  · intro a U U_in
    exact ⟨1, B.one U_in, mul_one a⟩
  · intro a U U_in
    rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩
    filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]
    rintro _ ⟨x, hx, rfl⟩
    calc
      (a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
      _ = a • x • V := smul_smul .. |>.symm
      _ ⊆ a • (V * V) := smul_set_mono <| smul_set_subset_smul hx
      _ ⊆ a • U := smul_set_mono hVU

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

Goal state before:
pp: case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E

pp: case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Tactic:
· intro h
    exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

Goal state after:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E
Module: Mathlib.FieldTheory.SeparableClosure

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
i : E →ₐ[F] K
x : E
⊢ (minpoly F (i x)).Separable ↔ (minpoly F x).Separable

Tactic:
minpoly.algHom_eq i i.injective

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finInsepDegree F ↥⊥ = 1

Tactic:
finInsepDegree_eq_of_equiv _ _ _ (botEquiv F E),

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finInsepDegree F F = 1
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ (algebraMap F E) (-(minpoly F x).coeff 0) = x ^ q ^ n

Tactic:
map_neg,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ -(algebraMap F E) ((minpoly F x).coeff 0) = x ^ q ^ n
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : (algebraMap K g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0

Tactic:
rw [eval₂_eq_eval_map]

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : (algebraMap K g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) = 0
⊢ eval (g.coeff n) (map (algebraMap R K) p) = 0
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
⊢ IsUnit f ↔ IsUnit (map φ f)

Tactic:
refine ⟨(mapRingHom φ).isUnit_map, fun h => ?_⟩
  rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
  have hdeg := degree_C u.ne_zero
  rw [hu, degree_map_eq_of_injective hinj] at hdeg
  rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢
  exact isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)

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

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
inst✝ : Algebra.IsAlgebraic F E
x : E
⊢ IsIntegral (↥(separableClosure F E)) x ∧
    (IsSeparable (↥(separableClosure F E)) x → x ∈ (algebraMap (↥(separableClosure F E)) E).range)

Tactic:
set L := separableClosure F E
  refine ⟨(IsAlgebraic.tower_top L (Algebra.IsAlgebraic.isAlgebraic (R := F) x)).isIntegral,
    fun h ↦ ?_⟩
  have := (isSeparable_adjoin_simple_iff_isSeparable L E).2 h
  have : Algebra.IsSeparable F (restrictScalars F L⟮x⟯) := Algebra.IsSeparable.trans F L L⟮x⟯
  have hx : x ∈ L⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x
  exact ⟨⟨x, mem_separableClosure_iff.2 <| isSeparable_of_mem_isSeparable F E hx⟩, rfl⟩

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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
⊢ IsSepClosed F

Tactic:
have := IsAlgClosure.isAlgClosed F (K := E)
    rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H

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

Goal state before:
pp: S : Type u_2
inst✝⁵ : CommRing S
K : Type u_4
inst✝⁴ : Field K
F : Type u_6
inst✝³ : Field F
inst✝² : Algebra K S
inst✝¹ : Algebra K F
inst✝ : Nontrivial S
pb : PowerBasis K S
hf : (Polynomial.map (algebraMap K F) (minpoly K pb.gen)).Splits
⊢ (algebraMap K F) (-(minpoly K pb.gen).nextCoeff) = ((minpoly K pb.gen).aroots F).sum

Tactic:
map_neg,

Goal state after:
S : Type u_2
inst✝⁵ : CommRing S
K : Type u_4
inst✝⁴ : Field K
F : Type u_6
inst✝³ : Field F
inst✝² : Algebra K S
inst✝¹ : Algebra K F
inst✝ : Nontrivial S
pb : PowerBasis K S
hf : (Polynomial.map (algebraMap K F) (minpoly K pb.gen)).Splits
⊢ -(algebraMap K F) (minpoly K pb.gen).nextCoeff = ((minpoly K pb.gen).aroots F).sum
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Semiring C
inst✝⁸ : Algebra A C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction (G ⧸ N) B := mulSemiringActionQuotient G B C N
g : G
q : G ⧸ N
b : B
h : G
⊢ (g • Quotient.mk'' h) • b = g • Quotient.mk'' h • b

Tactic:
simp [mul_smul, mulSemiringActionQuotient_smul_def]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
· exact ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (by positivity), h⟩

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
⊢ ¬∃ s, Nonempty (Basis (↥s) K L)

Tactic:
rintro ⟨s, ⟨b⟩⟩

Goal state after:
case neg.h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
s : Finset L
b : Basis (↥s) K L
⊢ False
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
⊢ traceMatrix A ⇑(b.reindex f) = (reindex f f) (traceMatrix A ⇑b)

Tactic:
by ext (x y); simp

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b) = P * traceMatrix A b * Pᵀ

Tactic:
refine AddEquiv.injective (transposeAddEquiv κ κ A) ?_
  rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
by
  suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0 by
    refine mt (fun ht => ?_) this
    rw [ht, map_zero]
  have : FiniteDimensional K L := pb.finite
  let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm
  · rw [RingHom.map_det, RingHom.mapMatrix_apply,
      traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
      embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]
    refine mt mul_self_eq_zero.mp ?_
    simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]
    rintro i ⟨_, j, hij, h⟩
    exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)
  · rw [AlgHom.card, pb.finrank]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
h : q = 1
this : 0 = 1
⊢ False

Tactic:
exact absurd this zero_ne_one

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.val ^ 2 + ↑b.val ^ 2 = ↑x

Tactic:
simpa using congr_arg (ZMod.castHom dvd_rfl R) hab

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ M
N : Submodule ℤ M
bN : Basis ι ℤ ↥N
e : M ≃ₗ[ℤ] ↥N := b.equiv bN (Equiv.refl ι)
⊢ (b.det (⇑N.subtype ∘ ⇑bN)).natAbs = (LinearMap.det (N.subtype ∘ₗ ↑e)).natAbs

Tactic:
Basis.det_comp_basis

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ M
N : Submodule ℤ M
bN : Basis ι ℤ ↥N
e : M ≃ₗ[ℤ] ↥N := b.equiv bN (Equiv.refl ι)
⊢ (LinearMap.det (N.subtype ∘ₗ ↑(b.equiv bN (Equiv.refl ι)))).natAbs = (LinearMap.det (N.subtype ∘ₗ ↑e)).natAbs
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ P (Multiset.map id (normalizedFactors a)).prod

Tactic:
Finset.prod_multiset_map_count

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case refine_2
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ (RingHom.ker (MvPolynomial.algebraTensorAlgEquiv R B).symm).FG

Tactic:
simp only [RingHom.ker_equiv]

Goal state after:
case refine_2
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ ⊥.FG
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Irreducible (absNorm I)
h : IsUnit I
⊢ IsUnit (absNorm I)

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
⊢ closure[inst✝¹] (S ∩ closedPoints X) = closure[inst✝¹] S

Tactic:
refine (closure_mono (Set.inter_subset_left)).antisymm ?_
  rw [IsClosed.closure_subset_iff isClosed_closure]
  intro x hx
  by_contra H
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := nonempty_inter_closedPoints (Z := S \ closure (S ∩ closedPoints X))
    ⟨x, hx, H⟩ (.inter hS isClosed_closure.isOpen_compl.isLocallyClosed)
  exact hy₂ (subset_closure ⟨hy₁, hy₃⟩)

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ DiscreteTopology X

Tactic:
have : closedPoints X = Set.univ := by
    rw [← Set.univ_subset_iff, ← closure_closedPoints,
      closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]
    exact h.isClosed_biUnion fun _ ↦ id

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
⊢ DiscreteTopology X
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_2
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
· let N := (Ring.jacobson R • ⊤ : Submodule R M).restrictScalars R₀
    have : Module.Finite R₀ N := by refine hs (h.imp ?_ ?_) <;> (intro; infer_instance)
    have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)
    exact .of_submodule_quotient N

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))
this : f '' closure[inst✝²] S ⊆ closure[inst✝¹] (f '' (S ∩ closedPoints X))
⊢ (f '' closure[inst✝²] S).Subsingleton

Tactic:
H₄.closure_eq

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
H₄ : IsClosed[inst✝¹] (f '' (S ∩ closedPoints X))
this : f '' closure[inst✝²] S ⊆ f '' (S ∩ closedPoints X)
⊢ (f '' closure[inst✝²] S).Subsingleton
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)

Goal state after:
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
this : ¬IsFiniteLength A M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)