mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rw [Ideal.mul_top] at h

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
⊢ (minpoly A x).natDegree ≤ ⊤.spanFinrank

Tactic:
by
  rcases LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero _ (Algebra.lmul A _ x) with
    ⟨f, f_monic, f_deg, f_aeval⟩
  refine f_deg ▸ (natDegree_le_natDegree <| minpoly.min _ _ f_monic ?_)
  rw [aeval_algHom_apply] at f_aeval
  exact Algebra.lmul_injective (R := A) <| by simpa using f_aeval

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ IsOpen (freeLocus R M)

Tactic:
by
  refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_
  have : Module.Free _ _ := hx
  obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)
  exact ⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩

Goal state after:
Module: Mathlib.GroupTheory.Solvable

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

Tactic:
rw [IsSimpleGroup.derivedSeries_succ] at hn
      intro a b
      rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
      exact subset_closure ⟨a, b, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : ⨆ x, adjoin F ((minpoly F x).rootSet L) = ⊤
⊢ L →ₐ[F] L'

Tactic:
rw [← gc.l_iSup] at this

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
⊢ L →ₐ[F] L'
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [normalClosure_le_iff] at h
    simpa only [fieldRange_val] using h K₁.val
  · rw [← normalClosure_of_normal K₂]
    exact normalClosure_mono K₁ K₂ h

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ Disjoint B B'

Tactic:
exact disjoint_of_subset_left hBI hIB'

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
by
  simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax
  refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_
  · obtain ⟨I', hII', hI', hne⟩ := hInotmax
    exact hne <| hIb.eq_of_subset_indep hII' hI'
  exact hB.1.isBase_of_maximal fun J hJ hBJ ↦ hB.2 hJ hBJ

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.IsBasis I (⋃ i, X i)

Tactic:
convert! IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _ <;> rw [iUnion_const]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case neg
α : 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 J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
⊢ False

Tactic:
have heI₀ : e ∉ I₀ := notMem_subset hI₀I heI

Goal state after:
case neg
α : 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 J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
hI' : M.IsBasis I' (R ∩ M.E)
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: case mpr
α : Type u_1
E I X : Set α
⊢ I = X ∧ X ⊆ E → (freeOn E).IsBasis I X

Tactic:
rintro ⟨rfl, hIE⟩

Goal state after:
case mpr
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).IsBasis I I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ (M.restrictSubtype M.E).IsBase B ↔ M.IsBase (Subtype.val '' B)

Tactic:
by
  rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]

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

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

pp: case neg
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
· simp [isLoop_iff_closure_eq_loops_and_mem_ground, he]

Goal state after:
case neg
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
rw [insert_inter_distrib, insert_union_distrib]

Goal state after:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X

Tactic:
by
  rw [setOfPred_isNonloop_eq, ← inter_sdiff_assoc, closure_sdiff_loops_eq, closure_inter_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, encard_ne_top_iff]
  exact ⟨fun h ↦ hB.rankFinite_of_finite h, fun h ↦ hB.finite⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.eRk {e} = 1 ↔ M.IsNonloop e

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.eRk_eq⟩
  rwa [← indep_singleton, indep_iff_eRk_eq_encard_of_finite (by simp), encard_singleton]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ X ⊆ M.closure X

Tactic:
simp [M.closure_def' X, subset_sInter_iff]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
hcon : ∀ e ∈ Y, e ∈ M.closure X
⊢ False

Tactic:
exact hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ¬M.IsColoop e
⊢ ∃ C, M.IsCircuit C ∧ e ∈ C

Tactic:
by
  simp only [isColoop_iff_forall_mem_isBase, not_forall, exists_prop] at he
  obtain ⟨B, hB, heB⟩ := he
  exact ⟨M.fundCircuit e B, hB.fundCircuit_isCircuit heE heB, .inl rfl⟩

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

Goal state before:
pp: case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)

Tactic:
hc

Goal state after:
case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₂.coloops)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I

Tactic:
exact hJI.subset

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ M.IsBasis I Y

Tactic:
refine hI.indep.isBasis_of_subset_of_subset_closure hY ?_

Goal state after:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure I
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree

Tactic:
rw [natDegree_expand]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX : M.Spanning X
⊢ M.Spanning I

Tactic:
hIX.spanning_iff_spanning

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX : M.Spanning X
⊢ M.Spanning X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case mp
α : 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
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
⊢ x ∈ I

Tactic:
rwa [← hfy]

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ u, s ⊆ u ∧ Maximal (fun x ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩

Goal state after:
case refine_1
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent R Subtype.val

case refine_2
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t
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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → Set.range x ⊆ s → Set.range x = s) ↔
    AlgebraicIndependent S x ∧ ∀ (s : Set A), AlgebraicIndepOn S _root_.id s → Set.range x ⊆ s → Set.range x = s

Tactic:
IsIntegral.algebraicIndependent_iff R S

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

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} #{ x // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
← ht.cardinalMk_eq_trdeg,

Goal state after:
R : Type u_1
S : Type v
A : Type w
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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} #{ x // x ∈ s } + lift.{v, w} #{ x // x ∈ t } = lift.{v, w} (trdeg R A)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ (fun x_1 ↦ x * x_1 * x⁻¹) ⁻¹' U

Tactic:
simp only [mul_inv_cancel_comm, preimage_id']

Goal state after:
G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ U
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
⊢ ∀ {x y : Set Gal(L/K)},
    x ∈ (fun g ↦ g.carrier) '' fixedByFinite K L →
      y ∈ (fun g ↦ g.carrier) '' fixedByFinite K L → ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L, z ⊆ x ∩ y

Tactic:
rintro _ _ ⟨_, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨_, ⟨E2, h_E2, rfl⟩, rfl⟩
    have : FiniteDimensional K E1 := h_E1
    have : FiniteDimensional K E2 := h_E2
    refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩
    exact Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)

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

Goal state before:
pp: case mpr
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
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ (minpoly R x).degree = 1

Tactic:
rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]

Goal state after:
case mpr
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
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ (map (algebraMap R K) (minpoly R x)).degree = 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ.refine_2
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
⊢ ((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:
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]

Goal state after:
case succ.refine_2
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
⊢ ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: K : Type v
inst✝² : Field K
k : Type u_1
inst✝¹ : CommSemiring k
inst✝ : IsSepClosed K
f : k →+* K
hf : Function.Injective ⇑f
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
x : K
hx : (map f p).IsRoot x
⊢ eval x (map f p) = 0

Tactic:
← IsRoot

Goal state after:
K : Type v
inst✝² : Field K
k : Type u_1
inst✝¹ : CommSemiring k
inst✝ : IsSepClosed K
f : k →+* K
hf : Function.Injective ⇑f
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
x : K
hx : (map f p).IsRoot x
⊢ (map f p).IsRoot x
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ (LinearMap.BilinForm.toMatrix b) (traceForm R S) i j = (trace R S) (b i * b j)

Tactic:
by
  rw [LinearMap.BilinForm.toMatrix_apply, traceForm_apply]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
val✝ : Fintype G
⊢ ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P

Tactic:
intro P Q hP hQ hPQ

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
⊢ ∃ g ∈ ⊤, Q ≤ g • P
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
⊢ IsIntegral R ((trace L F) x)

Tactic:
have hx' : IsIntegral L x := hx.tower_top
  rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]
  · refine (IsIntegral.multiset_sum ?_).nsmul _
    intro y hy
    rw [mem_roots_map (minpoly.ne_zero hx')] at hy
    use minpoly R x, minpoly.monic hx
    rw [← aeval_def] at hy ⊢
    exact minpoly.aeval_of_isScalarTower R x y hy
  · apply IsAlgClosed.splits

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
by
  have : (a.val : ℤ) - n ≤ 0 := by
    rw [sub_nonpos, Int.ofNat_le]
    exact a.val_le
  rw [valMinAbs_def_pos]
  split_ifs
  · rw [Int.natAbs_natCast, natCast_zmod_val]
  · rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]

Goal state after: