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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ Indep B

Tactic:
simpa using hB.indep

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∀ (I : Set β),
    (∃ t, ⇑f '' t = I) →
      (M.Indep ((fun x ↦ ↑(invFunOn (⇑f) univ x)) '' I) ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) I ↔
        M.Indep (Subtype.val '' ⇑f ⁻¹' I))

Tactic:
rintro _ ⟨I, rfl⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
I : Set ↑M.E
⊢ M.Indep ((fun x ↦ ↑(invFunOn (⇑f) univ x)) '' ⇑f '' I) ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) (⇑f '' I) ↔
    M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (M.map f hf).Indep (f '' I) ↔ M.Indep I

Tactic:
rw [map_indep_iff]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
⊢ M.IsFlat (⋂ i, Fs i)

Tactic:
by
  refine ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
    (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
  obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))
  refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)
  convert! hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ) using 1
  rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]
  exact fun hI ↦ ⟨fun h ↦ (M.closure_subset_ground _).antisymm h.2,
    fun h ↦ ⟨(M.subset_closure B).trans_eq h, h.symm.subset⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
aux : ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
h : f ∈ M.fundCircuit e B
⊢ f ∈ M✶.fundCocircuit e (M.E \ B)

Tactic:
by
      simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
⊢ ∃ x_1, (aeval Subtype.val) x_1 = (aeval x) p

Tactic:
refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
⊢ (aeval Subtype.val) ((rename (codRestrict x (range x) ⋯)) p) = (aeval x) p
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})

Tactic:
use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset sdiff_subset).subset ⟨he, heI⟩).2 rfl
  intro h
  obtain ⟨J, hJ⟩ := M.exists_isBasis I
  convert! hJ.indep
  refine hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)
  exact mem_of_mem_of_subset
    (hJ.subset_closure he) (M.closure_subset_closure (subset_sdiff_singleton hJ.subset heJ))

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

Goal state before:
pp: case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
⊢ False

Tactic:
obtain ⟨e, heI, heK⟩ := exists_of_ssubset hssu

Goal state after:
case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
convert! e.symm.isTranscendenceBasis hx; ext; simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

pp: case neg
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
· simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]

Goal state after:
case neg
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
mul_eq_zero,

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬(f = 0 ∨ g = 0)
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Module.rank F ↥(separableClosure F F) = 1

Tactic:
Subsingleton.elim (separableClosure F F) ⊥,

Goal state after:
F : Type u
inst✝ : Field F
⊢ Module.rank 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
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
have := expChar_of_injective_algebraMap (algebraMap F E).injective q
  have := expChar_of_injective_ringHom (C_injective (R := E)) q
  refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩
  · obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    have hx := congr_arg (Polynomial.aeval x) h.symm
    rw [minpoly.aeval, map_sub, map_pow, aeval_X, aeval_C, sub_eq_zero, eq_comm] at hx
    use n
    rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
  apply_fun constantCoeff at h
  simp_rw [map_pow, map_sub, constantCoeff_apply, coeff_map, coeff_X_zero, coeff_C_zero] at h
  rw [zero_sub, neg_pow, neg_one_pow_expChar_pow] at h
  exact ⟨n, -(minpoly F x).coeff 0, by rw [map_neg, h, neg_mul, one_mul, neg_neg]⟩

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∃ T, mulInvClosureNhd T W

Tactic:
rcases exist_mul_closure_nhds WClopen with ⟨S, Smemnhds, mulclose⟩

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
⊢ ∃ T, mulInvClosureNhd T W
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : (integerNormalization R⁰ p).content * ↑u = 0
⊢ False

Tactic:
mul_eq_zero,

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : (integerNormalization R⁰ p).content = 0 ∨ ↑u = 0
⊢ False
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x✝ x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ R[x]
⊢ R[x] = ⊤

Tactic:
exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
⊢ g ∈ lifts (algebraMap R K)

Tactic:
obtain ⟨b, hb₁, (hb₂ : g'.map _ = _)⟩ := integerNormalization_spec R⁰ g

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
⊢ g ∈ lifts (algebraMap R K)
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✝ : IsPurelyInseparable F E
⊢ insepDegree F E = Module.rank F E

Tactic:
rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']

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

Goal state before:
pp: case refine_2
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
g : G
x : A
y : B
⊢ (algebraMap B L) (g • x • y) = (algebraMap B L) (x • g • y)

pp: case refine_3
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
x : B
h : ∀ (g : G), g • x = x
⊢ ∃ a, (algebraMap A B) a = x

Tactic:
· simp [Algebra.smul_def, algebraMap.coe_smul', ← hc]

Goal state after:
case refine_3
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
x : B
h : ∀ (g : G), g • x = x
⊢ ∃ a, (algebraMap A B) a = x
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ¬IsField (𝓞 K)

Tactic:
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))
⊢ ¬IsField (𝓞 K)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑x.val - ↑(namedPattern k (n + 1) h✝¹)) = x

Tactic:
Int.cast_sub,

Goal state after:
case neg
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬x.val ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑x.val - ↑↑(namedPattern k (n + 1) h✝¹) = x
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑(x.valMinAbs - y) = 0

Tactic:
Int.cast_sub,

Goal state after:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑x.valMinAbs - ↑y = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ -↑(↑a.val - ↑n) = -a

Tactic:
Int.cast_sub,

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ -(↑↑a.val - ↑↑n) = -a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
by_cases h2a : 2 * a.val = n
  · rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
  · rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]

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

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf :
  (algebraMap B (B ⧸ Q)) b ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) *
      eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) =
    0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0

Tactic:
mul_eq_zero,

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf :
  (algebraMap B (B ⧸ Q)) b ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) = 0 ∨
    eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0
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
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    ∑ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)

Tactic:
rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x, ?f x

case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ -(a - eval b r) ∈ g • Q

Tactic:
neg_sub,

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b r - a ∈ g • Q
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
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
hx : IsSeparable K x
⊢ (trace K L) x = 0 x

Tactic:
lift x to separableClosure K L using hx

Goal state after:
case pos
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
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
⊢ (trace K L) ↑x = 0 ↑x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
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
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ n
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
cases n with

Goal state after: