mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
h : MultilinearMap R t E
x✝ : (i : ι) → s i
⊢ ((lift h ∘ₗ map f).compMultilinearMap (tprod R)) x✝ = ((lift (h.compLinearMap f)).compMultilinearMap (tprod R)) x✝

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, Function.comp_apply,
    map_tprod, lift.tprod, MultilinearMap.compLinearMap_apply]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
⊢ Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal)

Tactic:
have hxN₂ : x ∈ N₂ := (le_sup_right.trans_eq hx'.symm) (mem_span_singleton_self x)

Goal state after:
case refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
⊢ x ≠ 0

Tactic:
intro hx

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx : x = 0
⊢ False
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✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
⊢ rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)

Tactic:
← e.finrank_eq,

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
⊢ rankAtStalk M p = finrank k (k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
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 α
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
let g := minpoly F β

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 β
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)

Tactic:
rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]

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
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = h
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ↑x * ∑ x, r ↑x • ↑x = ↑(LinearMap.id x)

Tactic:
(Finset.sum_coe_sort ..).trans hr.2,

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ↑x * 1 = ↑(LinearMap.id x)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ J, M.IsBasis J Y ∧ J ∩ X = I

Tactic:
refine ⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J ∩ X ⊆ I
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case left
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ ↑(e 1) ∈ I

pp: case right
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ ↑(e 1) ∈ J

Tactic:
exacts [mul_le_left (e 1).2, mul_le_right (e 1).2]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
rintro ⟨hI, I, rfl⟩
    exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
hI : M.Indep I
f : α ↪ β
⊢ (M.mapEmbedding f).Indep (⇑f '' I)

Tactic:
simpa [preimage_image_eq I f.injective]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)

Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
  rw [hI.eRk_eq_encard]
  rw [isBasis'_iff_isBasis_inter_ground, isBasis_restrict_iff', restrict_ground_eq] at hI
  rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ ?m.80

Tactic:
by simpa using h (M.E \ B) hB.compl_isBase_dual

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M.removeLoops.Indep I ↔ M.Indep I

Tactic:
removeLoops_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ (M ↾ {e | M.IsNonloop e}).Indep I ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e

Tactic:
removeLoops_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ (M ↾ {e | M.IsNonloop e}).IsNonloop e ↔ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ M.removeLoops ↾ X = M ↾ X

Tactic:
removeLoops_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ M ↾ {e | M.IsNonloop e} ↾ X = M ↾ X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M ↾ univ).removeLoops = M.removeLoops

Tactic:
removeLoops_eq_restrict,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M ↾ univ ↾ {e | (M ↾ univ).IsNonloop e} = M.removeLoops
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
suffices B \ B' ⊆ U by
    refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
    simp only [sup_le_iff, le_refl, true_and]
    exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B \ B' ⊆ U
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ lift.{v, u} #↑(I \ J) = lift.{v, u} #↑(J \ I)

Tactic:
← mk_image_eq_of_injOn_lift _ _ (hfI.mono sdiff_subset),

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ lift.{u, v} #↑(f '' (I \ J)) = lift.{v, u} #↑(J \ I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) = M.closure I

Tactic:
apply subset_antisymm <;> apply closure_subset_closure_of_subset_closure
  · simp only [subset_def, mem_sdiff, mem_insert_iff, mem_singleton_iff]
    rintro a (rfl | haI)
    exacts [hf, M.subset_closure _ hI.subset_ground haI]
  · intro a haI
    obtain rfl | ne := eq_or_ne a e
    exacts [he, M.mem_closure_of_mem' ⟨.inr haI, ne⟩ (hI.subset_ground haI)]

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

Goal state before:
pp: case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f

Tactic:
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
    exact ⟨g, hgs, n, hge⟩

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

Goal state before:
pp: case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = range w
⊢ Surjective j

Tactic:
← @image_univ _ _ w

Goal state after:
case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u, u} #ι = #ι'

Tactic:
lift_cardinalMk_eq hx hy,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u, u} #ι' = #ι'
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ (map (algebraMap F f.SplittingField) f).natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
natDegree_map

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (map (algebraMap F f.SplittingField) f).natDegree ≠ Zero.zero

Tactic:
natDegree_map

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natDegree ≠ Zero.zero
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
rintro x hf _ hg rfl

Goal state after:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
by
  classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]
  exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
    Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

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

Goal state before:
pp: ι : 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
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
by
  obtain rfl | ne := eq_or_ne j i
  · exact H₁
  have := H₁.of_isAlgebraic_adjoin_insert_sdiff {i}ᶜ i j v (.inr ne)
  rw [compl_eq_univ_sdiff, insert_sdiff_self_of_mem (mem_univ _), ← compl_eq_univ_sdiff] at this
  exact this H₂

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

Goal state before:
pp: case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ ib ∈ B', ∃ ia, (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa

Goal state after:
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: 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
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
a✝ : f ∈ ⊤
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩

Tactic:
rcases restrictNormalHom_surjective K f with ⟨σ, hσ⟩

Goal state after:
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
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
a✝ : f ∈ ⊤
σ : Gal(K/↥L)
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩
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]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
⊢ minpoly R s = P

Tactic:
apply eq_of_sub_eq_zero

Goal state after:
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]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
⊢ minpoly R s - P = 0
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
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ (minpolyDiv R x).coeff (i + ((minpolyDiv R x).natDegree + 1)) ∈ R[x]

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ 0 ∈ R[x]

R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: case intro.intro
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✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
⊢ ∑ i, ((leftMulMatrix b) (∑ i, ((leftMulMatrix c) x).diag i)).diag i =
    ∑ i ∈ Finset.univ ×ˢ Finset.univ, ((leftMulMatrix (b.smulTower c)) x).diag i

Tactic:
Finset.sum_product

Goal state after:
case intro.intro
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✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
⊢ ∑ i, ((leftMulMatrix b) (∑ i, ((leftMulMatrix c) x).diag i)).diag i =
    ∑ x_1, ∑ y, ((leftMulMatrix (b.smulTower c)) x).diag (x_1, y)
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
g : G
⊢ e (g • e.symm x') = e (e.symm x')

Tactic:
simp [he, hx']

Goal state after: