mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mp
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.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
refine ⟨y, ys, ?_⟩

Goal state after:
case intro.intro.mp
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.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ y ∘ f = x
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'

Tactic:
have h := mk_image_eq_lift _ s' Equiv.ulift.injective

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{max w w', w} #↑(⇑Equiv.ulift '' s') = lift.{w, max w w'} #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ BoundedFormula.Realize φ (⇑g ∘ v) default = BoundedFormula.Realize φ (⇑g ∘ v) (⇑g ∘ default)

Tactic:
Unique.eq_default (g ∘ default)

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ BoundedFormula.Realize φ (⇑g ∘ v) default = BoundedFormula.Realize φ (⇑g ∘ v) default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ Formula.Realize φ (⇑g ∘ default) ↔ Formula.Realize φ default

Tactic:
Unique.eq_default (g ∘ default)

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ Formula.Realize φ default ↔ Formula.Realize φ default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
Theory.model_iff_subset_completeTheory,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ T ⊆ L.completeTheory M ↔ N ⊨ T
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ T ⊆ L.completeTheory M ↔ N ⊨ T

Tactic:
Theory.model_iff_subset_completeTheory,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ T ⊆ L.completeTheory M ↔ T ⊆ L.completeTheory N
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
p : ℕ
hp : p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
subst hp

Goal state after:
case inr
⊢ (Theory.ACF 0).IsSatisfiable
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀

pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀

Tactic:
· rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b = 0 ∨ c = 0
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False

Tactic:
cases hbc

Goal state after:
case inl
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : b = 0
⊢ False

case inr
n : ℕ
h✝¹ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
h✝ : c = 0
⊢ False
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
n : ℕ
a : R
⊢ logDeriv (a ^ n) = ↑n * logDeriv a

Tactic:
by
  induction n with
  | zero => simp
  | succ n h2 =>
    obtain rfl | hb := eq_or_ne a 0
    · simp
    · rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul, ← h2, pow_succ, logDeriv_mul] <;>
      simp [hb]

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ FinTrdeg K L → Algebra.trdeg K L < Cardinal.aleph0

Tactic:
intro ⟨E, fg, alg⟩

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K L < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
⊢ f.natDegree ∣ n

Tactic:
have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime k p⟩

Goal state after:
case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this : Fact (Nat.Prime p)
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝ : NeZero f.natDegree
this : Fact (Irreducible f)
p : ℕ
hp : CharP k p
⊢ (aeval a) (X ^ Nat.card k ^ f.natDegree - X) = 0

Tactic:
have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime k p⟩

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝¹ : NeZero f.natDegree
this✝ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this : Fact (Nat.Prime p)
⊢ (aeval a) (X ^ Nat.card k ^ f.natDegree - X) = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
· intro a; rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ (evalᵢ σ K).ker = ⊥

Tactic:
by
  cases nonempty_fintype σ
  refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)
  classical
  rw [Module.finrank_fintype_fun_eq_card, finrank_R]

Goal state after:
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ T1Space X

Tactic:
((t1Space_TFAE X).out 0 1 :)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : TotallyDisconnectedSpace X
⊢ ∀ (x : X), IsClosed[inst✝] {x}
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Tactic:
apply_fun e.symm at h

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : e.symm ↑a = e.symm (∑ x, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ e v₁ = v₁

Tactic:
simp only [v₁, map_div₀, map_sum, map_natCast]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ (∑ x, e (x v)) / ↑(Fintype.card Gal(K/F)) = (∑ x, x v) / ↑(Fintype.card Gal(K/F))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
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
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥

Tactic:
have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
    rw [← range_coe] at hi; exact (hi inferInstance).elim

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: case convert_2
K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ s • ↑x = ↑(((algebraMap S M).codRestrict (F.extendRight M).toSubalgebra ⋯) s) * ↑x

Tactic:
RingHom.codRestrict_apply,

Goal state after:
case convert_2
K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ s • ↑x = (algebraMap S M) s * ↑x
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
i : K →+* L
p : ℕ
inst✝² : IsPRadical i p
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : L
⊢ (iterateFrobeniusEquiv L p (Classical.choose ⋯).1).symm (i (Classical.choose ⋯).2) = x

Tactic:
Classical.choose_spec (lift_aux i p x),

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
i : K →+* L
p : ℕ
inst✝² : IsPRadical i p
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : L
⊢ (iterateFrobeniusEquiv L p (Classical.choose ⋯).1).symm (x ^ p ^ (Classical.choose ⋯).1) = x
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℤ
⊢ ↑x = mk K p (0, ↑x)

Tactic:
cases x <;> simp [natCast K p 0]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
e : PerfectClosure K p
⊢ ∀ (x y : ℕ × K), R K p x y → (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2) = (⇑(frobeniusEquiv L p).symm)^[y.1] (f y.2)

Tactic:
rintro - - ⟨n, x⟩

Goal state after:
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
e : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobeniusEquiv L p).symm)^[(n, x).1] (f (n, x).2) =
    (⇑(frobeniusEquiv L p).symm)^[(n + 1, (frobenius K p) x).1] (f (n + 1, (frobenius K p) x).2)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
h : H.index = 0
⊢ False

Tactic:
rw [hind, Finset.card_eq_zero] at h

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
by
  have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out
  have ntrivial : Subring.center D ≠ ⊤ :=
    congr(Subalgebra.toSubring $hcenter).trans_ne (Subalgebra.toSubring_injective.ne hneq)
  set φ := Subalgebra.equivOfEq (⊥ : Subalgebra L D) (.center L D) hcenter.symm
  set equiv : L ≃+* (center D) := ((botEquiv L D).symm.trans φ).toRingEquiv
  let _ : Algebra L (center D) := equiv.toRingHom.toAlgebra
  let _ : Algebra (center D) L := equiv.symm.toRingHom.toAlgebra
  have _ : IsScalarTower L (center D) D := .of_algebraMap_eq fun _ ↦ rfl
  have _ : IsScalarTower (center D) L D := .of_algebraMap_eq fun x ↦ by
    rw [IsScalarTower.algebraMap_apply L (center D)]
    congr
    exact (equiv.apply_symm_apply x).symm
  have _ : Algebra.IsAlgebraic (center D) D := .tower_top (K := L) _
  obtain ⟨x, hxd, hx⟩ := exists_separable_and_not_isCentral D ntrivial
  exact ⟨x, ⟨by rwa [← Subalgebra.center_toSubring L, hcenter] at hxd, IsSeparable.tower_top _ hx⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n - C a) = 0

Tactic:
AdjoinRoot.eval₂_root

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ 0 = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(L/K)
⊢ σ (rootOfSplitsXPowSubC ⋯ a L) = (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Tactic:
by
  obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ
  rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]
  simp only [MulEquiv.symm_trans_apply, AlgEquiv.autCongr_symm, AlgEquiv.symm_symm,
    MulEquiv.symm_symm, AlgEquiv.autCongr_apply, AlgEquiv.trans_apply,
    adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_root, map_smul,
    adjoinRootXPowSubCEquiv_root]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
⊢ ⋃ p ∈ s, ↑p ≠ Set.univ

Tactic:
by
  intro hcovers
  have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers
  have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex
  have : Nontrivial (E ⧸ p) := Submodule.Quotient.nontrivial_iff.mpr (ne_of_mem_of_not_mem hp hs)
  have : Infinite (E ⧸ p) := Module.Free.infinite k (E ⧸ p)
  exact not_finite (E ⧸ p)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Polynomial.C f.num - Polynomial.C f.denom * Polynomial.X = Polynomial.C f.num + -Polynomial.C f.denom * Polynomial.X

Tactic:
neg_mul

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Polynomial.C f.num - Polynomial.C f.denom * Polynomial.X = Polynomial.C f.num + -(Polynomial.C f.denom * Polynomial.X)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
f : K⟮X⟯
hf₁ : f ∈ E
hf₂ : f ∉ ⊥
⊢ IsAlgebraic (↥E) X

Tactic:
exact IsAlgebraic.tower_top_of_subalgebra_le (adjoin_simple_le_iff.mpr hf₁) <|
    f.isAlgebraic_adjoin_simple_X (by rintro ⟨c, rfl⟩; exact hf₂ ⟨c, rfl⟩)

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using! congr(toNat $(relrank_inf_mul_relrank A B C))

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (θ E).natDegree ≤ m E

Tactic:
convert! natDegree_sub_le _ _ using 3

Goal state after:
case e'_4.e'_3
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree = (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)).natDegree

case e'_4.e'_4
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree = (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)).natDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using! congr(toNat $(relrank_inf_mul_relrank A B C))

Goal state after: