mathlib-initiative/mathlib-tactics huggingface dataset:
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 q.Gal

Tactic:
have : Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
    rw [minpoly.eq_of_irreducible q_irred q_aeval]
    exact isSolvable_gal_minpoly hx
  refine Group.isSolvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)
  aesop

Goal state after:
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 ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inl)
      ((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inr) ↔
    (φ.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 ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
Function.comp_assoc,

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 ∘ Sum.elim (v ∘ Subtype.val) xs ∘ Sum.inl)
      ((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inr) ↔
    (φ.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 ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inl val✝)

Tactic:
simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]

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
p q : L.Substructure M
h : ↑p = ↑q
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
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
q : L.Substructure M
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝, fun_mem := fun_mem✝ } = ↑q
⊢ { carrier := carrier✝, fun_mem := fun_mem✝ } = q
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case pos
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
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
h : t ∈ s
⊢ ClosedUnder f ((fun t ↦ ⋂ (_ : t ∈ s), ↑t) t)

pp: case neg
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
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
h : t ∉ s
⊢ ClosedUnder f ((fun t ↦ ⋂ (_ : t ∈ s), ↑t) t)

Tactic:
· simpa [h] using! t.fun_mem f

Goal state after:
case neg
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
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
h : t ∉ s
⊢ ClosedUnder f ((fun t ↦ ⋂ (_ : t ∈ s), ↑t) t)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
have : Countable s := h.to_subtype

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable ↑s
⊢ Countable ↥((closure L).toFun s)
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
s : Set M
⊢ Small.{u, w} ↥⊥

Tactic:
by
  rw [← closure_empty]
  have : Small.{u} (∅ : Set M) := small_subsingleton _
  exact Substructure.small_closure

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
⊢ (RelMap R fun i ↦ ((⇑f ∘ Term.realize (Sum.elim default xs)) ∘ ts) i) ↔
    RelMap R fun i ↦ (Term.realize (Sum.elim default xs) ∘ ts) i

Tactic:
Function.comp_assoc,

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
⊢ (RelMap R fun i ↦ (⇑f ∘ Term.realize (Sum.elim default xs) ∘ ts) i) ↔
    RelMap R fun i ↦ (Term.realize (Sum.elim default xs) ∘ ts) i
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ f.range = ⊤ ↔ Function.Surjective ⇑f

Tactic:
rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
Formula.iExs

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a ↦ Sum.map id (⇑(Classical.choice ⋯)) a) φ).exs.Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)
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
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
a : N
ha : ¬φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
⊢ (∼φ).Realize default (Fin.snoc (⇑f ∘ xs) a)

Tactic:
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
          exact ha

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]

Tactic:
exact forall_congr' fun _ ↦ realize_rel₂

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
n : ℕ
⊢ K ⊨ genericMonicPolyHasRoot n ↔ ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, eval x ↑p = 0

Tactic:
by
  rw [Equiv.forall_congr_left ((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv)]
  simp [Sentence.Realize, genericMonicPolyHasRoot, lift_genericMonicPoly]

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Surjective res

Tactic:
rw [← Finite.injective_iff_surjective]

Goal state after:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Injective res
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inl
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
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
eq : ℵ₀ = Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

pp: case inr
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
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
· simp_rw [← eq, mk_lt_aleph0_iff] at this
        have : FiniteDimensional F (adjoin F s) :=
          finiteDimensional_adjoin fun x _ ↦ (IsAlgebraic.isAlgebraic x).isIntegral
        exact (Module.rank_lt_aleph0 _ _).trans_eq eq

Goal state after:
case inr
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
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
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
i : WithTop (Module.rank F E).ord.ToType
h : i < ⊤
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case coe
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
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
· obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne
      exact ⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩

Goal state after:
case coe
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
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
⊢ ⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun x ↦ ↑(g x)) (↑s) Set.univ

Tactic:
simp [Set.eq_univ_iff_forall, mem_leftCoset_iff, Set.SurjOn,
    QuotientGroup.forall_mk, QuotientGroup.eq]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
⊢ mk K p (m, x) * (mk K p (m, x))⁻¹ = 1

Tactic:
have := mt (eq_iff _ _ _ _).2 H
    rw [mk_inv, mk_mul_mk]
    refine (eq_iff K p _ _).2 ?_
    simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢
    rw [mul_inv_cancel₀ this, iterate_map_one]

Goal state after:
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)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
rw [← mem_nthRoots hn, (hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq
    (rootOfSplitsXPowSubC_pow a L)] at hα

Goal state after:
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)
α : L
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hα : α ∈ Multiset.map (fun x ↦ (algebraMap K L) ζ ^ x * rootOfSplitsXPowSubC ⋯ a L) (Multiset.range n)
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = ⊤

Tactic:
apply Subalgebra.restrictScalars_injective R
      rw [restrictScalars_top, ← H']
      exact mulMap_range A B

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0) → x = -y

Tactic:
rintro ⟨a, rfl, b, rfl, h⟩
    rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]

Goal state after:
Module: Mathlib.FieldTheory.PrimeField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
⊢ ⊥ = (algebraMap ℚ K).fieldRange

Tactic:
by
  rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]

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:
dsimp [iterateFrobenius]

Goal state after:
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
⊢ IsPurelyInseparable.iterateFrobeniusAux✝ K L p n (r • a) =
    (_root_.iterateFrobenius F p n) r • IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a
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
⊢ IsPurelyInseparable F E ↔ perfectClosure F E = ⊤

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ (∀ (x : E), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ 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
⊢ IsPurelyInseparable F ↥(perfectClosure F E)

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]

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
⊢ ∀ (x : ↥(perfectClosure F E)), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥(perfectClosure F E)).range
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
x : E
⊢ IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1

Tactic:
by
  rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ ↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree

Tactic:
by
  apply natDegree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs)
    (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx) x.denom_ne_zero
  rw [mul_assoc]

Goal state after:
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
⊢ A ⊓ map f ⊤ ⊓ map f B = A ⊓ map f B

Tactic:
inf_assoc,

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 ⊓ (map f ⊤ ⊓ 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
⊢ A ⊓ f.fieldRange ⊓ (B ⊓ f.fieldRange) = A ⊓ (B ⊓ f.fieldRange)

Tactic:
inf_assoc,

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

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

Tactic:
inf_assoc,

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ (B ⊓ C)).relrank C
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : IsConvexSet R s
hsx : IsConvexSet R (s \ {x})
hx : x ∈ s \ {x}
⊢ False

Tactic:
exact hx.2 (mem_singleton _)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hF : F.IsFaceOf C
⊢ ∀ {x y : N} {a : R}, f x ∈ C → f y ∈ C → 0 < a → a • f x + f y ∈ F → f x ∈ F

Tactic:
exact hF.mem_of_smul_add_mem

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 ≠ ⊥
| Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) * ↑⟨generator E, ⋯⟩) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
enter [1, 2, 1, 2, 2]; rw [← num_div_denom (generator E)]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| ↑⟨(algebraMap K[X] K⟮X⟯) (generator E).num / (algebraMap K[X] K⟮X⟯) (generator E).denom, ⋯⟩