mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.Spanning (M.E \ X)

Tactic:
by
    refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (sdiff_subset.trans hB.subset_ground)).trans ?_
    rw [subset_sdiff, and_iff_left hXss.2.symm]
    apply closure_subset_ground

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
⊢ e ∈ M.fundCocircuit f B → f ∈ M.fundCircuit e B

Tactic:
he

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
this : Finsupp.linearCombination R x = (aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X
⊢ Injective ⇑(Finsupp.linearCombination R X)

Tactic:
← linearIndependent_iff_injective_finsuppLinearCombination

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
this : Finsupp.linearCombination R x = (aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X
⊢ LinearIndependent R X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
⊢ M.closure (I \ X) ⊂ M.closure I

Tactic:
refine hI.closure_ssubset_closure <| sdiff_subset.ssubset_of_ne fun h ↦ ?_
  rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h
  simp [h] at hX

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Minimal M.Spanning B

Tactic:
minimal_subset_iff

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : IsTranscendenceBasis R x
h✝ : Subsingleton R
⊢ IsTranscendenceBasis R Subtype.val

case inr
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : IsTranscendenceBasis R x
h✝ : Nontrivial R
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
  obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)
  exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsAlgebraic F x
x : E
h : x ∈ L
⊢ x ∈ algebraicClosure F E

Tactic:
simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
    Algebra.algebraMap_self, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩

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
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g

Tactic:
by
  rw [← fixedBy_inv]
  ext x
  rw [Set.mem_inv_smul_set_iff]
  refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩
  rw [← fixedBy_inv] at s_ss_fixedBy
  rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs

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 = w '' univ
⊢ Surjective j

Tactic:
exact range_eq_univ.mp (image_injective.mpr i'.injective p)

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

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
⊢ IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Subsingleton R
⊢ IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))

case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
⊢ IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
⊢ IsTranscendenceBasis R Subtype.val

case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
⊢ IsTranscendenceBasis R Subtype.val
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
i : E ≃ₐ[F] K
⊢ AlgebraicClosure K ≃ₐ[F] AlgebraicClosure E

Tactic:
let _ : Algebra E K := i.toAlgHom.toRingHom.toAlgebra

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
i : E ≃ₐ[F] K
x✝ : Algebra E K := (↑i).toAlgebra
⊢ AlgebraicClosure K ≃ₐ[F] AlgebraicClosure E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ rootOfSplits ⋯ ⋯ ∈ (f.aroots f.SplittingField).toFinset

Tactic:
rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
mul_eq_zero

Goal state after:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
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)
inst✝ : FiniteDimensional F E
⊢ finrank (↥(fixedField H)) E = Nat.card ↥H

Tactic:
by
  have := Fintype.ofFinite H
  rw [Nat.card_eq_fintype_card]
  exact FixedPoints.finrank_eq_card H E

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃ V ∈ 𝓝 0,
        ∃
          W ∈
            (have this := default;
              this).sets,
          V • W ⊆ U

Tactic:
by
        rintro U (rfl : U ∈ {{(0 : M)}})
        use univ, univ_mem, {0}, rfl
        rintro a ⟨x, -, m, rfl, rfl⟩
        simp only [smul_zero, mem_singleton_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
x₀ : R
U : Set M
h : U ∈ {{0}}
⊢ ∃
    V ∈
      (have this := default;
        this).sets,
    V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Tactic:
mem_singleton_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
x₀ : R
U : Set M
h : U = {0}
⊢ ∃
    V ∈
      (have this := default;
        this).sets,
    V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∃ T ∈ 𝓝 1, W * T ⊆ W

Tactic:
by
  apply WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
    ⟨Set.univ, by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
    (fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
    fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦ ⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
      rw [union_mul]
      exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
        (mul_subset_mul_left inter_subset_right |>.trans mem2) ⟩
  intro x memW
  have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]
  rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
    ⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩
  have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))
  exact ⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩,
    V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦ h6 ((mul_subset_mul_right inter_subset_left) a)⟩

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

Goal state before:
pp: 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))
⊢ ∃ H, ↑H ⊆ W

Tactic:
use ⟨S, this⟩

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 := ⋯
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
⊢ ↑{ toSubgroup := S, isOpen' := this } ⊆ W
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsOpen ↑H

Tactic:
by
  rw [← QuotientGroup.t1Space_iff] at h
  rw [← QuotientGroup.discreteTopology_iff]
  infer_instance

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

Goal state before:
pp: case h.right
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ IsOpen (σ • ↑(adjoin k {y}).fixingSubgroup) ∧ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Tactic:
· simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
      use 1
      simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

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

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : Gal(K/k)
hσ : σ ∈ H
⊢ σ x = x

Tactic:
have : ((restrictNormalHom L σ) ⟨x, xL⟩).1 = x := by rw [h σ hσ]

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : Gal(K/k)
hσ : σ ∈ H
this : ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x
⊢ σ x = x
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
h : n = 0
⊢ False

Tactic:
rw [h, Nat.cast_zero] at hn
    exact hn.out rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

case inr
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
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✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
⊢ finrank (↥F⟮x⟯) E < d

Tactic:
rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
⊢ 1 < q ^ m
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
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ^ p ^ 0 ∈ (algebraMap R A).rangeS

Tactic:
rw [pow_zero, pow_one]; exact ⟨x, rfl⟩

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

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = (X - C 0) ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X - C 0 ∣ q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
rw [map_zero, sub_zero] at hq hq0

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
h✝ : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
h : ¬0 ≤ a.valMinAbs * ?m.102
⊢ False

pp: n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ 0 < ?m.102

pp: n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ ℤ

Tactic:
he

Goal state after:
n : ℕ
a : ZMod (n + 1)
h✝ : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
h : ¬0 ≤ ↑(n + 1)
⊢ False

n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ 0 < 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs * 2 - y * 2| < ↑n * 2

Tactic:
abs_lt

Goal state after:
case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs = y

Tactic:
by
    rw [← sub_eq_zero]
    apply @Int.eq_zero_of_abs_lt_dvd n
    · rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
    rw [← mul_lt_mul_iff_left₀ (@zero_lt_two ℤ _ _ _ _ _)]
    nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
    rw [← abs_mul, sub_mul, abs_lt]
    constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ p.Coprime q

Tactic:
Nat.coprime_primes hp.1 hq.1

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ p ≠ q
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
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ ∑ σ, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ, σ pb.gen

Tactic:
have : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F

Goal state after:
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 L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝ : FiniteDimensional L F
this : Algebra.IsSeparable L F
⊢ ∑ σ, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ, σ pb.gen
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
H : ¬Algebra.IsSeparable K L
⊢ trace K L = 0

Tactic:
obtain ⟨p, hp⟩ := ExpChar.exists K

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
⊢ trace K L = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos.succ.prime
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar✝ : CharP K p
⊢ ↑p * (trace K ↥(separableClosure K L)) (p ^ n • x) = 0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
CharP.cast_eq_zero,

Goal state after:
case pos.succ.prime
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar✝ : CharP K p
⊢ 0 * (trace K ↥(separableClosure K L)) (p ^ n • x) = 0 ((algebraMap (↥(separableClosure K L)) L) x)