mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ : M →[L] N
S : L.Substructure N
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S
⊢ funMap f (⇑φ ∘ x) ∈ ↑S

Tactic:
exact S.fun_mem f (φ ∘ x) hx

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
refine
    ⟨(equivShrink S).bundledInduced L,
      ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
      lift_inj.1 (_root_.trans ?_ hS)⟩

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ lift.{w', w} #↑(Equiv.bundledInduced L (equivShrink ↥S)) = lift.{w, w'} #↥S
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ

Tactic:
| intro M MI =>

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, #↑N = κ

Tactic:
cases h with
  | intro M MI =>
    obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
    have : Nonempty N := hN.nonempty
    exact ⟨hN.theory_model.bundled, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
Set.definable_iff_finitely_definable

Goal state after:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : ∃ A0, ↑A0 ⊆ c ∧ (↑A0).Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
Module: Mathlib.FieldTheory.Finite.Valuation

Goal state before:
pp: Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst✝⁴ : Field Fq
inst✝³ : Finite Fq
inst✝² : Ring A
inst✝¹ : Algebra Fq A
inst✝ : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
ha : a ≠ 0
⊢ v ((algebraMap Fq A) a) = 1

Tactic:
by
  have : Fintype Fq := Fintype.ofFinite Fq
  have hpow : (v (algebraMap Fq A a)) ^ (Fintype.card Fq - 1) = 1 := by
    simp [← map_pow, FiniteField.pow_card_sub_one_eq_one a ha]
  grind [pow_eq_one_iff, → IsPrimePow.two_le, FiniteField.isPrimePow_card]

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

Goal state before:
pp: case a
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
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
| (↑v)′

Tactic:
apply (deriv_algebraMap v)

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

Goal state before:
pp: case e'_6
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
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ (e v)′ = e v′

Tactic:
rw [algEquiv_deriv']

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) s * ↑x

Tactic:
← Algebra.smul_def

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 = s • ↑x
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
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f ↦ f.comp i) f = (fun f ↦ f.comp i) g
x : L
⊢ f x = g x

Tactic:
obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x

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
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f ↦ f.comp i) f = (fun f ↦ f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x = g 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
f : PerfectClosure K p → PerfectClosure K p := fun e ↦ e.liftOn (fun x ↦ mk K p (x.1 + 1, x.2)) ⋯
⊢ Bijective fun x ↦ (frobenius (PerfectClosure K p) p) x

Tactic:
refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩

Goal state after:
case refine_1
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p := fun e ↦ e.liftOn (fun x ↦ mk K p (x.1 + 1, x.2)) ⋯
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ f ((fun x ↦ (frobenius (PerfectClosure K p) p) x) (mk K p (n, x))) = mk K p (n, x)

case refine_2
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p := fun e ↦ e.liftOn (fun x ↦ mk K p (x.1 + 1, x.2)) ⋯
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ (fun x ↦ (frobenius (PerfectClosure K p) p) x) (f (mk K p (n, x))) = mk K p (n, x)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mk
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 : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobenius L p))^[n] ((⇑(frobeniusEquiv L p).symm)^[n] (f ((of K p) x))) =
    f ((⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)))

Tactic:
iterate_frobenius_mk,

Goal state after:
case mk
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 : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobenius L p))^[n] ((⇑(frobeniusEquiv L p).symm)^[n] (f ((of K p) x))) = f ((of K p) x)
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:
by
  simp [Set.eq_univ_iff_forall, mem_leftCoset_iff, Set.SurjOn,
    QuotientGroup.forall_mk, QuotientGroup.eq]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
⊢ ∃ b, ((ad (↥k) D) a) b ≠ 0

Tactic:
by
    rw [Subring.mem_center_iff, not_forall] at ha
    use ha.choose
    change a * ha.choose - ha.choose * a ≠ 0
    simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑(↑A ∪ ↑B))) ℵ₀ ≤ Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
calc
    _ ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} (#A ⊔ #B) ⊔ ℵ₀ := by
      gcongr
      rw [Cardinal.lift_le]
      exact (mk_union_le _ _).trans_eq (by simp)
    _ = _ := by
      simp [lift_mk_le_lift_mk_of_injective (algebraMap F A).injective]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ p ^ n - C a)

Tactic:
by
  apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow
  intro q hq hq'
  simpa [(Nat.prime_dvd_prime_iff_eq hq hp).mp (hq.dvd_of_dvd_pow hq')] using ha

Goal state after:
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:
have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out

Goal state after:
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 : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
⊢ ∃ x ∉ ⊥, IsSeparable L x
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ

Tactic:
rw [← hcovers', Set.iUnion_sigma, Set.iUnion_subtype]
    refine Set.iUnion_congr fun i => ?_
    rw [Finset.mem_filter, Set.iUnion_and]
    refine Set.iUnion_congr fun hi => ?_
    by_cases hfi : (H i).FiniteIndex <;>
      simp [Set.smul_set_iUnion, Set.iUnion_subtype, ← leftCoset_assoc,
        f, K, hHD, ← (ht i hi _).2, hfi]

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this : FiniteDimensional F ↥F⟮a⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
have : FiniteDimensional F F⟮b⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral b)

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K 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
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
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
x✝ : L'
⊢ (IsScalarTower.toAlgHom F L' E) x✝ = ((IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)) x✝

Tactic:
exact IsScalarTower.algebraMap_apply L' L E _

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 B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B

Tactic:
h₁,

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ finrank F ↥⊤ = finrank F ↥A * finrank F ↥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
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
this : IsGalois (↥B) E
⊢ Nat.card Gal(E/↥B) = Nat.card Gal(↥A/F)

Tactic:
exact Nat.card_congr <| Equiv.ofBijective (restrictRestrictAlgEquivMapHom _ _ _ _)
    ⟨restrictRestrictAlgEquivMapHom_injective _ _ h₁,
      restrictRestrictAlgEquivMapHom_surjective _ _ h₂⟩

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
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ adjoin F S = adjoin F ((fun x ↦ x ^ q ^ n) '' S)

Tactic:
set M := adjoin F ((· ^ q ^ n) '' S)
  have := expChar_of_injective_algebraMap (algebraMap F M).injective q
  refine le_antisymm (adjoin_le_iff.2 fun x hx ↦ ?_) (adjoin_le_iff.2 ?_)
  · have : Algebra.IsSeparable M M⟮x⟯ :=
      (isSeparable_adjoin_simple_iff_isSeparable M E).2 <|
        ((isSeparable_adjoin_iff_isSeparable F E).1 inferInstance x hx).tower_top M
    have : IsPurelyInseparable M M⟮x⟯ :=
      (isPurelyInseparable_adjoin_simple_iff_pow_mem M E q).2
        ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩
    have hx' := mem_adjoin_simple_self M x
    rw [M⟮x⟯.eq_bot_of_isPurelyInseparable_of_isSeparable, mem_bot] at hx'
    obtain ⟨y, rfl⟩ := hx'
    exact y.2
  · rintro _ ⟨y, hy, rfl⟩
    exact pow_mem (subset_adjoin F S hy) _

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

Goal state before:
pp: case haeval
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ (Polynomial.aeval (a ^ q ^ n)) (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) = 0

pp: case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ (Polynomial.map (iterateFrobenius F q n) (minpoly F a)).natDegree ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree

Tactic:
· simpa using! Eq.symm <|
      (minpoly F a).map_aeval_eq_aeval_map (RingHom.iterateFrobenius_comm _ q n) a

Goal state after:
case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ (Polynomial.map (iterateFrobenius F q n) (minpoly F a)).natDegree ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree
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 : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
i : ι
⊢ lF i ≠ 0 → i ∈ l.support

Tactic:
contrapose

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
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 : ι → ℕ
n : ℕ := ⋯
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
i : ι
⊢ i ∉ l.support → lF i = 0
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
· simp [hx]

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree
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) / C f.num.leadingCoeff)⁻¹
⊢ False

Tactic:
← map_div₀,

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
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 ⋯
⊢ Irreducible (f.minpolyX ↥K[f])

Tactic:
let φ : K[X][X] := f.num.map (algebraMap ..) -
    Polynomial.C Polynomial.X * f.denom.map (algebraMap ..)

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
⊢ Irreducible (f.minpolyX ↥K[f])
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 ∉ ⊥
⊢ ¬∃ c, f = C c

Tactic:
by rintro ⟨c, rfl⟩; exact hf₂ ⟨c, rfl⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
⊢ (∃ D, Submodule.FG D ∧ dual p ↑D = C) → DualFG p C

Tactic:
rintro ⟨_, ⟨s, rfl⟩, rfl⟩
    use s; simp

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 ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree

Tactic:
conv at this => enter [2, 1, 2]; rw [← num_div_denom (generator E)]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num *
        ((algebraMap K[X] K⟮X⟯) (generator E).num / (algebraMap K[X] K⟮X⟯) (generator E).denom) *
      (algebraMap K[X] K⟮X⟯) (g E)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
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✝ : (convexHull R) s = {x}
hs : s = ∅
⊢ False

Tactic:
simp_all [eq_comm (a := ∅)]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ E = K⟮generator E⟯

Tactic:
by_cases h : E = ⊥
  · rwa [generator_eq_zero h, adjoin_zero]
  refine le_antisymm (relfinrank_eq_one_iff.mp ?_) adjoin_generator_le
  suffices (φ E).natDegree = m E 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))
  rw [← Φ_natDegree_eq_φ_natDegree h, Φ_natDegree_eq_θ_natDegree h]
  exact le_antisymm (θ_natDegree_le h) (swap_Φ_natDegree_eq_θ_natDegree h ▸ m_le_swap_Φ_natDegree h)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (vectorSpan ℝ ((s.map f.toAffineMap ⋯).points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points) =
    (Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ f.linearIsometry.range ⊓
      Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (Set.range s.points))

Tactic:
← AffineIsometry.linear_eq_linearIsometry,

Goal state after:
case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (vectorSpan ℝ ((s.map f.toAffineMap ⋯).points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points) =
    (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ f.linear.range ⊓
      Submodule.map f.linear (vectorSpan ℝ (Set.range s.points))