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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ i ∈ 𝓤 X, netEntropyEntourage T F i ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
refine iSup₂_le fun U U_uni ↦ ?_

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : CompatibleRing K
n : ℕ
v : Empty → K
⊢ Formula.Realize (eqZero n) v ↔ ↑n = 0

Tactic:
by
  simp [eqZero]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]

Tactic:
by
  rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]
  refine congr rfl (funext fun _ => ?_)
  simp only [Matrix.cons_val_fin_one]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Encodable α
inst✝ : Encodable ((i : ℕ) × L.Functions i)
t : L.Term α
⊢ (do
        let a ← [t].head?
        pure (some a)).join =
    some t

Tactic:
simp only [Option.join, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some,
      id_eq]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ (f✝.restrictFreeVar f).Realize v (snoc xs x✝) ↔ f✝.Realize v' (snoc xs x✝)

Tactic:
rw [ih3]

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ A.Definable L ((fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize)

Tactic:
refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ (fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize = ofPred (BoundedFormula.relabel id φ).exs.Realize
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
a : N
h' : f✝.Realize v (snoc xs (EquivLike.inv g a))
⊢ f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)

Tactic:
rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'

Goal state after:
case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
a : N
h' : f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)
⊢ f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : Algebra.trdeg K L < Cardinal.aleph0
s : Set L
hs : IsTranscendenceBasis K Subtype.val
fin : s.Finite
alg : Algebra.IsAlgebraic (↥(adjoin K (Set.range Subtype.val))) L
⊢ Algebra.IsAlgebraic (↥(adjoin K s)) L

Tactic:
Subtype.range_coe

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : Algebra.trdeg K L < Cardinal.aleph0
s : Set L
hs : IsTranscendenceBasis K Subtype.val
fin : s.Finite
alg : Algebra.IsAlgebraic (↥(adjoin K s)) L
⊢ Algebra.IsAlgebraic (↥(adjoin K s)) L
Module: Mathlib.FieldTheory.Differential.Liouville

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

Tactic:
simpa [AlgEquiv.commutes, map_add, map_sum, map_mul, logDeriv, algEquiv_deriv'] using h

Goal state after:
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
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this : finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ False

Tactic:
refine (isLeast_leastExt i).1 (hx ▸ ?_)

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
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this : finrank ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ ≤ 1
x : ↥(adjoin F (⇑b ∘ φ '' Iio i))
hx : (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x = b (φ i)
⊢ (Algebra.ofId (↥(adjoin F (⇑b ∘ φ '' Iio i))) E).toRingHom x ∈ adjoin F (⇑b ∘ φ '' Iio i)
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: 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
inst✝³ : Algebra R ↥F
inst✝² : Algebra R M
inst✝¹ : IsScalarTower R (↥F) M
inst✝ : IsIntegralClosure S R ↥F
x : S
⊢ (algebraMap (↥(F.extendRight M)) M) ((algebraMap S ↥(F.extendRight M)) x) = (algebraMap (↥F) M) ((algebraMap S ↥F) x)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
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
inst✝³ : Algebra R ↥F
inst✝² : Algebra R M
inst✝¹ : IsScalarTower R (↥F) M
inst✝ : IsIntegralClosure S R ↥F
x : S
⊢ (algebraMap S M) x = (algebraMap (↥F) M) ((algebraMap S ↥F) x)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ x ∈ pNilradical R p → x ∈ ⊥

Tactic:
rw [mem_pNilradical, Ideal.mem_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ (∃ n, x ^ p ^ n = 0) → x = 0
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.hom.op))
          ((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g))
        x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
change (algebraMap L' K (algebraMap L L' (AlgEquiv.restrictNormal (proj (mk L') g) L x))) = _

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      ((algebraMap ↥L ↥L')
        ((((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })
                g).restrictNormal
            ↥L)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
⊢ (algEquivToLimit k K) (limitToAlgEquiv g) = g

Tactic:
apply Subtype.val_injective
    ext L
    change (limitToAlgEquiv g).restrictNormal _ = _
    ext x
    have : ((limitToAlgEquiv g).restrictNormal L.unop) x = (limitToAlgEquiv g) x.1 := by
      exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x
    simp_rw [this]
    exact proj_adjoin_singleton_val _ _ _ _ x.2

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hj' : (g j)⁻¹ * x ∈ ↑H
hi' : (g i)⁻¹ * x ∈ ↑H
hx : x ∈ c
⊢ x ∈ ⊥

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hj' : (g j)⁻¹ * x ∈ H
hi' : (g i)⁻¹ * x ∈ H
hx : x ∈ c
⊢ x ∈ ⊥
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 ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
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 : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : (g i)⁻¹ * (x * (y⁻¹ * z)) ∈ ↑(H i)
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)

Tactic:
SetLike.mem_coe,

Goal state after:
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 ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
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 : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : (g i)⁻¹ * (x * (y⁻¹ * z)) ∈ H i
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)
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
⊢ #↥(adjoin F (↑A ∪ ↑B)) ≤ #↥A * #↥B

Tactic:
mul_mk_eq_max,

Goal state after:
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
⊢ #↥(adjoin F (↑A ∪ ↑B)) ≤ max #↥A #↥B
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ Irreducible (X ^ (p * n) - C a)

Tactic:
| prime_mul p n hp IH =>

Goal state after:
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:
by
      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: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c : ConjRootClass K L
⊢ (-c).carrier = -c.carrier

Tactic:
by
  ext
  simp [mem_carrier, ← mk_neg, neg_eq_iff_eq_neg]

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
⊢ (algebraMap K L) (IsPurelyInseparable.iterateFrobeniusAux✝ K L p n (r • a)) =
    (algebraMap K L) ((algebraMap F K) ((_root_.iterateFrobenius F p n) r)) *
      (algebraMap K L) (IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a)

Tactic:
← IsScalarTower.algebraMap_apply,

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
⊢ (algebraMap K L) (IsPurelyInseparable.iterateFrobeniusAux✝ K L p n (r • a)) =
    (algebraMap F L) ((_root_.iterateFrobenius F p n) r) *
      (algebraMap K L) (IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a)
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
a : F
⊢ (algebraMap K L) ((iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a)) =
    (algebraMap K L) ((algebraMap F K) (a ^ p ^ n))

Tactic:
← IsScalarTower.algebraMap_apply,

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
a : F
⊢ (algebraMap K L) ((iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a)) = (algebraMap F L) (a ^ p ^ n)
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 : (finrank F ↥A).Coprime (finrank F L)
this✝ : Field ↥(IsScalarTower.toAlgHom F L E).range :=
  { toCommRing := (IsScalarTower.toAlgHom F L E).range.toCommRing, inv := of_finrank_coprime._aux_1_1,
    div := of_finrank_coprime._aux_1_3, zpow := of_finrank_coprime._aux_1_5, div_eq_mul_inv := ⋯, zpow_zero' := ⋯,
    zpow_succ' := ⋯, zpow_neg' := ⋯, toNontrivial := ⋯, nnratCast := of_finrank_coprime._aux_1_12,
    ratCast := of_finrank_coprime._aux_1_14, mul_inv_cancel := ⋯, inv_zero := ⋯, nnratCast_def := ⋯,
    nnqsmul := of_finrank_coprime._aux_1_19, nnqsmul_def := ⋯, ratCast_def := ⋯, qsmul := of_finrank_coprime._aux_1_23,
    qsmul_def := ⋯ }
this : Field ↥A.toSubalgebra :=
  { toCommRing := A.toCommRing, inv := fun a ↦ ⟨(↑a)⁻¹, ⋯⟩, div := fun a b ↦ ⟨↑a / ↑b, ⋯⟩,
    zpow := fun n x ↦ Pow.pow x n, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯,
    toNontrivial := ⋯, nnratCast := fun q ↦ ⟨↑q, ⋯⟩, ratCast := fun q ↦ ⟨↑q, ⋯⟩, mul_inv_cancel := ⋯, inv_zero := ⋯,
    nnratCast_def := ⋯, nnqsmul := fun a a_1 ↦ ⟨a • ↑a_1, ⋯⟩, nnqsmul_def := ⋯, ratCast_def := ⋯,
    qsmul := fun a a_1 ↦ ⟨a • ↑a_1, ⋯⟩, qsmul_def := ⋯ }
⊢ (finrank F ↥A.toSubalgebra).Coprime (finrank F ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.finrank_eq

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 : (finrank F ↥A).Coprime (finrank F ↥(IsScalarTower.toAlgHom F L E).range)
this✝ : Field ↥(IsScalarTower.toAlgHom F L E).range :=
  { toCommRing := (IsScalarTower.toAlgHom F L E).range.toCommRing, inv := of_finrank_coprime._aux_1_1,
    div := of_finrank_coprime._aux_1_3, zpow := of_finrank_coprime._aux_1_5, div_eq_mul_inv := ⋯, zpow_zero' := ⋯,
    zpow_succ' := ⋯, zpow_neg' := ⋯, toNontrivial := ⋯, nnratCast := of_finrank_coprime._aux_1_12,
    ratCast := of_finrank_coprime._aux_1_14, mul_inv_cancel := ⋯, inv_zero := ⋯, nnratCast_def := ⋯,
    nnqsmul := of_finrank_coprime._aux_1_19, nnqsmul_def := ⋯, ratCast_def := ⋯, qsmul := of_finrank_coprime._aux_1_23,
    qsmul_def := ⋯ }
this : Field ↥A.toSubalgebra :=
  { toCommRing := A.toCommRing, inv := fun a ↦ ⟨(↑a)⁻¹, ⋯⟩, div := fun a b ↦ ⟨↑a / ↑b, ⋯⟩,
    zpow := fun n x ↦ Pow.pow x n, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯,
    toNontrivial := ⋯, nnratCast := fun q ↦ ⟨↑q, ⋯⟩, ratCast := fun q ↦ ⟨↑q, ⋯⟩, mul_inv_cancel := ⋯, inv_zero := ⋯,
    nnratCast_def := ⋯, nnqsmul := fun a a_1 ↦ ⟨a • ↑a_1, ⋯⟩, nnqsmul_def := ⋯, ratCast_def := ⋯,
    qsmul := fun a a_1 ↦ ⟨a • ↑a_1, ⋯⟩, qsmul_def := ⋯ }
⊢ (finrank F ↥A.toSubalgebra).Coprime (finrank F ↥(IsScalarTower.toAlgHom F L 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
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:
by
  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: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
E' : IntermediateField F E := adjoin F (Set.range v)
y : ι
⊢ IsSeparable F (v y)

Tactic:
exact hsep y

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

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

Tactic:
have : (f.minpolyX K⟮f⟯).natDegree ≤ _ := natDegree_sub_le _ _

Goal state after:
case neg.a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this :
  (f.minpolyX ↥K⟮f⟯).natDegree ≤
    max (Polynomial.map (algebraMap K ↥K⟮f⟯) f.num).natDegree
      (Polynomial.C ((algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom).natDegree
⊢ (f.minpolyX ↥K⟮f⟯).natDegree ≤ max f.num.natDegree f.denom.natDegree