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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
⊢ ∀ (x : A) (y : ↥(submoduleAlgebra e)),
    (LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype) (x ⊗ₜ[R] y) =
      (AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e) (x ⊗ₜ[R] y)

Tactic:
intro a x

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x✝ : A ⊗[R] ↥(submoduleAlgebra e)
a : A
x : ↥(submoduleAlgebra e)
⊢ (LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype) (a ⊗ₜ[R] x) =
    (AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e) (a ⊗ₜ[R] x)
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ M✶.Indep (M.E \ (B ∪ R ∩ M.E))

Tactic:
rw [dual_indep_iff_exists]

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
⊢ ∃ B_1, M.IsBase B_1 ∧ Disjoint (M.E \ (B ∪ R ∩ M.E)) B_1
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case h.refine_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint (insert e I) B''

Tactic:
rw [← union_singleton, disjoint_union_left, disjoint_singleton_left, and_iff_left heB'']

Goal state after:
case h.refine_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint I B''
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ Maximal M✶.Indep B ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
maximal_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
    Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary

Tactic:
refine ⟨fun K hK ↦ ?_⟩

Goal state after:
α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → (uniqueBaseOn I E).Indep J
⊢ (uniqueBaseOn I E).Indep K
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

Tactic:
rw [dual_indep_iff_exists]

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ ∃ B_1, M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)

Tactic:
rw [eq_loopyOn_iff]; aesop

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
⊢ N.Dep (insert e (f '' I))

Tactic:
obtain ⟨⟨e, heX, rfl⟩, he⟩ := he

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ N.Dep (insert (f e) (f '' I))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Tactic:
by
  obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])
  simp only [mem_sdiff, Finset.mem_coe] at hx
  exact ⟨x, hx.1, hx.2, hxI⟩

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

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

Tactic:
hf.image_eq_image_iff hI hI'.subset_ground

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ¬M.Indep C ∧ ∀ ⦃t : Set α⦄, t ⊂ C → ¬¬M.Indep t

Tactic:
and_iff_right hC.not_indep,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → ¬¬M.Indep t
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.map id ⋯ = M

Tactic:
simp [ext_iff_indep]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set ↑(Iic M.E)
hs : ∀ a ∈ s, M.IsFlat ↑a
⊢ M.IsFlat ↑(sInf s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty
    · simp
    have _ := hne.coe_sort
    convert! IsFlat.iInter (M := M) (Fs := fun (F : s) ↦ F.1.1) (fun F ↦ hs F.1 F.2)
    ext
    aesop

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

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
simp [isColoop_iff_forall_notMem_isCircuit, he]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I

Tactic:
rw [← M.closure_closure I, h.indep.closure_eq_setOfPred_isBasis_insert]

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure {x | M.IsBasis I (insert x I)}
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst✝ : M.InvariantCardinalRank
⊢ (M ↾ X).InvariantCardinalRank

Tactic:
by
  refine ⟨fun I J Y hI hJ ↦ ?_⟩
  rw [isBasis_restrict_iff'] at hI hJ
  exact hI.1.cardinalMk_sdiff_comm hJ.1

Goal state after:
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' : e ∉ M.closure (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ False

Tactic:
hiI.notMem_closure_iff_of_notMem (notMem_subset hiX heEI.2)

Goal state after:
α : 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
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
show I = insert e (I \ {e}) by simp [heI]

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_2
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
⊢ M.Indep (I ∪ J)

Tactic:
obtain ⟨K, hKIJ, hK⟩ := hI.subset_isBasis_of_subset (show I ⊆ I ∪ J from subset_union_left)

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
⊢ M.Indep (I ∪ J)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ (I ∪ J) \ I

Tactic:
exact ⟨heI, notMem_subset hK heK⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)

Tactic:
rw [coindep_iff_exists, spanning_iff_exists_isBase_subset]

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 α
s : Set α
g : G
⊢ (∀ (x : α), x ∈ s ↔ g • x ∈ s) ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
Iff.comm

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 α
inst✝ : FaithfulSMul G α
g h : G
ne_one : g ≠ 1
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
⊢ ¬Commute g h

Tactic:
by
  contrapose ne_one with comm
  rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ natSepDegree 0 = 0

Tactic:
← C_0,

Goal state after:
F : Type u
inst✝ : Field F
⊢ (C 0).natSepDegree = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

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

Tactic:
· exact ⟨his, ne⟩

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

Goal state before:
pp: case refine_1
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)

Tactic:
have h2 : g.natDegree = 1 := by
      rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h

Goal state after:
case refine_1
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
h' : ¬IsIntegral F x
⊢ False

Tactic:
simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this✝ : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K

Tactic:
exact insepDegree_top_le_insepDegree_of_isScalarTower _ _ _

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

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

Tactic:
IntermediateField.mem_fixingSubgroup_iff F g

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
g : Gal(L/K)
hg : ∀ x ∈ F, g x = x
x : L
hx : x ∈ E
h_in_F : σ⁻¹ x ∈ F
⊢ g (σ⁻¹ x) = σ⁻¹ x
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : a ∈ (map (algebraMap K g.SplittingField) g).roots
⊢ a ∈ (map (algebraMap R g.SplittingField) f).roots

Tactic:
IsScalarTower.algebraMap_eq R K _,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : a ∈ (map (algebraMap K g.SplittingField) g).roots
⊢ a ∈ (map ((algebraMap K g.SplittingField).comp (algebraMap R K)) f).roots
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
⊢ eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((aeval x) (derivative (minpoly R x))) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = σ ((aeval x) (derivative (minpoly R x)))

case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F x).Separable
⊢ x ∈ (algebraMap F E).range

Tactic:
← minpoly.algebraMap_eq (algebraMap E K).injective

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F ((algebraMap E K) x)).Separable
⊢ x ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
⊢ IsPurelyInseparable F E

Tactic:
rw [isPurelyInseparable_iff_finSepDegree_eq_one, finSepDegree, Nat.card_eq_one_iff_unique]

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
have := congr_arg Cardinal.toNat (sepDegree_mul_insepDegree F E)
    rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this

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

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (adjoin.powerBasis hx).gen).aroots F).sum = ((minpoly K x).aroots F).sum

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x))).aroots F).sum = ((minpoly K x).aroots F).sum
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen)).Splits

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x)))).Splits
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.val ≤ n / 2
⊢ 0 ≤ ↑x.val ↔ x.val ≤ n / 2

case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ ↑x.val - ↑n ↔ x.val ≤ n / 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑x.val * 2 ≤ ↑n then ↑x.val else ↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    (algebraMap L (AlgebraicClosure L)) (∑ σ, σ x)

Tactic:
_root_.map_sum (algebraMap L (AlgebraicClosure L))

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    ∑ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L

Tactic:
exact (FixedPoints.finrank_eq_card G L).symm

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

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1

Tactic:
rw [← Fintype.card_units, pow_card_eq_one]

Goal state after:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1