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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝 0)

Tactic:
replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
        (tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hu₂ : Tendsto (fun j ↦ T⁻¹ * 2 * ↑(n j)) l atTop
⊢ Tendsto δ l (𝓝 0)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑s
⊢ ∃ a, s = AddSubgroup.zmultiples a

Tactic:
by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : IsMinimal M α
⊢ IsTopologicallyTransitive M α

Tactic:
refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr fun h hn ↦ ?_
  simp only [h.iUnion_preimage_smul M hn, dense_univ]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (a ^ c) ^ d = (a ^ d) ^ c

Tactic:
← pow_mul,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ a ^ (c * d) = (a ^ d) ^ c
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ (sum fun x ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
sum_const,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] * lift.{u, v} ℵ₀ = lift.{v, u} #R[X] * ℵ₀
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ ∃ m, map i (X ^ n - 1) = C (map i (X ^ n - 1)).leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

Tactic:
leadingCoeff_map

Goal state after:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ ∃ m, map i (X ^ n - 1) = C (i (X ^ n - 1).leadingCoeff) * (Multiset.map (fun x ↦ X - C x) m).prod
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e.invLHom.comp ((LHom.id L').comp e.toLHom) = LHom.id L

Tactic:
LHom.id_comp,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e.invLHom.comp e.toLHom = LHom.id L
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp ((LHom.id L').comp e'.invLHom) = LHom.id L''

Tactic:
LHom.id_comp,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e'.toLHom.comp e'.invLHom = LHom.id L''
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2.inr
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
r : (constantsOn ↑A).Relations n
⊢ RelMap (Sum.inr r) (f.toFun ∘ x) ↔ RelMap (Sum.inr r) x

Tactic:
exact isEmptyElim r

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), relabel id (_ts✝ a) = _ts✝ a
⊢ relabel id (func _f✝ _ts✝) = func _f✝ _ts✝

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), relabel g (relabel f (_ts✝ a)) = relabel (g ∘ f) (_ts✝ a)
⊢ relabel g (relabel f (func _f✝ _ts✝)) = relabel (g ∘ f) (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (LHom.id L).onTerm (_ts✝ a) = id (_ts✝ a)
⊢ (LHom.id L).onTerm (func _f✝ _ts✝) = id (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), (φ.comp ψ).onTerm (_ts✝ a) = (φ.onTerm ∘ ψ.onTerm) (_ts✝ a)
⊢ (φ.comp ψ).onTerm (func _f✝ _ts✝) = (φ.onTerm ∘ ψ.onTerm) (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), realize v ((_ts✝ a).subst tf) = realize (fun a ↦ realize v (tf a)) (_ts✝ a)
⊢ realize v ((func _f✝ _ts✝).subst tf) = realize (fun a ↦ realize v (tf a)) (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinset → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinset), v (f a_1) = v' ↑a_1) → realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinset → β
hv' : ∀ (a : ↥(func _f✝ _ts✝).varFinset), v (f a) = v' ↑a
⊢ realize v ((func _f✝ _ts✝).restrictVar f) = realize v' (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice fun i ↦ ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
rw [Quotient.finChoice_eq, Quotient.map_mk]

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: case func
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
ih : ∀ (a : Fin l✝), realize (fun i ↦ ⟦x i⟧) (_ts✝ a) = ⟦realize x (_ts✝ a)⟧
⊢ realize (fun i ↦ ⟦x i⟧) (func _f✝ _ts✝) = ⟦realize x (func _f✝ _ts✝)⟧

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinsetLeft → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' ↑a_1) →
      realize xs ((_ts✝ a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinsetLeft → β
hxs' : ∀ (a : ↥(func _f✝ _ts✝).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs ((func _f✝ _ts✝).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (func _f✝ _ts✝)

Tactic:
| func _ _ ih =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case imp
α : 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
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin n✝ → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) →
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a) ↔
    ∀ᶠ (a : α) in ↑u, (f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) → f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
Ultrafilter.eventually_imp

Goal state after:
case imp
α : 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
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin n✝ → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) →
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a) ↔
    (∀ᶠ (x_1 : α) in ↑u, f₁✝.Realize (fun i ↦ x i x_1) fun i ↦ v i x_1) →
      ∀ᶠ (x_1 : α) in ↑u, f₂✝.Realize (fun i ↦ x i x_1) fun i ↦ v i x_1
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
⊢ BoundedFormula.Realize φ (fun i ↦ Quotient.mk' (x i)) default ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i ↦ x i a) default

Tactic:
← boundedFormula_realize_cast φ x,

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 α)
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode l) = l

Tactic:
by
    induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Goal state after:
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
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
classical
    rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
    have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
    simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
    rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h
    refine h.trans ?_
    rw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self,
      Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs,
      BoundedFormula.realize_restrictFreeVar v (by simp)]

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case H
L : Language
n : ℕ
f g : L.Functions n
h : (fun f ↦ func f default =' func f default) f = (fun f ↦ func f default =' func f default) g
⊢ f = g

Tactic:
rcases h with ⟨rfl, ⟨rfl⟩⟩

Goal state after:
case H
L : Language
n : ℕ
f : L.Functions n
⊢ f = f
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ (constantsOn α).card ≤ ℵ₀

Tactic:
simpa only [card_constantsOn, mk_le_aleph0_iff]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
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✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R✝ fun i ↦ g (Term.realize (Sum.elim v xs) (ts✝ i))) ↔ RelMap R✝ fun i ↦ Term.realize (Sum.elim v xs) (ts✝ i)

Tactic:
exact StrongHomClass.map_rel g _ _

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) T
⊢ IsSatisfiable (⋃ i, T i) ↔ ∀ (i : ι), (T i).IsSatisfiable

Tactic:
by
  refine ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩
  rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
  intro T0 hT0
  obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
  exact (h' i).mono hi

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R

Tactic:
lift_id,

Goal state after:
R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ max #↥S #R = #R
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : #(OreLocalization S X) ≤ lift.{u, v} (lift.{v, v} #X * lift.{v, v} #X)
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
lift_id,

Goal state after:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : #(OreLocalization S X) ≤ lift.{u, v} (#X * #X)
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_3
E : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Field L
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra K L
inst✝³ : Algebra E L
inst✝² : IsScalarTower K E L
inst✝¹ : FinTrdeg K E
inst✝ : FinTrdeg E L
⊢ FinTrdeg K L

Tactic:
finTrdeg_iff_trdeg,

Goal state after:
K : Type u_3
E : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Field L
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra K L
inst✝³ : Algebra E L
inst✝² : IsScalarTower K E L
inst✝¹ : FinTrdeg K E
inst✝ : FinTrdeg E L
⊢ Algebra.trdeg K L < Cardinal.aleph0
Module: Mathlib.FieldTheory.FinTrdeg

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

Tactic:
finTrdeg_iff_trdeg,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Algebra.trdeg K L < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case succ
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
ih : ∀ {x : Extension k p n}, (frob k p n ^ i) x = x ^ Nat.card k ^ i
x : Extension k p n
⊢ (x ^ Nat.card k) ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)

Tactic:
← pow_mul,

Goal state after:
case succ
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
ih : ∀ {x : Extension k p n}, (frob k p n ^ i) x = x ^ Nat.card k ^ i
x : Extension k p n
⊢ x ^ (Nat.card k * Nat.card k ^ i) = x ^ Nat.card k ^ (i + 1)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ #↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1} = #↑{s | ∀ (n : σ), s n < Fintype.card K}

Tactic:
by
      refine Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩
      refine forall_congr' fun n => le_tsub_iff_right ?_
      exact Fintype.card_pos_iff.2 ⟨0⟩

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap) ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
      ((fun x ↦ x ^ ↑i) X) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)

Tactic:
toSpanSingleton_apply,

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (fun x ↦ x ^ ↑i) X • (AEval'.of (frobeniusAlgHom K L).toLinearMap) x =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)
Module: Mathlib.FieldTheory.Galois.NormalBasis

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
inst✝ : IsGalois K L
e : Gal(L/K)
⊢ e ⋯.choose = e (1 ⋯.choose)

Tactic:
AlgEquiv.one_apply

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
e : Gal(L/K)
⊢ e ⋯.choose = e ⋯.choose
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : WithTop (Module.rank F E).ord.ToType
h : i < j
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases j
    · obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne
      exact ⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩
    · obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp (h.trans <| coe_lt_top _).ne
      exact strictMono_filtration (coe_lt_coe.mp h)

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
x y : R
⊢ x - y ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = y ^ p ^ n

Tactic:
by
  simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

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

Tactic:
← pow_mul,

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 : x ^ (p ^ n * p ^ n') = i y ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.refl
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y H : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[H.1 + z] H.2 = (⇑(frobenius K p))^[H.1 + z] H.2

Tactic:
| refl H =>

Goal state after: