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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(#s)).log / ↑n

Tactic:
apply (coverEntropyEntourage_le_log_coverMincard_div F_inv n_pos).trans

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ (↑(coverMincard T F U n)).log / ↑n ≤ (↑(#s)).log / ↑n
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : (X ^ n - C a).SplittingField
hc : c ^ n = 1
⊢ (aeval c) (X ^ n) = (aeval c) 1

Tactic:
aeval_X_pow,

Goal state after:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : (X ^ n - C a).SplittingField
hc : c ^ n = 1
⊢ c ^ n = (aeval c) 1
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : (aeval b) (X ^ n) - (aeval b) (C a) = 0
⊢ (σ * τ) b = (τ * σ) b

Tactic:
aeval_X_pow,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n - (aeval b) (C a) = 0
⊢ (σ * τ) b = (τ * σ) b
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F

Tactic:
by
  cases F
  rfl

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F

Tactic:
by
  cases F
  rfl

Goal state after:
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
⊢ map i (X ^ n) - map i 1 = C (i a⁻¹) * (map i (X ^ n) - map i (C a)).comp (C b * X)

Tactic:
Polynomial.map_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
⊢ map i X ^ n - map i 1 = C (i a⁻¹) * (map i X ^ n - map i (C a)).comp (C b * X)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: α : Type u'
⊢ (constantsOn α).card = #α

Tactic:
simp [card_eq_card_functions_add_card_relations, sum_nat_eq_add_sum_succ]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
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
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * (Multiset.map (fun c ↦ C b * (X - C (c / b))) s).prod =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod

Tactic:
Multiset.prod_map_mul,

Goal state after:
case h
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
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * ((Multiset.map (fun c ↦ C b) s).prod * (Multiset.map (fun c ↦ X - C (c / b)) s).prod) =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' ((⇑f.toEquiv ∘ ⇑f.symm) ∘ x)

Tactic:
Equiv.self_comp_symm,

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' (id ∘ x)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r ((⇑f.toEquiv ∘ ⇑f.symm) ∘ x) ↔ RelMap r x

Tactic:
Equiv.self_comp_symm,

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r (id ∘ x) ↔ RelMap r x
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable
    (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n) - map (algebraMap F (X ^ n - 1).SplittingField) (C x)).Gal

Tactic:
Polynomial.map_pow,

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable
    (map (algebraMap F (X ^ n - 1).SplittingField) X ^ n - map (algebraMap F (X ^ n - 1).SplittingField) (C x)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n) - map (algebraMap F (X ^ n - 1).SplittingField) 1).Splits
⊢ (X ^ n - 1).Splits

Tactic:
Polynomial.map_pow,

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
key : (map (algebraMap F (X ^ n - 1).SplittingField) X ^ n - map (algebraMap F (X ^ n - 1).SplittingField) 1).Splits
⊢ (X ^ n - 1).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval ((aeval x) (X ^ n))) p = 0

Tactic:
aeval_X_pow,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval (x ^ n)) p = 0
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable ((map (algebraMap F p.SplittingField) p).comp (map (algebraMap F p.SplittingField) (X ^ n))).Gal

Tactic:
Polynomial.map_pow,

Goal state after:
case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable ((map (algebraMap F p.SplittingField) p).comp (map (algebraMap F p.SplittingField) X ^ n)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
⊢ Group.IsSolvable (minpoly F z).Gal

Tactic:
have key : minpoly F z = minpoly F (f ⟨z, hz'⟩) := by
    refine minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))
    rw [aeval_algHom_apply, map_eq_zero]
    apply (algebraMap (↥F⟮x, y⟯) E).injective
    simp [← aeval_algebraMap_apply]

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Group.IsSolvable (minpoly F z).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Group.IsSolvable (minpoly F (f ⟨z, hz'⟩)).Gal

Tactic:
refine gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨z, hz'⟩)⟩ (gal_mul_isSolvable hx' hy')

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Normal F (p * q).SplittingField
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
map_cons,

Goal state after:
case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ ts i :: listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
· rw [← Cardinal.one_le_iff_ne_zero]
      refine _root_.trans ?_ (le_ciSup bddAbove_of_small 1)
      rw [Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]
      exact ⟨var (Sum.inr 0)⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : ↥(equal t₁✝ t₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(equal t₁✝ t₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁✝ =
      realize (Sum.elim v xs) (t₂✝.restrictVarLeft (f ∘ Set.inclusion ⋯)) ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Tactic:
realize_restrictVarLeft v' (by simp [hv'])

Goal state after:
case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : ↥(equal t₁✝ t₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(equal t₁✝ t₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁✝ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂✝ ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v xs) ((ts✝ x✝).restrictVarLeft (f ∘ Set.inclusion ⋯)) = realize (Sum.elim v' xs) (ts✝ x✝)

Tactic:
realize_restrictVarLeft v' (by simp [hv'])

Goal state after:
case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts✝ x✝) = realize (Sum.elim v' xs) (ts✝ x✝)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
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✝ + 1)
⊢ ClosedUnder f ∅

Tactic:
intro x hx

Goal state after:
case succ
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✝ + 1)
x : Fin (n✝ + 1) → M
hx : ∀ (i : Fin (n✝ + 1)), x i ∈ ∅
⊢ funMap f x ∈ ∅
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc xs x)) ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

Goal state after:
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 φ ih xs

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 : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀' φ).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (∀' φ).Realize default xs
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ range (Term.realize Subtype.val) ⊆ A

Tactic:
intro x hx

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
x : M
hx : x ∈ range (Term.realize Subtype.val)
⊢ x ∈ A
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
by
  classical
    refine Finset.induction definable_empty (fun i s _ h => ?_) s
    rw [Finset.sup_insert]
    exact (hf i).union h

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
⊢ T.IsSatisfiable

Tactic:
set M : Finset T → Type max u v := fun T0 : Finset T =>
      (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
    let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
    have h' : M' ⊨ T := by
      refine ⟨fun φ hφ => ?_⟩
      rw [Ultraproduct.sentence_realize]
      refine
        Filter.Eventually.filter_mono (Ultrafilter.of_le _)
          (Filter.eventually_atTop.2
            ⟨{⟨φ, hφ⟩}, fun s h' =>
              Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
                ?_⟩)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
        Subtype.exists, exists_and_right, exists_eq_right]
      exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
    exact ⟨ModelType.of T M'⟩

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:
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.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
x : L[[↑A]].Term β
c : {n : ℕ} → L[[↑A]].Functions n → L'[[↑A]].Term (Fin n)
hc : ∀ {n : ℕ} (g : L[[↑A]].Functions n), (fun v ↦ Term.realize v g.term) = fun v ↦ Term.realize v (c g)
⊢ A.TermDefinable L' fun v ↦ Term.realize v x

Tactic:
simp only [funext_iff] at hc

Goal state after:
M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
x : L[[↑A]].Term β
c : {n : ℕ} → L[[↑A]].Functions n → L'[[↑A]].Term (Fin n)
hc : ∀ {n : ℕ} (g : L[[↑A]].Functions n) (x : Fin n → M), Term.realize x g.term = Term.realize x (c g)
⊢ A.TermDefinable L' fun v ↦ Term.realize v x
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ((fun x ↦ f (x ())) = fun v ↦ Term.realize v φ) ↔ f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
rw [funext_iff, funext_iff, (Equiv.funUnique Unit M).forall_congr']

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ∀ (b : M),
    f ((Equiv.funUnique Unit M).symm b ()) = Term.realize ((Equiv.funUnique Unit M).symm b) φ ↔
      f b = ((fun v ↦ Term.realize v φ) ∘ Function.const Unit) b
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
| ∑ a ∈ monoms i,
    if ∃ (h : a ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) = 0 then
      (if h : a ∈ monoms i then f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) else 0) * ∏ x ∈ a.support, f (Sum.inr x) ^ a x
    else 0

Tactic:
← Finset.sum_attach

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
| ∑ x ∈ (monoms i).attach,
    if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
      (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
    else 0
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h
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
⊢ (fun x ↦ x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Tactic:
rw [oreDiv_eq_iff]

Goal state after:
case h
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
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h
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
⊢ (fun x ↦ x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Tactic:
rw [oreDiv_eq_iff]

Goal state after:
case h
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
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1