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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})

Tactic:
rw [← insert_sdiff_singleton_comm (by rintro rfl; contradiction),
    (hI.sdiff _).insert_indep_iff_of_notMem (by simp [heI])]

Goal state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep (insert e (C \ {e})) ∨ e ∈ C \ {e}

Tactic:
insert_sdiff_singleton,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep (insert e C) ∨ e ∈ C \ {e}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e (C \ {e})

Tactic:
insert_sdiff_singleton,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X ∧ InjOn Subtype.val I ∧ I ⊆ X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

Tactic:
and_iff_right Subtype.val_injective.injOn,

Goal state after:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X ∧ I ⊆ X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i

Tactic:
insert_sdiff_singleton,

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z J ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).IsNonloop e ↔ M.IsNonloop (f e)

Tactic:
rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
    and_iff_left (injOn_singleton _ _)]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hIfin : I.Finite
h : M.eRank ≤ M.eRk I
⊢ M.IsBase I

Tactic:
by
  simpa using hI.isBasis_of_eRk_ge hIfin hI.subset_ground (M.eRk_ground.trans_le h)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.eRank = 0
⊢ M = loopyOn M.E

Tactic:
by simpa [eRank_eq_zero_iff] using h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (M.closure (B \ {e})) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t

Tactic:
closure_spanning_iff (sdiff_subset.trans hB.subset_ground)

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I

Tactic:
refine ⟨fun h _ ↦ h.closure_ssubset_closure,
    fun h ↦ (indep_iff_forall_notMem_closure_sdiff hI).2 fun e heI hecl ↦ ?_⟩

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.E ⊆ M.closure S

Tactic:
rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]

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

Goal state before:
pp: case inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

Tactic:
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]

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

Goal state before:
pp: 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'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
by
  nontriviality R
  rw [trdeg, lift_iSup bddAbove_of_small]
  refine ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <|
    of_comp f ?_)
  convert! i.2; simp [invFun_eq (hf _)]

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
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝³ : IsScalarTower (↥Rt) (↥St) A
this✝² : NoZeroDivisors ↥St
this✝¹ : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
this✝ : Nontrivial R
this : Nontrivial A
⊢ IsAlgebraic (↥Rt) y

Tactic:
exact adjoin_induction (fun _ h ↦ isAlgebraic_algebraMap (⟨_, subset_adjoin h⟩ : Rt))
      (fun z ↦ ((alg.1 z).algHom (IsScalarTower.toAlgHom R S A)).extendScalars fun _ _ eq ↦ by
        exact hx.algebraMap_injective congr($eq.1)) (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) hy

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
by
  rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]

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

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = s

Tactic:
Matroid.closure,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | (matroid R A).IsFlat F ∧ s ∩ (matroid R A).E ⊆ F} = s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
have : (insert i s).InjOn v := (injOn_insert hi).mpr ⟨inj, hi'⟩

Goal state after:
case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝³ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝² : Nontrivial S
this✝¹ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
· intro x₀
    rw [nhds_eq, nhds_one_eq]
    rfl

Goal state after:
case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
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✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ fixedField ⊤ = ⊥

Tactic:
← fixingSubgroup_bot,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ fixedField ⊥.fixingSubgroup = ⊥
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
this : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ ↑H ∈ 𝓝 x

Tactic:
simpa only [SetLike.mem_coe, Filter.mem_map',
    H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using! this hg

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
h_in_F : σ⁻¹ x ∈ F
⊢ g (σ⁻¹ x) = σ⁻¹ x

Tactic:
rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
g : Gal(L/K)
hg : ∀ x ∈ F, g x = x
x : L
hx : x ∈ E
h_in_F : σ⁻¹ x ∈ F
⊢ g (σ⁻¹ x) = σ⁻¹ x
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
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.IsSplittingField (↥L) E T'

Tactic:
rw [isSplittingField_iff_intermediateField] at hT₂ ⊢

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ (Polynomial.map (algebraMap (↥L) E) T').Splits ∧ adjoin (↥L) (T'.rootSet E) = ⊤
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)
⊢ False

Tactic:
e,

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : 0 * (X - C x) = map (algebraMap R S) (minpoly R x)
⊢ False
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case h
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
⊢ p = C p.leadingCoeff * minpoly R s

Tactic:
have ⟨q, hMul⟩ := isIntegrallyClosed_dvd hInt hp

Goal state after:
case h
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ p = C p.leadingCoeff * minpoly R s
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
⊢ IsIntegral R s ↔ C p.leadingCoeff ∣ p

Tactic:
refine ⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩
  · use minpoly R s
    have ⟨q, hMul⟩ := isIntegrallyClosed_dvd hInt hp
    suffices q.degree ≤ 0 by simp [degree_le_zero_iff.mp this ▸ hMul, minpoly.monic hInt, mul_comm]
    apply WithBot.le_of_add_le_add_left <| Polynomial.degree_ne_bot.mpr <| minpoly.ne_zero hInt
    convert! pmin _ (minpoly.monic hInt) (minpoly.aeval ..)
    · rw [hMul, degree_mul]
    · rw [add_zero]
  · convert! right_ne_zero_of_mul <| hMul ▸ h₀
    refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm
    · have := hMul ▸ leadingCoeff_mul .. |>.symm
      simp only [leadingCoeff_C, ne_eq, leadingCoeff_eq_zero, h₀, not_false_eq_true, mul_eq_left₀]
        at this
      exact this
    · have := congrArg (Polynomial.aeval s) hMul
      simp only [hp, h₀, map_mul, aeval_C, zero_eq_mul, FaithfulSMul.algebraMap_eq_zero_iff,
        leadingCoeff_eq_zero, false_or] at this
      exact this
    · exact (hMul ▸ degree_C_mul <| by simp [h₀]) ▸ pmin

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
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : c * d ≠ 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [Ne, ← C_eq_zero] at hcd0

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
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
⊢ IsUnit a ∨ IsUnit b
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 E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h

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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F ((algebraMap E K) x)).Separable
⊢ x ∈ (algebraMap F E).range
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✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
⊢ (minpoly F x).natDegree = q ^ m

Tactic:
e,

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
⊢ (X ^ q ^ m - C y).natDegree = q ^ m
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✝ : IsPurelyInseparable F E
x : E
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
obtain ⟨n, h⟩ := IsPurelyInseparable.minpoly_eq_X_sub_C_pow F (ringExpChar F) x

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
inst✝ : IsPurelyInseparable F E
x : E
n : ℕ
h : Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ ringExpChar F ^ n
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl.add
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
this : ExpChar (R ⊗[k] K) q
h : ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).rangeS
h' : ∃ n, y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).rangeS
⊢ ∃ n, (x + y) ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).rangeS

Tactic:
← Subalgebra.mem_perfectClosure_iff

Goal state after:
case inl.add
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
this : ExpChar (R ⊗[k] K) q
h : x ∈ Subalgebra.perfectClosure R (R ⊗[k] K) q
h' : y ∈ Subalgebra.perfectClosure R (R ⊗[k] K) q
⊢ x + y ∈ Subalgebra.perfectClosure R (R ⊗[k] K) q
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
⊢ x = 0

Tactic:
have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : (algebraMap K L) ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) x)
⊢ x = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Tactic:
· apply natAbs_valMinAbs_le

Goal state after:
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 : Finset L
b : Basis (↥s) K L
⊢ False

Tactic:
exact h₀ (Module.Finite.of_basis b)

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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝¹ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this✝ : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
e : g.natDegree = 0
this : g.natDegree * p ^ (n + 1) = (minpoly K x).natDegree
⊢ False

Tactic:
e,

Goal state after:
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
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this✝ : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
e : g.natDegree = 0
this : 0 * p ^ (n + 1) = (minpoly K x).natDegree
⊢ False