mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)

Tactic:
have h_root : h.eval β = 0 := by
    apply eval_gcd_eq_zero
    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
    · rw [eval_map_algebraMap, minpoly.aeval]

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
simp only [← heq] at αyβ_in_K

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
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 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
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ I₀ ⊆ I, I₀.Finite → Indep (insert e I₀)
⊢ False

Tactic:
refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_

Goal state after:
α : 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
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ I₀ ⊆ I, I₀.Finite → Indep (insert e I₀)
J : Set α
hJss : J ⊆ insert e I
hJfin : J.Finite
⊢ Indep J
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 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
⊢ ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
hImax

Goal state after:
α : 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
⊢ Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
by
  rw [isBasis_iff', and_iff_left hX]

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

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Goal state after:
α : Type u_1
⊢ (emptyOn α)✶.E = ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M = emptyOn α ∨ M.Nonempty

Tactic:
rw [← ground_eq_empty_iff]

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ∨ M.Nonempty
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Goal state after:
α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M.E = ∅
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ N.comap f ↾ f ⁻¹' N.E = N.comap f

Tactic:
restrict_eq_self_iff

Goal state after:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Tactic:
rw [← not_indep_iff (by simpa [← image_insert_eq] using image_mono hss)]

Goal state after:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ (M.mapEmbedding f).IsBase (⇑f '' B)

Tactic:
by
  rw [Matroid.mapEmbedding, map_isBase_iff]
  exact ⟨B, hB, rfl⟩

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ (N.restrictSubtype M.E).Indep (M.E ↓∩ I) ↔ N.Indep I

Tactic:
restrictSubtype_indep_iff_of_subset

Goal state after:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ N.Indep I ↔ N.Indep I

α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ (f '' I).encard = I.encard

Tactic:
(hf.mono hI.indep.subset_ground).encard_image

Goal state after:
α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ I.encard = I.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ Disjoint (B ∩ X) (M.E \ B)

Tactic:
tauto_set

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ Disjoint (M.E \ B ∩ (M.E \ X)) X

Tactic:
tauto_set

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ B ∩ X ∪ M.E \ B = M.E \ B ∩ (M.E \ X) ∪ X

Tactic:
tauto_set

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.closure I = {x | M.IsBasis I (insert x I)}

Tactic:
by
  set F := {x | M.IsBasis I (insert x I)}
  have hIF : M.IsBasis I F := hI.isBasis_setOfPred_insert_isBasis
  have hF : M.IsFlat F := by
    refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
    exact (hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
      (hIF.subset.trans subset_union_right)).isBasis_subset (subset_insert _ _)
      (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
  rw [subset_antisymm_iff, closure_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
  · rintro F' ⟨hF', hIF'⟩ e (he : M.IsBasis I (insert e I))
    rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
    obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset hIF' hF'.2
    exact (hF'.1 hJ (he.isBasis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))
  exact ⟨hF, inter_subset_left.trans hIF.subset⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite

Tactic:
rwa [← hC.eq_of_not_indep_subset hJ hJC]

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

Goal state before:
pp: case inl
α : 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
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops

Tactic:
exact ⟨disjoint_of_subset_left sdiff_subset hdj, disjoint_sdiff_left⟩

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ ¬IsAlgebraic R ((Polynomial.aeval (X i)) f)

Tactic:
← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
    Function.injective_id (by ext1; rfl),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ ¬IsAlgebraic (↥(supported R ∅)) ((RingHom.id (MvPolynomial σ R)) ((Polynomial.aeval (X i)) f))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩

Goal state after:
case refine_1
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.IsBase B

case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
by rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]

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

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

Tactic:
hI'.indep.mem_closure_iff',

Goal state after:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ (M ↾ R).E ∧ ((M ↾ R).Indep (insert e I) → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E
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.comap f).Indep (insert x I) → x ∈ I) ↔ f x ∈ M.closure (f '' I)

Tactic:
hI'.indep.mem_closure_iff',

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 : α),
    f x ∈ M.E ∧ ((M.comap f).Indep (insert x I) → x ∈ I) ↔ f x ∈ M.E ∧ (M.Indep (insert (f x) (f '' I)) → f x ∈ f '' I)
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ trdeg R A' ≤ trdeg R A

Tactic:
rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]; exact lift_trdeg_le_of_surjective f hf

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 α
g : G
a : α
h : ∀ (j : ℤ), a ∈ fixedBy α (g ^ j)
⊢ a ∈ fixedBy α g

Tactic:
simpa using h 1

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

Goal state before:
pp: case inl.ha
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R s)) a

Tactic:
apply is_transcendental_of_subsingleton

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

Goal state before:
pp: case inl.hb
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R t)) a

Tactic:
apply is_transcendental_of_subsingleton

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
x : F
n : ℕ
⊢ ((X - C x) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X_sub_C]

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

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

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

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
⊢ ∀ (x₀ : Gal(L/K)) {U : Set Gal(L/K)},
    U ∈ (galBasis K L).sets → ∃ V ∈ (galBasis K L).sets, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩

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
⊢ ∃ V ∈ (galBasis K L).sets, V ⊆ (fun x ↦ σ * x * σ⁻¹) ⁻¹' (fun g ↦ g.carrier) E.fixingSubgroup
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
⊢ ↑{ toSubgroup := S, isOpen' := this } ⊆ W

Tactic:
have (n : ℕ) : V ^ (n + 1) ⊆ W * V ^ (n + 1) := by
    intro x xin
    rw [Set.mem_mul]
    use 1, einW, x, xin
    rw [one_mul]

Goal state after:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this✝ : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
this : ∀ (n : ℕ), V ^ (n + 1) ⊆ W * V ^ (n + 1)
⊢ ↑{ toSubgroup := S, isOpen' := this✝ } ⊆ W
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ (if j = i then (algebraMap R S) (f j) else (algebraMap R S) (f j) * 0) ∈ 1

Tactic:
mul_zero,

Goal state after:
case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ (if j = i then (algebraMap R S) (f j) else 0) ∈ 1
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
K : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)

Tactic:
by
  let L := FractionRing S
  rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]

Goal state after:
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
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ p.leadingCoeff ≠ 0

Tactic:
by simp [h₀]

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✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
⊢ IsUnit p

Tactic:
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
  obtain ⟨c, c0, hc⟩ := integerNormalization_spec R⁰ p
  rw [Algebra.smul_def, algebraMap_apply] at hc
  apply isUnit_of_mul_isUnit_right
  rw [← hc, (integerNormalization R⁰ p).eq_C_content_mul_primPart, ← hu, ← map_mul, isUnit_iff]
  refine
    ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => ?_,
      by simp⟩
  replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ con
  rw [mul_eq_zero, content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff] at con
  rcases con with (con | con)
  · apply h0 con
  · apply Units.ne_zero _ con

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ∃ s, Nonempty (Basis (↥s) R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

Tactic:
rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]

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

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) := ⋯
f : ↥L → IntermediateField k K := ⋯
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
⊢ ⨆ l, f l ≤ L

Tactic:
apply iSup_le
        intro l
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l.1}),
          fixedField_fixingSubgroup L] using inf_le_left

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
p : S × T
⊢ (trace R (S × T)) p = ((trace R S).coprod (trace R T)) p

Tactic:
rw [coprod_apply, trace_prod_apply]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) = of fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))

Tactic:
by
  ext; rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]

Goal state after: