mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝ : Nontrivial R
⊢ Free R M

Tactic:
obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
⊢ Free R M
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
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Algebra.lmul A B) ((Polynomial.aeval x) f) = 0
⊢ (Algebra.lmul A B) ((Polynomial.aeval x) f) = (Algebra.lmul A B) 0

Tactic:
by simpa using f_aeval

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ IsSolvable ↥H

Tactic:
· obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
    use n + 1
    rw [← map_subtype_inj, Subgroup.map_bot] at hn ⊢
    rw [← hn]
    clear hn
    induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ 0) = _root_.commutator G

Tactic:
exact derivedSeries_one G

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
⊢ Nonempty (Fin 5 ↪ X)

Tactic:
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ AlgebraicIndependent R x

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x
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, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑m

Tactic:
refine ⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩

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, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
⊢ m.range = ⊤
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Tactic:
exact hI' hB'

Goal state after:
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
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₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ f ⟨x, ⋯⟩ ⊆ iUnion f

Tactic:
apply subset_iUnion

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ M₁ = M₂

Tactic:
rw [h', restrict_ground_eq] at hR

Goal state after:
α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ M₁ = M₂
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N = M ∨ N <r M

Tactic:
simpa using eq_or_lt_of_le (ofMatroid_le_iff.2 h)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I R : Set α
hI : (M ↾ R).Indep I
⊢ M.Indep I

Tactic:
exact hI.of_restrict

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.IsCircuit ∅
⊢ False

Tactic:
by simpa using h.nonempty

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x ↦ ¬M.Indep x) C

Tactic:
by
  simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]
  exact fun ⦃t⦄ a ↦ ssubset_indep hC a

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Tactic:
refine ⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩
  simp_rw [isCircuit_iff, restrict_dep_iff, and_imp, dep_iff]
  exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finitary

Tactic:
by
  refine ⟨fun I hI ↦ ?_⟩
  simp only [map_indep_iff]
  have h' : I ⊆ f '' M.E := by
    intro e he
    obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
    exact image_mono hI₀.subset_ground <| h_eq.subset rfl
  obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'
  refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩
  specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)
  rwa [map_image_indep_iff (hJ₀I₀.trans hI₀E)] at hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)

Tactic:
eRk_union_closure_left_eq

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I.encard ≤ M.eRank

Tactic:
← hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRank
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_3
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ z ∉ range x

Tactic:
rintro ⟨i, hi, rfl⟩
    exact hzC _ (h_mem i)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ M.Dep X

Tactic:
rw [← not_indep_iff, indep_iff_eRk_eq_encard_of_finite hX]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ ¬M.eRk X = X.encard
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ I ∩ f '' X = I

Tactic:
inter_eq_self_of_subset_left hIX.subset

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ I = I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
by
  have := hA.coe_sort
  convert! closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa) <;>
  simp

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
⊢ AlgebraicIndependent R (⇑f ∘ x)

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I

Tactic:
subst hef

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e 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
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R Subtype.val

Tactic:
let f : t.map (Embedding.subtype (· ∈ s)) → s := fun x =>
    ⟨x.1, by
      obtain ⟨x, h⟩ := x
      rw [Finset.mem_map] at h
      obtain ⟨a, _, rfl⟩ := h
      simp only [Subtype.coe_prop, Embedding.coe_subtype]⟩
  convert! AlgebraicIndependent.comp li f _
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  rw [Finset.mem_map] at hx hy
  obtain ⟨a, _, rfl⟩ := hx
  obtain ⟨b, _, rfl⟩ := hy
  simp only [f, imp_self, Subtype.mk_eq_mk]

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

Goal state before:
pp: case mpr
α : 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
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : (M.map f hf).Indep (f '' insert x I)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)

Tactic:
map_image_indep_iff (insert_subset hxE hI.subset_ground)

Goal state after:
case mpr
α : 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
hxi : M.Indep (insert x I) → x ∈ I
J : Set α
hJI : insert (f x) (f '' I) = f '' J
hJ : M.Indep (insert x I)
hrw : f '' insert x I = f '' J
⊢ M.Indep (insert x I)
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✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Nat.card Gal(E/F) = finrank F E

Tactic:
obtain ⟨α, hα⟩ := Field.exists_primitive_element F E

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
⊢ Nat.card Gal(E/F) = finrank F E
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✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
⊢ False

Tactic:
obtain ⟨K, h₁, h₂⟩ := exists_lt_finrank_of_infinite_dimensional H (Nat.card Gal(E/F))

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✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
⊢ False
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
⊢ ⊤.fixingSubgroup = ⊥

Tactic:
ext
  simp [DFunLike.ext_iff]

Goal state after:
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✝
H : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
⊢ E.fixingSubgroup.Normal

Tactic:
apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)

Goal state after:
F : Type u_1
inst✝⁷ : Field F
E✝ : Type u_2
inst✝⁶ : Field E✝
inst✝⁵ : Algebra F E✝
H : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
σ : Gal(L/K)
⊢ MulAut.conj σ • E.fixingSubgroup = E.fixingSubgroup
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
i : ι
hi : p i
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i

Tactic:
exact hsmul_right m₀ hi

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable F ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
change Algebra.IsSeparable F (restrictScalars F E'⟮x⟯) at this

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✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable F ↥(IntermediateField.restrictScalars F (↥E')⟮x⟯)
⊢ IsSeparable F x
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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ IsUnit (C g.leadingCoeff⁻¹)

Tactic:
exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit

Goal state after:
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 : ι
⊢ (B ((B.dualBasis hB b) i)) (f j • b j) ∈ 1

Tactic:
rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]

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 : ι
⊢ (algebraMap R S) (f j) • (B ((B.dualBasis hB b) i)) (b j) ∈ 1
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:
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.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
h : Irreducible f := UniqueFactorizationMonoid.irreducible_of_factor f hf
⊢ f.Splits

Tactic:
obtain ⟨x, hx⟩ := H f h (hp.of_dvd (UniqueFactorizationMonoid.dvd_of_mem_factors hf))

Goal state after:
case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
h : Irreducible f := UniqueFactorizationMonoid.irreducible_of_factor f hf
x : k
hx : eval x f = 0
⊢ f.Splits
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (charpoly G b) = 0

Tactic:
rw [charpoly_eq, eval_prod]

Goal state after:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ ∏ j, eval b (X - C (j • b)) = 0
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
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ eval b (map (algebraMap A B) p) = 0

Tactic:
hp1,

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
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ eval b (charpoly G b) = 0
Module: Mathlib.Data.ZMod.ValMinAbs

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

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

Tactic:
· rw [Int.natAbs_natCast, natCast_zmod_val]

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