mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᵐ[volume] ball x ε

Tactic:
· suffices volume (closedBall x ε) ≤ volume (ball x ε) from
      (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this
        measurableSet_ball.nullMeasurableSet (measure_ne_top _ _)).symm
    have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) := by
      simp_rw [volume_closedBall]
      refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
      exact nhdsWithin_le_nhds
    refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_
    exact measure_mono (closedBall_subset_ball hr.2)

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ c • μ[univ | s] = c

Tactic:
(cond_isProbabilityMeasure hμs).1,

Goal state after:
case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ c • 1 = c
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
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
t : Fin n → ↥s
y z : X
y_int : ∀ (i : Fin n), ∀ i_1 < m, (T^[i_1] ↑(t i), T^[i_1] (T^[m * ↑i] y)) ∈ U
k : ℕ
k_mn : k / m < n
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U

Tactic:
specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)

Goal state after:
case inr
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
t : Fin n → ↥s
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] y)) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k % m] (T^[m * ↑⟨k / m, k_mn⟩] z)) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ s, ⨅ (_ : IsDynCoverOf T F U n ↑s), ↑(#s)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
iInf_subtype'

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
classical
  rcases isEmpty_or_nonempty X with _ | _
  · exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le⟩⟩
  -- If `t` is a dynamical cover of `φ '' F`, then we want to choose one preimage by `φ` for each
  -- element of `t`. This is complicated by the fact that `t` may not be a subset of `φ '' F`,
  -- and may not even be in the range of `φ`. Hence, we first modify `t` to make it a subset
  -- of `φ '' F`. This requires taking larger entourages.
  obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter
  choose! g g_rel g_mem using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)
  choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ hy
  refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
  simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
    mem_preimage, map_apply, exists_exists_and_eq_and]
  obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)
  refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩
  rw [φ_f _ (g_mem _ hy)]
  exact g_rel _ hy

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ (refl L M).toHom = Hom.id L M

Tactic:
refl_toHom

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ Hom.id L M = Hom.id L M
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ (refl L N).toHom = Hom.id L N

Tactic:
refl_toHom

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ Hom.id L N = Hom.id L N
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
h : n✝ ≤ n✝
⊢ castLE h falsum = falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
k n✝ : ℕ
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km falsum) = castLE ⋯ falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) falsum) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) falsum = falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) falsum = castLE ⋯ falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ (LHom.id L).onBoundedFormula falsum = id falsum

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K 0
⊢ K ⊨ if 0 = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime 0 then {eqZero 0} else {⊥}

Tactic:
simp only [ite_true, Theory.model_iff, Set.mem_image, Set.mem_ofPred_eq,
      Sentence.Realize, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      Formula.realize_not, realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K 0
⊢ CharZero K
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case falsum
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
⊢ (φ.comp ψ).onBoundedFormula falsum = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum

Tactic:
| falsum =>

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
⊢ ⊤.Realize v xs ↔ True

Tactic:
simp [Top.top]

Goal state after:
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)
n : ℕ
f : L.Functions n
x : Fin n → (a : α) → M a
⊢ (funMap f fun i ↦ Quotient.mk' (x i)) = Quotient.mk' fun a ↦ funMap f fun i ↦ x i a

Tactic:
by
  apply funMap_quotient_mk'

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

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

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Tactic:
by
  subst h
  simp only [castLE_rfl, cast_refl, Function.comp_id]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) falsum).Realize v' xs ↔ falsum.Realize v xs

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) falsum).Realize v' xs ↔ falsum.Realize (v xs) (xs ∘ natAdd k)

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
xs : Fin (n✝ + n') → M
hmn : m ≤ n✝
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) falsum).Realize v xs ↔
    falsum.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
| falsum =>

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
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)

Goal state after:
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
h :
  (Formula.relabel (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) (φ.restrictFreeVar id).toFormula).Realize
      (↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ↔
    (Formula.relabel (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) (φ.restrictFreeVar id).toFormula).Realize
      (Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{u, w} #↥((closure L).toFun s) ≤ max ℵ₀ (lift.{u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
← lift_umax

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max w u, w} #↥((closure L).toFun s) ≤ max ℵ₀ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
xs : Fin n✝ → M
⊢ (φ.onBoundedFormula falsum).Realize v xs ↔ falsum.Realize v xs

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case falsum
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l') = ⟨n✝, falsum⟩ :: listDecode l'

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
v : α ⊕ Fin n✝ → M
⊢ falsum.toFormula.Realize v ↔ falsum.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : ∅.Definable L[[↑A]] s
hAB : A ⊆ B
⊢ ∅.Definable L[[↑B]] s

Tactic:
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse (fun g ↦ g ∘ ⇑f.symm) fun g ↦ g ∘ ⇑f

Tactic:
intro i
    ext a
    simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
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✝ : ℕ
xs : Fin n✝ → M
⊢ BoundedFormula.falsum.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ BoundedFormula.falsum.Realize v xs

Tactic:
| falsum =>

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (F ⁻¹' S)

Tactic:
have h_graph : A.Definable L { w : α ⊕ β → M | ∀ i, F (w ∘ Sum.inl) i = w (Sum.inr i) } := by
    rw [ofPred_forall]
    refine definable_iInter_of_finite fun i => ?_
    simpa [tupleGraph] using!
      (hF i).preimage_comp (fun | none => Sum.inr i | some j => Sum.inl j)
  have h_cyl : A.Definable L { w : α ⊕ β → M | w ∘ Sum.inr ∈ S } :=
    hS.preimage_comp Sum.inr
  convert! Definable.exists_of_finite (Definable.inter h_graph h_cyl) using 1
  ext v
  simp [← funext_iff]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
· exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T

Tactic:
exact ⟨h, inferInstance⟩

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs

Tactic:
by
  have h' : φ.toFormula.Realize (Sum.elim v xs) := (models_toFormula_iff.2 h).realize_formula M
  simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'
  exact h'

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
⊢ T.IsComplete → T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
intro hcomp
    refine ⟨hcomp.1, ?_⟩
    intro M N
    rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]

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

Goal state before:
pp: case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1

Tactic:
exact (one_lt_aleph0.trans_le ha).ne'

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

Goal state before:
pp: case inj
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
⊢ Function.Injective fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1

Tactic:
· apply (add_right_injective _).comp
    apply mul_right_injective₀
    rw [ne_eq, ← minpoly.dvd_iff]
    have : 0 < (minpoly F x).natDegree := Irreducible.natDegree_pos
      (minpoly.irreducible (Algebra.IsIntegral.isIntegral _))
    apply not_dvd_of_natDegree_lt
    · intro nh
      simp_all
    apply natDegree_derivative_lt
    exact Nat.ne_zero_of_lt this

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

Goal state before:
pp: case inj
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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ Function.Injective Algebra.cast

Tactic:
apply FaithfulSMul.algebraMap_injective

Goal state after:
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 S ↥(F.extendRight M)) x) = ↑((F.extendRightEquiv' M R) ((algebraMap S ↥F) x))

Tactic:
← algebraMap_apply (F.extendRight M),

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 (↥(F.extendRight M)) M) ((algebraMap S ↥(F.extendRight M)) x) =
    ↑((F.extendRightEquiv' M R) ((algebraMap S ↥F) x))
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) =
    ↑((F.extendRightEquiv' M R) ((algebraMap S ↥F) x))

Tactic:
← algebraMap_apply (F.extendRight M),

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 (↥(F.extendRight M)) M) ((algebraMap S ↥(F.extendRight M)) x) =
    (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv' M R) ((algebraMap S ↥F) x))
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 + (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_add]
      apply R.intro

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0

Tactic:
rwa [hp, one_pow, pow_one] at h

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
obtain ⟨n, y, hy⟩ := pow_mem f p x

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n
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
⊢ i 1 = 1 ^ p ^ 0

Tactic:
rw [one_pow, map_one]

Goal state after: