mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)

pp: case e'_7
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict s

Tactic:
· refine singularPart_eq_restrict ?_ (hfν.preimage_null hνs)
    rw [← mem_ae_iff, ← Filter.eventuallyEq_univ,
      ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]
    calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]

Goal state after:
case e'_7
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x

Tactic:
ext1 s hs
    rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
    conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
    rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
    · congr with x
      rw [mul_comm]
      simp only [Pi.mul_apply]
    · refine ae_restrict_of_ae ?_
      exact Measure.rnDeriv_lt_top _ _
    · exact (Measure.measurable_rnDeriv _ _).aemeasurable

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 = netMaxcard T F U n

Tactic:
rw [← k_max]

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
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = ↑k
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

pp: case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Tactic:
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

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

Goal state before:
pp: case inr.inr.refine_2
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
⊢ #sn.toFinset ≤ #s ^ n

Tactic:
· rw [toFinset_card]
    apply (Fintype.card_range_le dyncover).trans
    simp only [Fintype.card_fun, Fintype.card_coe, Fintype.card_fin, le_refl]

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 = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
rw [← WithTop.coe_sSup' h_bdda] at k_max

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 = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
⊢ netMaxcard T ∅ U n = 0

Tactic:
netMaxcard_empty

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : F = ∅
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
suffices μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ) by
    calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)
  rw [withDensity_rnDeriv_eq _ _ hνμ, ← withDensity_rnDeriv_eq _ _ hμν]
  conv in ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ => rw [withDensity_rnDeriv_eq _ _ hμν]
  change (ν.withDensity (μ.rnDeriv ν)).withDensity (fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν
  rw [withDensity_inv_same (measurable_rnDeriv _ _)
    (by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne')
    (rnDeriv_ne_top _ _)]

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

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ coverMincard T F U m ^ 0

Tactic:
mul_zero,

Goal state after:
case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) 0 ≤ coverMincard T F U m ^ 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
rw [h3]

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
⊢ coverEntropy T (closure F) = coverEntropy T F

Tactic:
by
  refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropy_monotone T subset_closure)
  obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
  exact le_iSup₂_of_le V V_uni ((coverEntropyEntourage_antitone T (closure F) V_U).trans
    (coverEntropyEntourage_closure h F V V_uni))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
⊢ ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹ →
    μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1) →
      μ.rnDeriv ν a < ∞ → μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
ha1

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1) →
    μ.rnDeriv ν a < ∞ → μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : 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
φ : L.Formula β
x : β → (a : α) → M a
⊢ (φ.Realize fun i ↦ Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i ↦ x i a

Tactic:
simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]

Goal state after:
α : 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
φ : L.Formula β
x : β → (a : α) → M a
⊢ BoundedFormula.Realize φ (fun i ↦ Quotient.mk' (x i)) default =
    BoundedFormula.Realize φ (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' fun a ↦ default i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l

Tactic:
induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
hnp : N ↪ₑ[L] P
hmn : M ↪ₑ[L] N
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((⇑hnp ∘ ⇑hmn) ∘ x) ↔ φ.Realize x

Tactic:
by simp [Function.comp_assoc]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (R.formula₁ t).Realize v ↔ RelMap R ![Term.realize v t]

Tactic:
rw [Relations.formula₁, realize_rel, iff_eq_eq]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap R fun i ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ⨆ i, S i = ⨆ i, (closure L).toFun ↑(S i)

Tactic:
closure_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'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ Realize f✝.toFormula
      (Sum.elim v (snoc default a ∘ castAdd 0) ∘
        Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm))
      (snoc default a ∘ natAdd 1) =
    Realize f✝.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) default

Tactic:
simp only [Function.comp_def]

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (Realize f✝.toFormula
      (fun x ↦
        Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
          (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x)) x))
      fun x ↦ snoc default a (natAdd 1 x)) =
    Realize f✝.toFormula (Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a)) default
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
⊢ (listDecode φ.snd.listEncode)[0]? = some φ

Tactic:
by
    have h := listDecode_encode_list [φ]
    rw [flatMap_singleton] at h
    rw [h]
    rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
f : (α → M) → M
⊢ DefinableFun L ∅ f ↔ ∃ φ, tupleGraph f = ofPred φ.Realize

Tactic:
simp [DefinableFun, Set.empty_definable_iff]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsSatisfiable (⋃ i, T i)

Tactic:
isSatisfiable_iff_isFinitelySatisfiable

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsFinitelySatisfiable (⋃ i, T i)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)

Tactic:
by rw [empty.nonempty_equiv_iff, hM, hN]

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

Goal state before:
pp: n : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False

Tactic:
rw [h, zero_dvd_iff, mul_eq_zero] at hbc

Goal state after:
n : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b = 0 ∨ c = 0
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False
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 : ∃ 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

Tactic:
rcases hS with ⟨c, _, hS⟩

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)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
hS : (↑c).Definable ring S
⊢ 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.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (indicator c).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}

Tactic:
rw [indicator]
  classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_1
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 j : (Module.rank F E).ord.ToType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)

Tactic:
exact strictMono_leastExt hj

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
i : K →+* L
p : ℕ
inst✝² : IsPRadical i p
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : L
⊢ liftAux i i p x = x

Tactic:
liftAux,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
i : K →+* L
p : ℕ
inst✝² : IsPRadical i p
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : L
⊢ (iterateFrobeniusEquiv L p (Classical.choose ⋯).1).symm (i (Classical.choose ⋯).2) = x
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ liftAux (RingHom.id K) j p x = j x

Tactic:
liftAux,

Goal state after:
K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) = j x
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm ((iterateFrobeniusEquiv M p n2) (j y1)) *
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm ((iterateFrobeniusEquiv M p n2).symm ((iterateFrobeniusEquiv M p n2) (j y1))) *
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm ((iterateFrobeniusEquiv M p n2) (j y1)) +
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm ((iterateFrobeniusEquiv M p n2).symm ((iterateFrobeniusEquiv M p n2) (j y1))) +
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
⊢ ∃ t, IsComplement ↑t ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H

Tactic:
have hf : t.Finite := ht.1.finite_left_iff.mpr inferInstance

Goal state after:
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
⊢ ∃ t, IsComplement ↑t ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
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, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep
  have nzero : n ≠ 0 := by
    rintro rfl
    rw [pow_zero, pow_one] at hn
    exact ha hn
  exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : b * ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = b * 0
⊢ m i = 0

Tactic:
mul_zero,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : b * ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
⊢ m i = 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
x✝ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x) ∨ y ∈ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x)
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with

Goal state after: