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

Goal state before:
pp: case refine_2
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U✝ : Set α
hU : IsOpen U✝
x✝¹ : U✝.Nonempty
b : M
x✝ : α
⊢ x✝ ∈ (fun x ↦ b • x) ⁻¹' ⋃ m, (fun x ↦ m • x) ⁻¹' U✝ → x✝ ∈ ⋃ m, (fun x ↦ m • x) ⁻¹' U✝

Tactic:
simp only [preimage_iUnion, mem_iUnion, mem_preimage, smul_smul, forall_exists_index]

Goal state after:
case refine_2
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U✝ : Set α
hU : IsOpen U✝
x✝¹ : U✝.Nonempty
b : M
x✝ : α
⊢ ∀ (x : M), (x * b) • x✝ ∈ U✝ → ∃ i, i • x✝ ∈ U✝
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
s : Subalgebra F E :=
  { carrier := {x | ∃ (hx : x ∈ solvableByRad F E), motive x hx}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
    zero_mem' := ⋯, algebraMap_mem' := ⋯ }
⊢ s.IsAlgebraic

Tactic:
rintro x ⟨hx, hx'⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x✝ : E
hx✝ : x✝ ∈ solvableByRad F E
s : Subalgebra F E :=
  { carrier := {x | ∃ (hx : x ∈ solvableByRad F E), motive x hx}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
    zero_mem' := ⋯, algebraMap_mem' := ⋯ }
x : E
hx : x ∈ solvableByRad F E
hx' : motive x hx
⊢ IsAlgebraic F x
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x : ring.Term α
v : α → R
⊢ Term.realize v (-x) = -Term.realize v x

Tactic:
simp [neg_def, funMap_neg]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
exact isSolvable_gal_minpoly hx

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
⊢ (LHom.id L).onBoundedFormula = id

Tactic:
ext f
  induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
⊢ ∀ (xs : Fin k → M), (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

Tactic:
xs

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)
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)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y

Tactic:
refine mem_of_superset (iInter_mem.2 xy) fun a ha => ?_

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : a ∈ ⋂ i, {x_1 | (fun a ↦ x i a = y i a) x_1}
⊢ a ∈ {x_1 | (fun a ↦ funMap f x a = funMap f y a) x_1}
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize (v ∘ Subtype.val) xs ↔ φ.Realize v xs

Tactic:
BoundedFormula.realize_restrictFreeVar v (by simp)

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ φ.Realize v xs ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
φ : L.Formula α
x : α → M
⊢ φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
by
  rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.falsum.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ BoundedFormula.falsum.Realize default xs

Tactic:
exact fun {_} _ => Iff.rfl

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
⊢ ∀ (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

Tactic:
xs

Goal state after:
case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
⊢ ∀ (xs : Fin n → M), (∀' φ).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' φ).Realize default xs

Tactic:
xs

Goal state after:
case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀' φ).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' φ).Realize default xs
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (⋃ i ∈ s, f i)

Tactic:
by
  rw [← Finset.sup_set_eq_biUnion]
  exact definable_finset_sup hf s

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default ⇑xs.some

Tactic:
rintro _ i j ij rfl
    simpa using ij

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ((fun x ↦ f (x ())) = fun v ↦ Term.realize v φ) ↔ f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
funext_iff,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ (∀ (x : Unit → M), f (x ()) = Term.realize x φ) ↔ f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ (∀ (x : Unit → M), f (x ()) = Term.realize x φ) ↔ f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
funext_iff,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ (∀ (x : Unit → M), f (x ()) = Term.realize x φ) ↔
    ∀ (x : M), f x = ((fun v ↦ Term.realize v φ) ∘ Function.const Unit) x
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ (Derivation.liftOfSurjective ⋯ ⋯) ((AdjoinRoot.mk p).toIntAlgHom (C a)) = (algebraMap F (AdjoinRoot p)) a′

Tactic:
rw [Derivation.liftOfSurjective_apply, implicitDeriv_C]

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ (AdjoinRoot.mk p).toIntAlgHom (C a′) = (algebraMap F (AdjoinRoot p)) a′
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Fintype k := Fintype.ofFinite k
i : ℕ
hi : i < Module.finrank k (Extension k p n)
⊢ frob k p n ^ i = (fun n_1 ↦ frobeniusAlgEquivOfAlgebraic k (Extension k p n) ^ ↑n_1) ⟨i, hi⟩

Tactic:
ext; simp [frob]

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : ¬a = b
⊢ ∃ i, a i ≠ b i

Tactic:
funext_iff,

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : ¬∀ (x : σ), a x = b x
⊢ ∃ i, a i ≠ b i
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i
      (((Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k).map
            ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec
        (fun x ↦ (algebraMap K L) (a x)) i) =
    ∑ i, a i • i (∑ k, b k • e k)

Tactic:
simp [Algebra.smul_def, Matrix.mulVec_eq_sum, mul_comm]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ (iterateFrobeniusEquiv M p (m + n)) (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p (m + n')) (j y)

Tactic:
iterateFrobeniusEquiv_def,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (Classical.choose ⋯).2 ^ p ^ (m + n) = (iterateFrobeniusEquiv M p (m + n')) (j y)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (Classical.choose ⋯).2 ^ p ^ (m + n) = (iterateFrobeniusEquiv M p (m + n')) (j y)

Tactic:
iterateFrobeniusEquiv_def,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ j (Classical.choose ⋯).2 ^ p ^ (m + n) = j y ^ p ^ (m + n')
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)
⊢ (X ^ n - C a).Separable

Tactic:
by
  let := Fact.mk H
  let : Algebra K K[n√a] := inferInstance
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  by_cases hn' : n = 1
  · rw [hn', pow_one]; exact separable_X_sub_C
  have ⟨ζ, hζ⟩ := hζ
  rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ
  rw [← separable_map (algebraMap K K[n√a]), Polynomial.map_sub, Polynomial.map_pow, map_C, map_X,
    AdjoinRoot.algebraMap_eq,
    X_pow_sub_C_eq_prod (hζ.map_of_injective (algebraMap K _).injective) hn
    (root_X_pow_sub_C_pow n a), separable_prod_X_sub_C_iff']
  exact (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
    (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this : Field (↥A ⊗[R] ↥B) := H.toField
⊢ Function.Injective ⇑(A.mulMap B)

Tactic:
let : NonAssocRing (A ⊗[R] B) := Ring.toNonAssocRing

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
a✝ : Nontrivial S
this✝ : Field (↥A ⊗[R] ↥B) := H.toField
this : NonAssocRing (↥A ⊗[R] ↥B) := Ring.toNonAssocRing
⊢ Function.Injective ⇑(A.mulMap B)
Module: Mathlib.FieldTheory.LinearDisjoint

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✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L'
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'

Tactic:
by
  rw [linearDisjoint_iff] at H ⊢
  have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
  simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this
  rw [AlgHom.fieldRange_toSubalgebra]
  convert! this <;> (ext; exact IsScalarTower.algebraMap_apply _ E K _)

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:
← le_perfectClosure_iff

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
L1 L2 : IntermediateField F E
h1 : L1 ≤ perfectClosure F E
h2 : L2 ≤ perfectClosure F E
⊢ L1 ⊔ L2 ≤ perfectClosure F E
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
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), IsPurelyInseparable F ↥(t i)
⊢ IsPurelyInseparable F ↥(⨆ i, t i)

Tactic:
← le_perfectClosure_iff

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
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ perfectClosure F E
⊢ ⨆ i, t i ≤ perfectClosure F E
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ f = C (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)

Tactic:
map_div₀,

Goal state after:
case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ f = C (f.num.coeff f.denom.natDegree) / C f.denom.leadingCoeff
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ x = y
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ max f.num.natDegree f.denom.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree

Tactic:
· exact max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ (aeval X) f = 0

Tactic:
· simpa using congr(aeval (X : K⟮X⟯) $(hf))

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ E = K⟮0⟯

Tactic:
adjoin_zero

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ E = ⊥
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
⊢ K⟮generator E⟯.relfinrank E = 1

Tactic:
by
    refine (mul_eq_right₀ ?_).mp <| this ▸ (generator E).finrank_eq_max_natDegree ▸
      φ_natDegree h ▸ relfinrank_mul_finrank_top (adjoin_generator_le (E := E))
    intro H
    exact generator_ne_C h ((eq_C_iff _).mpr (Nat.max_eq_zero_iff.mp H))

Goal state after: