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

Goal state before:
pp: X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
by
  classical
  -- WLOG, there exists a maximal dynamical net `s`.
  rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  have larger_net : IsDynNetIn T F U n (insert x s) := by
    refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
    refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
    exact mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))

Goal state after:
Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ ((fun x1 x2 ↦ x1 * x2) a b)⁻¹ * (fun x1 x2 ↦ x1 * x2) b a ∈ (commutator G).topologicalClosure

Tactic:
h

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ ⁅b⁻¹, a⁻¹⁆ ∈ (commutator G).topologicalClosure
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) = μ (f ⁻¹' f '' s)

Tactic:
← hf.restrict_map,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β) in f '' s, (map f μ).rnDeriv (map f ν) a ∂map f ν = μ (f ⁻¹' f '' s)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ Nonempty (K ≃+* L)

Tactic:
let : Algebra (ZMod p) L := ZMod.algebra _ _

Goal state after:
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
⊢ Nonempty (K ≃+* L)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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
C_mul_C : C (i a⁻¹) * C (i a) = 1
⊢ X ^ n - 1 = C (i a⁻¹) * ((C b * X) ^ n - C (i a))

Tactic:
mul_pow,

Goal state after:
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
C_mul_C : C (i a⁻¹) * C (i a) = 1
⊢ X ^ n - 1 = C (i a⁻¹) * (C b ^ n * X ^ n - C (i a))
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 f' : M ↪[L] N
⊢ (fun x ↦ x.toHom) f = (fun x ↦ x.toHom) f' → f = f'

Tactic:
h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x ↦ x.toHom) f = (fun x ↦ x.toHom) f'
⊢ f = f'
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
⊢ a₁✝.toEmbedding = a₂✝.toEmbedding → a₁✝ = a₂✝

Tactic:
h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ a₁✝ = a₂✝
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:
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.CharP

Goal state before:
pp: case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize,
      forall_eq, Formula.realize_bot, false_iff]

Goal state after:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ ¬CharP K p
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
f : L[[α]].Functions (n✝ + 1)
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun i ↦ y i a

Tactic:
← funext ha2

Goal state after:
case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 ↦ x x_1 a
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: 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 : ℕ
φ : L.BoundedFormula α n
v : α → M
v' : β → M
xs : Fin n → 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
⊢ (mapTermRel ft fr (fun x ↦ id) φ).Realize v' xs ↔ φ.Realize v xs

Tactic:
by
  induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel, Realize, h1]
  | rel => simp [mapTermRel, Realize, h1, h2]
  | imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
  | all _ ih => simp only [mapTermRel, Realize, ih, id]

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
h :
  (φ.restrictFreeVar id).Realize (↑f ∘ v ∘ Subtype.val) ((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inr) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
Function.comp_assoc _ _ Sum.inr,

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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
⊢ realize (Sum.elim v x) (t.subst (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr))) =
    realize (Sum.elim (fun a ↦ realize v (tf a)) x) t

Tactic:
Term.realize_subst

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
⊢ realize (fun a ↦ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun a ↦ realize v (tf a)) x) t
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h : a = b
⊢ Sum.inl a = Sum.inl b

Tactic:
h

Goal state after:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h : a = b
⊢ Sum.inl b = Sum.inl b
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ funMap f (⇑φ ∘ x) = φ (funMap f x)

Tactic:
h

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ funMap f x = funMap f x
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
n : ℕ
ψ : L.BoundedFormula α n
h : m = n
⊢ L.BoundedFormula α n = L.BoundedFormula α m

Tactic:
h

Goal state after:
L : Language
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
n : ℕ
ψ : L.BoundedFormula α n
h : m = n
⊢ L.BoundedFormula α n = L.BoundedFormula α n
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
n₁ : ℕ
t₁ : L.Term (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : L.Term (α ⊕ Fin n₂)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : n₁ = n₂
⊢ L.Term (α ⊕ Fin n₂) = L.Term (α ⊕ Fin n₁)

Tactic:
h

Goal state after:
L : Language
α : Type u'
n₁ : ℕ
t₁ : L.Term (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : L.Term (α ⊕ Fin n₂)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : n₁ = n₂
⊢ L.Term (α ⊕ Fin n₂) = L.Term (α ⊕ Fin n₂)
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
h : ∅ ∈ (closure L).closed
⊢ x ∉ ↑((closure L).toFun ∅)

Tactic:
h

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
h : ∅ ∈ (closure L).closed
⊢ x ∉ ∅
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔ M ⊨ φ

Tactic:
refine _root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a ↦ ↑(L.con a)) default) default
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)

Tactic:
rw [← StrongHomClass.realize_formula Substructure.topEquiv φ]
  simp

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5.refine_2
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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : M), φ.Realize default (Fin.snoc xs a)) → ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)

Tactic:
· contrapose!
      rintro ⟨a, ha⟩
      obtain ⟨b, hb⟩ := htv n φ.not xs a (by
          rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
          exact ha)
      refine ⟨b, fun h => hb (Eq.mp ?_ ((ih _).2 h))⟩
      rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
h

Goal state after:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h : listDecode φ.snd.listEncode = [φ]
⊢ [φ][0]? = some φ
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:
h

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
h : φ.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: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s') ∧
    ℵ₀ ≤ lift.{?u.141, w} #↑(⇑Equiv.ulift '' s')

Tactic:
h

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s') ∧ ℵ₀ ≤ #↑s'
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ (decide ¬i = j) = true

Tactic:
simpa using ij

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default ⇑xs.some

Tactic:
simpa using ij

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ T ⊆ L.completeTheory M ↔ T ⊆ L.completeTheory N

Tactic:
h.completeTheory_eq

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ T ⊆ L.completeTheory N ↔ T ⊆ L.completeTheory N
Module: Mathlib.ModelTheory.Skolem

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

Tactic:
h

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

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

Tactic:
· refine _root_.trans ?_ (lift_le.2 (mk_le_mk_of_subset Set.subset_union_right))
    rw [aleph0_le_lift, ← aleph0_le_lift, h]
    exact h1

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

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

Tactic:
have f : ∀ ψ ∈ Theory.ACF 0,
      { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } := by
    intro ψ hψ
    rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
    apply Classical.choice
    rcases hψ with h | ⟨p, hp, rfl⟩
    · refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)
    · refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ φ ∈ T

Tactic:
refine (h.mem_or_not_mem φ).resolve_right fun con => ?_
  rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ
  exact hφ h.1

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

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = s ^ i • x

Tactic:
heq

Goal state after:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = s ^ j • x
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ i • x

Tactic:
heq

Goal state after:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ j • x
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
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
rcases finite_or_infinite X with _ | _

Goal state after:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)