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

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ↑i + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))

Tactic:
natCast_lt_aleph0

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ max ℵ₀ #(↑s ⊕ (i : ℕ) × L.Functions i) ≤ max ℵ₀ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
mk_sum,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ max ℵ₀ (lift.{u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ ((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs

Tactic:
simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]
  refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl
  simp only [relabelEquiv_apply, Term.realize_relabel]
  refine congr (congr rfl ?_) rfl
  ext (i | i) <;> rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : M ⊨ T
h' : M ⊨ T'
⊢ M ⊨ T ∪ T'

Tactic:
simp only [model_iff, Set.mem_union] at *
  exact fun φ hφ => hφ.elim (h _) (h' _)

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ ((closure L).toFun (A ∪ s)).withConstants ⋯ ≤ (closure L[[↑A]]).toFun s

Tactic:
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ (L.lhomWithConstants ↑A).substructureReduct (((closure L).toFun (A ∪ s)).withConstants ⋯) ≤
    (L.lhomWithConstants ↑A).substructureReduct ((closure L[[↑A]]).toFun s)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
mk_sum,

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} #((k : ℕ) × L.Term (α ⊕ Fin k)) + lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)) + lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
mk_sum,

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (max ℵ₀ (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
mk_sum,

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} #ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v} #((l : ℕ) × L.Functions l ⊕ (l : ℕ) × L.Relations l))

Tactic:
mk_sum,

Goal state after:
L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v}
          (lift.{v, u} #((l : ℕ) × L.Functions l) + lift.{u, v} #((l : ℕ) × L.Relations l)))
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ ∅.TermDefinable L f ↔ ∃ φ, f = fun v ↦ Term.realize v φ

Tactic:
TermDefinable,

Goal state after:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ φ, f = fun v ↦ Term.realize v φ) ↔ ∃ φ, f = fun v ↦ Term.realize v φ
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : Cardinal.{u}
⊢ a = 1 → IsUnit a

Tactic:
rintro rfl

Goal state after:
⊢ IsUnit 1
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
⊢ logDeriv 0 = 0

Tactic:
by
  simp [logDeriv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
⊢ logDeriv 1 = 0

Tactic:
by
  simp [logDeriv]

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
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a * b) = logDeriv a + logDeriv b

Tactic:
unfold logDeriv

Goal state after:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b)′ / (a * b) = a′ / a + b′ / b
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a / b) = logDeriv a - logDeriv b

Tactic:
unfold logDeriv

Goal state after:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ (a / b)′ / (a / b) = a′ / a - b′ / b
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x)

Tactic:
unfold logDeriv

Goal state after:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ (∏ x ∈ s, f x)′ / ∏ x ∈ s, f x = ∑ x ∈ s, (f x)′ / f x
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ logDeriv ((algebraMap F K) a) = (algebraMap F K) (logDeriv a)

Tactic:
unfold logDeriv

Goal state after:
F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ ((algebraMap F K) a)′ / (algebraMap F K) a = (algebraMap F K) (a′ / a)
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : AlgebraicIndependent K x
⊢ Finite ι

Tactic:
rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : AlgebraicIndependent K x
⊢ Cardinal.lift.{?u.24, u_3} (Cardinal.mk ι) < Cardinal.aleph0
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
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
⊢ Nonempty (l ≃ₐ[k] Extension k p n)

Tactic:
have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this : Module.Finite k l
⊢ Nonempty (l ≃ₐ[k] Extension k p n)
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
K : Type u_3
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ ((algebraMap (↥B) K) a)′ = (algebraMap (↥B) K) a′

Tactic:
change (B.val a)′ = B.val a′

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
K : Type u_3
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ (B.val a)′ = B.val a′
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
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
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, (algebraMap F K) (c x / ↑(Fintype.card Gal(K/F))) * logDeriv (∏ x_1, x_1 (u x)) +
      ((∑ x, x v) / ↑(Fintype.card Gal(K/F)))′

Tactic:
push_cast

Goal state after:
case refine_2
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
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, ↑(c x) / ↑(Fintype.card Gal(K/F)) * logDeriv (∏ x_1, x_1 (u x)) + ((∑ x, x v) / ↑(Fintype.card Gal(K/F)))′
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
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 : ⊤ ≤ adjoin F s
⊢ False

Tactic:
← eq_top_iff

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
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 : adjoin F s = ⊤
⊢ False
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : x ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ x ∈ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

Tactic:
apply hO

Goal state after:
case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : x ∈ ↑(IntermediateField.lift L').fixingSubgroup
⊢ (AlgEquiv.restrictNormalHom ↥L) x ∈ ↑L'.fixingSubgroup
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hn : n ≠ 0
⊢ ∃ r, x = r ^ n

Tactic:
induction n using Nat.strong_induction_on generalizing x with
  | h n ih =>
    rcases Nat.even_or_odd n with (even | odd)
    · rcases even with ⟨m, hm⟩
      rcases hx with ⟨s, hs⟩
      rcases isSquare_or_isSquare_neg s with (h | h) <;>
        rcases ih m (by lia) h (by lia) with ⟨r, hr⟩ <;>
        exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩
    · exact exists_eq_pow_of_odd x odd

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
inst✝ : ExpChar L p
x : K
⊢ (lift i j p) (i x) = j x

Tactic:
by
  rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_zero]; rfl

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
hn : a ^ p ^ 0 ∈ k
⊢ False
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers'✝ : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x✝ : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x✝⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x ↦
    match x with
    | (k₁, some k₂) => g ↑k₂ * x✝⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ¬⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
x : Subgroup G
⊢ (∃ y, K y = x) → x ∈ (Finset.image H s).erase (H j)

Tactic:
exact fun ⟨k, hk⟩ => hk ▸ hK' k

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ m ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (X ^ 0 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
h : ¬root (X ^ n - C a) = 0
⊢ σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
div_mul_cancel₀ _ h

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
h : ¬root (X ^ n - C a) = 0
⊢ σ (root (X ^ n - C a)) = σ (root (X ^ n - C a))
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
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
this : Fintype ↑(Set.range p)
⊢ ∃ i, p i = ⊤

Tactic:
simp_rw [← Set.biUnion_range (f := p), ← Set.mem_toFinset] at hcovers

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
this : Fintype ↑(Set.range p)
hcovers : ⋃ x ∈ (Set.range p).toFinset, ↑x = Set.univ
⊢ ∃ i, p i = ⊤
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

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

Tactic:
rintro rfl

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
y : ConjRootClass K L
⊢ ∃ a, mk K a = -y ∧ ∃ b, mk K b = y ∧ a + b = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ (A.mulMap B).range = A ⊔ B

Tactic:
simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: 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
H : IsField (A ⊗[R] B)
⊢ Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B

Tactic:
by
  by_contra! h
  simp_rw [← Algebra.transcendental_iff_not_isAlgebraic] at h
  obtain ⟨_, _⟩ := h
  exact Algebra.TensorProduct.not_isField_of_transcendental R A B H

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{v, w} (Module.rank F L) * Cardinal.lift.{w, v} (Module.rank (↥(adjoin L ↑A)) E) =
    Cardinal.lift.{w, v} (Module.rank (↥A) E)

Tactic:
← H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg,

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars ⋯)) * Cardinal.lift.{w, v} (Module.rank (↥(adjoin L ↑A)) E) =
    Cardinal.lift.{w, v} (Module.rank (↥A) 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
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : (frobenius E p) x' = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = ↑x ^ p ^ n
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x

Tactic:
rw [frobenius_def] at hx

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
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = ↑x ^ p ^ n
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by_cases hs : i ∈ l.support

Goal state after:
case pos
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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

case neg
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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ l i ^ q ^ n ∈ (algebraMap 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
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((Algebra.ofId F E).toRingHom z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x

Tactic:
simp only [Algebra.ofId] at h

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((algebraMap F E) z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u_1
inst✝ : Field K
hf : ¬∃ c, 0 = C c
⊢ False
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : f = (C (f.denom.coeff f.num.natDegree / f.num.leadingCoeff))⁻¹
⊢ False

Tactic:
← map_inv₀

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : f = C (f.denom.coeff f.num.natDegree / f.num.leadingCoeff)⁻¹
⊢ False