mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (φ '' ↑s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Tactic:
← s.coe_image

Goal state after:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n ↑(Finset.image φ s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤

Tactic:
refine ENat.eq_top_iff_forall_gt.mpr fun k ↦ ?_
    specialize h (k + 1)
    obtain ⟨s, s_net, s_card⟩ := h
    apply s_net.card_le_netMaxcard.trans_lt'
    rw [Nat.cast_lt]
    exact (lt_add_one k).trans_le s_card

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone fun F ↦ coverEntropyInfEntourage T F U

Tactic:
refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : IsTopologicallyTransitive M α
U : Set α
hUo : IsOpen U
hUne : U.Nonempty
hUinv : ∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U
⊢ ⋃ m, (fun x ↦ m • x) ⁻¹' U ⊆ U

Tactic:
by simpa only [iUnion_subset_iff]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = (τ * σ) a

Tactic:
τ.mul_apply,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ (σ a)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 + μ.withDensity (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).2

Tactic:
by simpa using mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (τ b) = (τ * σ) b

Tactic:
τ.mul_apply,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (τ b) = τ (σ b)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
⊢ Function.LeftInverse varsToConstants constantsToVars

Tactic:
intro t
    induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f✝) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f✝
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f✝.all) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f✝.all

Tactic:
simp [mapTermRel, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) f✝ = f✝
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) f✝.all = f✝.all

Tactic:
simp [mapTermRel, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)

Tactic:
refine fun m a => funext (Fin.reverseInduction ?_ fun i _ => ?_)

Goal state after:
case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
m : (a : α) → M a
a : α
⊢ Fin.snoc v m (Fin.last k) a = Fin.snoc (fun i ↦ v i a) (m a) (Fin.last k)

case refine_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
m : (a : α) → M a
a : α
i : Fin k
x✝ : Fin.snoc v m i.succ a = Fin.snoc (fun i ↦ v i a) (m a) i.succ
⊢ Fin.snoc v m i.castSucc a = Fin.snoc (fun i ↦ v i a) (m a) i.castSucc
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
xs : Fin (k + n) → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ natAdd k)

Tactic:
induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel, Realize, h1]
  | rel => simp [mapTermRel, Realize, h1, h2]
  | imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
  | all _ ih => simp [mapTermRel, Realize, ih, hv]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
⊢ funMap fn x ∈ {x | f x = g x}

Tactic:
have h : f ∘ x = g ∘ x := by
      ext
      repeat' rw [Function.comp_apply]
      apply hx

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
h : ⇑f ∘ x = ⇑g ∘ x
⊢ funMap fn x ∈ {x | f x = g x}
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S

Tactic:
simp only [Hom.mem_range, Embedding.coe_toHom, coe_subtype]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
have h' : ∀ a,
        A.Definable L { x : α → M | x a = x (rangeSplitting f (rangeFactorization f a)) } := by
          refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
          simp

Goal state after:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
a : α
as : a ∈ s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ s → (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) x₂ → a = x₂

Tactic:
b

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
a : α
as : a ∈ s
b : α
⊢ b ∈ s → (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b → a = b
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: R : Type u
X : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Cardinal.lift.{u, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))

Tactic:
FreeMonoid

Goal state after:
R : Type u
X : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Cardinal.lift.{u, v} (Cardinal.mk (List X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ 2 ≤ finSepDegree ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Tactic:
finSepDegree_eq_finrank_of_isSeparable,

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ 2 ≤ finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).1 + (s, z).1,
      (⇑(frobenius K p))^[(s, z).1]
          ((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).2 *
        (⇑(frobenius K
                p))^[((m, x).1 + (n, y).1,
                (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).1]
          (s, z).2) =
    ((m, x).1 +
        ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).1,
      (⇑(frobenius K
                p))^[((n, y).1 + (s, z).1,
                (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).1]
          (m, x).2 *
        (⇑(frobenius K p))^[(m, x).1]
          ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).2)

Tactic:
simp only [mul_assoc, iterate_map_mul, ← iterate_add_apply,
              add_comm, add_left_comm]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
⊢ Irreducible (X ^ n - C (AdjoinSimple.gen K x))

Tactic:
have : IsIntegral K x := not_not.mp fun h ↦ by
      simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
        WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
⊢ Irreducible (X ^ n - C (AdjoinSimple.gen K x))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
⊢ ∀ (b : ↥K⟮x⟯), b ^ q ≠ AdjoinSimple.gen K x

Tactic:
b

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
⊢ b ^ q ≠ AdjoinSimple.gen K x
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
⊢ (toSubmodule A).rTensorOne (1 ⊗ₜ[R] 1) = 1

Tactic:
· exact Submodule.rTensorOne_tmul_one _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case e'_2
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ (algebraMap R[X] B) X = b

Tactic:
exact aeval_X _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case e'_3
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ (algebraMap R[X] A) X = a

Tactic:
exact aeval_X _

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ (↑↑(iterateFrobenius K L p hn)).toFun (r • a) =
    (_root_.iterateFrobenius F p n) r • (↑↑(iterateFrobenius K L p hn)).toFun a

Tactic:
by
    dsimp [iterateFrobenius]
    rw [Algebra.smul_def _ (iterateFrobeniusAux K L p n a)]
    apply (algebraMap K L).injective
    rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

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
L1 L2 : IntermediateField F E
h1 : IsPurelyInseparable F ↥L1
h2 : IsPurelyInseparable F ↥L2
⊢ IsPurelyInseparable F ↥(L1 ⊔ L2)

Tactic:
rw [← le_perfectClosure_iff] at h1 h2 ⊢
  exact sup_le h1 h2

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = b (f x✝) ^ q ^ n

Tactic:
b

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = (Basis.extend h') (f x✝) ^ q ^ n
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ map f (comap f A) ⊓ map f B = A ⊓ map f B

Tactic:
map_comap_eq,

Goal state after:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ A ⊓ f.fieldRange ⊓ map f B = A ⊓ map f B
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
| lift.{w, v} ((map f (comap f A)).relrank (map f (comap f B)))

Tactic:
map_comap_eq,

Goal state after:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
| lift.{w, v} ((A ⊓ f.fieldRange).relrank (map f (comap f B)))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| b E • Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)

Tactic:
← Φ'_map,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (c E).num ≠ 0

Tactic:
exact num_ne_zero (c_ne_zero h)

Goal state after: