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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst✝ : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : ν₁ univ = (a • ν₁ + b • ν₂) univ
hν₂μ : ν₂ univ = (a • ν₁ + b • ν₂) univ
⊢ (a • ν₁ + b • ν₂) univ < ∞

Tactic:
apply measure_lt_top

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
hx : x ∈ mulForbidden F
⊢ mulShift h x ∈ mulForbidden F

Tactic:
p

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
hx : x ∈ mulForbidden F
p : Pattern A G
⊢ p ∈ F → ∀ (g : G), ¬p.mulOccursInAt (mulShift h x) g
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
w✝¹ : τ
ht : w✝¹ ∈ i✝
w✝ : α
hx : w✝ ∈ s
hϕtx : w✝ ∈ ϕ w✝¹ ⁻¹' t✝
⊢ (t✝ ∩ image2 ϕ i✝ s).Nonempty

Tactic:
exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩

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

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
⊢ xy ∈ (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V →
    xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)

Tactic:
xy_comp

Goal state after:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : xy ∈ (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)
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
F_nemp : F.Nonempty
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
have _ : Nonempty X := F_nemp.nonempty

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
F_nemp : F.Nonempty
x✝ : Nonempty X
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ coverMincard T F U n < ⊤

Tactic:
obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_uniformContinuous F_comp h U_uni n
  exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy (MapsTo.restrict T G G hG) (val ⁻¹' F) = coverEntropy T F

Tactic:
← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F),

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy T (val '' val ⁻¹' F) = coverEntropy T F
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone fun F ↦ coverEntropyEntourage T F U

Tactic:
by
  refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : (coverEntropySupBotHom T) (s.sup F) = s.sup (⇑(coverEntropySupBotHom T) ∘ F)
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)

Tactic:
s.sup_set_eq_biUnion,

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : (coverEntropySupBotHom T) (⋃ x ∈ s, F x) = s.sup (⇑(coverEntropySupBotHom T) ∘ F)
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun x ↦ x.toHom

Tactic:
intro f f' h
  ext
  exact congr_fun (congr_arg (↑) h) _

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
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 : ℕ} (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)

Tactic:
intro n

Goal state after:
case refine_1
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 : ℕ
⊢ ∀ (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2
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 : ℕ} (r : L[[↑A]].Relations n) (x : Fin n → M), RelMap r (f.toFun ∘ x) ↔ RelMap r x

Tactic:
intro n

Goal state after:
case refine_2
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 : ℕ
⊢ ∀ (r : L[[↑A]].Relations n) (x : Fin n → M), RelMap r (f.toFun ∘ x) ↔ RelMap r x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
⊢ Function.Injective fun f ↦ f.comp h

Tactic:
by
  intro f g hfg
  convert! (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg) <;>
    rw [comp_assoc, self_comp_symm, comp_refl]

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

Goal state before:
pp: case existsPairNE
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K existsPairNE

Tactic:
exact exists_pair_ne K

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)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default

Tactic:
← realize_formula_cast φ,

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)
φ : L.Sentence
⊢ Formula.Realize φ default ↔ Formula.Realize φ fun i ↦ Quotient.mk' fun a ↦ default i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (do
        let a ← (listDecode t.listEncode).head?
        pure (some a)).join =
    some t

Tactic:
have h := listDecode_encode_list [t]

Goal state after:
L : Language
α : Type u'
t : L.Term α
h : listDecode (flatMap listEncode [t]) = [t]
⊢ (do
        let a ← (listDecode t.listEncode).head?
        pure (some a)).join =
    some t
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
f : M ↪ₑ[L] N
A : Set M
⊢ ∀ ⦃n : ℕ⦄ (φ : L[[↑A]].Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
intro n

Goal state after:
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
f : M ↪ₑ[L] N
A : Set M
n : ℕ
⊢ ∀ (φ : L[[↑A]].Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
h : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
⊢ ∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
intro n

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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
h : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
n : ℕ
⊢ ∀ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
⊢ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f ∅

Tactic:
intro n

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
n : ℕ
⊢ ∀ (f : L.Functions n), ClosedUnder f ∅
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs

Tactic:
intro n

Goal state after:
case refine_5
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ : L.BoundedFormula Empty n✝
n : ℕ
⊢ ∀ (f_1 : L.BoundedFormula Empty (n + 1)),
    (∀ (xs : Fin (n + 1) → M), f_1.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f_1.Realize default xs) →
      ∀ (xs : Fin n → M), (∀' f_1).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' f_1).Realize default xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
Formula.iAlls

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a ↦ Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls.Realize v ↔
    ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥((closure L).toFun A)) (a : M),
    φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
intro n

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
⊢ ∀ (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥((closure L).toFun A)) (a : M),
    φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LHom.sumInl.substructureReduct S)) (a : M),
    φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
intro n

Goal state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
⊢ ∀ (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LHom.sumInl.substructureReduct S)) (a : M),
    φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ Std.Refl fun x y ↦ RelMap r ![x, y]

Tactic:
by
  rw [refl_def]
  exact forall_congr' fun _ ↦ realize_rel₂

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.total ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] ∨ RelMap r ![b, a]

Tactic:
exact forall₂_congr fun _ _ ↦ realize_sup.trans <| or_congr realize_rel₂ realize_rel₂

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤
            (List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize
        default xs) ↔
    Nonempty (Fin n ↪ M)

Tactic:
BoundedFormula.realize_foldr_inf

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      ∀
        φ ∈
          List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)),
        φ.Realize default xs) ↔
    Nonempty (Fin n ↪ M)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case intro
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ

Tactic:
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2

Goal state after:
case intro
L : Language
T : L.Theory
M : T.ModelType
MI : Infinite ↑M
N : Bundled L.Structure
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #↑N
⊢ ∃ N_1, #↑N_1 = #↑N
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
models_iff_not_satisfiable

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
by
  have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)
  let M' : ModelType T' := ⟨M⟩
  exact hφ M'

Goal state after:
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:
empty.nonempty_equiv_iff,

Goal state after:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ lift.{w, w} #↑M = lift.{w, w} #↑N
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : Cardinal.{u}
⊢ IsUnit a ↔ a = 1

Tactic:
refine
    ⟨fun h => ?_, by
      rintro rfl
      exact isUnit_one⟩
  rcases eq_or_ne a 0 with (rfl | ha)
  · exact (not_isUnit_zero h).elim
  rw [isUnit_iff_forall_dvd] at h
  obtain ⟨t, ht⟩ := h 1
  rw [eq_comm, mul_eq_one_iff_of_one_le] at ht
  · exact ht.1
  · exact Cardinal.one_le_iff_ne_zero.mpr ha
  · apply Cardinal.one_le_iff_ne_zero.mpr
    intro h
    rw [h, mul_zero] at ht
    exact zero_ne_one ht

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

Goal state before:
pp: case inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

pp: case inr.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

pp: case inr.inr
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk; simp [hk]

Goal state after:
case inr.inr
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
⊢ let S := zeroLocus K I;
  Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S

Tactic:
by
  let := compatibleRingOfRing K
  intro S
  obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I
  exact ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (expand p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) = (expand p) p✝ * X n✝ ^ p

Tactic:
frobenius_def

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (expand p) p✝ * X n✝ ^ p = (expand p) p✝ * X n✝ ^ p
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
⊢ ∀ (i : σ), Multiset.count i (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1

Tactic:
intro n

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ b ∈ Finset.univ, b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

Tactic:
intro b _ ne
      simp [ne, eqComm]

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
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
⊢ ↑a = ∑ x, ↑(c₀ x) * logDeriv (u₀ x) + v₀′

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
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 : ι₀), (c₀ x)′ = 0

Tactic:
· rw [h₀]
      simp [hc]

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
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 : ι₀), (c₀ x)′ = 0
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ 2 ^ Module.rank F E ≤ Cardinal.prod fun i ↦ #(Cardinal.factor ↑i)

Tactic:
conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Goal state after:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun x ↦ 2) ≤ Cardinal.prod fun i ↦ #(Cardinal.factor ↑i)
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
x : L
⊢ ∃ y, i y.2 = x ^ p ^ y.1

Tactic:
obtain ⟨n, y, h⟩ := IsPRadical.pow_mem i p x

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
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ ∃ y, i y.2 = x ^ p ^ y.1
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
obtain ⟨w, ih⟩ := ih

Goal state after:
case mp.symm
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : Relation.EqvGen (R K p) x y
w : ℕ
ih : (⇑(frobenius K p))^[y.1 + w] x.2 = (⇑(frobenius K p))^[x.1 + w] y.2
⊢ ∃ z, (⇑(frobenius K p))^[x.1 + z] y.2 = (⇑(frobenius K p))^[y.1 + z] x.2