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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
x✝ : Nonempty ↥s
y : X
y_F : y ∈ F
t : Fin n → ↥s
ht : ∀ (k : Fin n), y ∈ T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ y ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)

Tactic:
by simpa using ht

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
have : netMaxcard T F U n
      = sSup (WithTop.some '' Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      rw [netMaxcard, ← image_comp, sSup_image]
      simp only [mem_ofPred_eq, ENat.some_eq_natCast, Function.comp_apply]
      exact biSup_congr (fun _ _ ↦ rfl)

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = expGrowthInf fun x ↦ 1

Tactic:
coverEntropyInfEntourage

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthInf fun n ↦ ↑(coverMincard T F univ n)) = expGrowthInf fun x ↦ 1
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₂.refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) x_2)
⊢ ∀ᶠ (x_1 : α) in ↑u,
    ¬φ.Realize (fun i ↦ x i x_1)
        (Fin.snoc (fun i ↦ v i x_1)
          ((fun a ↦ Classical.epsilon fun m ↦ ¬φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) m)) x_1))

Tactic:
exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ #(L.Term (α ⊕ Fin 1)) ≠ 0

Tactic:
mk_ne_zero_iff

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ Nonempty (L.Term (α ⊕ Fin 1))
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
⊢ Function.Injective ⇑φ

Tactic:
by
  intro x y
  exact (φ.map_formula ((var 0).equal (var 1)) fun i => if i = 0 then x else y).1

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↥((closure L).toFun s) ≤ #(L.Term ↑s)

Tactic:
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)
Module: Mathlib.ModelTheory.Definability

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

Tactic:
← Finset.inf_set_eq_iInter

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = lift.{w, max w w'} #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'

Tactic:
lift_id'.{w, w'}

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ DefinableFun L A fun v ↦ if p v then f v else g v

Tactic:
let P : Set (Option α → M) := {w | p (w ∘ some)}

Goal state after:
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w | p (w ∘ some)}
⊢ DefinableFun L A fun v ↦ if p v then f v else g v
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ #↑N0 ≤ lift.{max (max (max (max u v) w) w') w, max (max (max u v) w) w'} #↑N0

Tactic:
lift_id

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ #↑N0 ≤ #↑N0
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: ⊢ IsUnit 1

Tactic:
exact isUnit_one

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : Cardinal.{u_1}
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n

Tactic:
by_cases h : ℵ₀ ≤ a
  · simp [h, (prime_of_aleph0_le h).isPrimePow]
  simp only [h, false_or, isPrimePow_nat_iff]
  lift a to ℕ using not_le.mp h
  rw [isPrimePow_def]
  refine
    ⟨?_, fun ⟨n, han, p, k, hp, hk, h⟩ =>
          ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact mod_cast h⟩⟩
  rintro ⟨p, k, hp, hk, hpk⟩
  have key : p ^ (1 : Cardinal) ≤ ↑a := by
    rw [← hpk]; apply power_le_power_left hp.ne_zero; exact mod_cast hk
  rw [power_one] at key
  lift p to ℕ using key.trans_lt natCast_lt_aleph0
  exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, mod_cast hpk⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ((aeval x) (minpoly F x))′ =
    (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′

Tactic:
conv_rhs => apply (@deriv_aeval_eq _ _ _ _ _ default.1 _ default.2 _ _).symm

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✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ((aeval x) (minpoly F x))′ = ((aeval x) (minpoly F x))′
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
⊢ s.Infinite

Tactic:
by
  refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)
  have := @Finite.instDiscreteTopology s _ _ hf.to_subtype
  exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

Goal state after:
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
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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
this : v₁ ∈ ⊥
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
IntermediateField.mem_bot

Goal state after:
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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
this : v₁ ∈ Set.range ⇑(algebraMap F K)
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ i, filtration ↑i = filtration ⊤

Tactic:
exact iSup_adjoin_eq_top

Goal state after:
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
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥

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
a✝ : (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥

Tactic:
· have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
    rw [← range_coe] at hi; exact (hi inferInstance).elim

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
a✝ : (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥
Module: Mathlib.FieldTheory.IsPerfectClosure

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

Tactic:
iterateFrobeniusEquiv_add_apply,

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

Goal state before:
pp: R : Type u
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ x, f.IsRoot x
x : R
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
by
    rcases le_total x 0 with (neg | pos)
    · exact .inr <| isSquare_of_nonneg (neg_nonneg_of_nonpos neg)
    · exact .inl <| isSquare_of_nonneg pos

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ (taylor r) p ∈ R[X]⁰

Tactic:
mem_nonZeroDivisors_iff_right

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ ∀ (x : R[X]), x * (taylor r) p = 0 → x = 0
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 : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
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_1 ↦
    match x_1 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
y : G
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
      | inl hy =>
        have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
        have hk' : H k = H j := And.right <| by simpa using hk
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
        exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
      | inr hy =>
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
hq' : (aeval α) q = 0
⊢ ↑(finrank K L) ≤ ↑(minpoly K α).natDegree

Tactic:
← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α),

Goal state after:
case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
hq' : (aeval α) q = 0
⊢ ↑(finrank K L) ≤ ↑(finrank K ↥K⟮α⟯)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
⊢ [IsGalois K L ∧ IsCyclic Gal(L/K),
      ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a),
      ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE

Tactic:
have : NeZero (Module.finrank K L) := NeZero.of_pos finrank_pos
  tfae_have 1 → 3
  | ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK
  tfae_have 3 → 2
  | ⟨α, ⟨a, ha⟩, hα⟩ => ⟨a, irreducible_X_pow_sub_C_of_root_adjoin_eq_top ha.symm hα,
      isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top hK ha.symm hα⟩
  tfae_have 2 → 1
  | ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L,
      isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩
  tfae_finish

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ↑(H i)
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D

Tactic:
rw [← (ht i hi.1 hi.2).2] at hi'

Goal state after:
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)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case zero
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : IsPurelyInseparable K L
inst✝¹ : FiniteDimensional K L
inst✝ : CharZero K
h✝ : ExpChar K 1
⊢ HasExponent K L

Tactic:
exact ⟨0, fun a ↦ surjective_algebraMap_of_isSeparable K L _⟩

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : LinearIndependent R j
⊢ A.LinearDisjoint B

Tactic:
rw [LinearIndependent] at hj

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
j : Fin (finrank R (↥A ⊗[R] ↥B)) → ↥(A ⊔ B)
hj : Function.Injective ⇑(Finsupp.linearCombination R j)
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ IsField (A ⊗[F] B)

Tactic:
obtain ⟨M, hM⟩ := Ideal.exists_maximal (A ⊗[F] B)
  apply not_imp_not.1 (Ring.ne_bot_of_isMaximal_of_not_isField hM)
  let K : Type (max v w) := A ⊗[F] B ⧸ M
  let : Field K := Ideal.Quotient.field _
  let i := IsScalarTower.toAlgHom F (A ⊗[F] B) K
  let fa := i.comp (Algebra.TensorProduct.includeLeft : A →ₐ[F] _)
  let fb := i.comp (Algebra.TensorProduct.includeRight : B →ₐ[F] _)
  replace H := H K fa fb
  simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra,
    Subalgebra.linearDisjoint_iff_injective] at H
  have hi : i = (fa.range.mulMap fb.range).comp (Algebra.TensorProduct.congr
      (AlgEquiv.ofInjective fa fa.injective) (AlgEquiv.ofInjective fb fb.injective)) := by
    ext <;> simp [fa, fb]
  replace H : Function.Injective i := by simpa only
    [hi, AlgHom.coe_comp, AlgEquiv.coe_toAlgHom, EquivLike.injective_comp, fa, this, K, fb]
  change Function.Injective (Ideal.Quotient.mk M) at H
  rwa [RingHom.injective_iff_ker_eq_bot, Ideal.mk_ker] at H

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

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ ↑(-x).num.natDegree - ↑(-x).denom.natDegree = ↑x.num.natDegree - ↑x.denom.natDegree

Tactic:
← natDegree_neg x.num

Goal state after:
case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ ↑(-x).num.natDegree - ↑(-x).denom.natDegree = ↑(-x.num).natDegree - ↑x.denom.natDegree
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (aeval X) (f.minpolyX ↥K⟮f⟯) = 0

Tactic:
by
  simp only [aeval_sub, aeval_map_algebraMap, aeval_X_left_eq_algebraMap, map_mul, aeval_C,
    IntermediateField.algebraMap_apply, coe_algebraMap]
  nth_rw 2 [← num_div_denom f]
  rw [div_mul_cancel₀ _ (algebraMap_ne_zero f.denom_ne_zero)]
  exact sub_self _

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ Irreducible (f.minpolyX ↥K⟮f⟯)

Tactic:
← f.minpolyX_map K[f] K⟮f⟯,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ Irreducible (Polynomial.map (algebraMap ↥K[f] ↥K⟮f⟯) (f.minpolyX ↥K[f]))