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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
hu₂ : Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop
⊢ EventuallyConst s (ae volume)

Tactic:
eventuallyConst_set'

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
hu₂ : Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop
⊢ s =ᵐ[volume] ∅ ∨ s =ᵐ[volume] univ
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
hf : HasCompactFixedSupport f
hg : HasCompactFixedSupport g
⊢ HasCompactFixedSupport (f ∘ g)

Tactic:
rw [HasCompactFixedSupport_iff'] at *

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
hf : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
hg : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints g)ᶜ ⊆ K
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints (f ∘ g))ᶜ ⊆ K
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
⊢ {x | p.mulOccursInAt x g} = cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)

Tactic:
ext x

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ {x | p.mulOccursInAt x g} ↔ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_2
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
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ Fintype.card ↑sn ≤ #s ^ n

Tactic:
apply (Fintype.card_range_le dyncover).trans

Goal state after:
case inr.inr.refine_2
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
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := ⋯
⊢ Fintype.card (Fin n → ↥s) ≤ #s ^ n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
exact fun _ ↦ isClosed_closure

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

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
obtain ⟨s, _, s_card⟩ := h

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty

Tactic:
rw [Order.one_le_iff_ne_zero, nonempty_iff_ne_empty]
  exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk
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
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ toEmbedding✝¹ = toEmbedding✝

Tactic:
ext x

Goal state after:
case mk.mk
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
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
x : M
⊢ toEmbedding✝¹ x = toEmbedding✝ 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 : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
⊢ f = g

Tactic:
ext x

Goal state after:
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 : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g 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 : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
⊢ f = g

Tactic:
ext x

Goal state after:
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 : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
x : M
⊢ f x = g x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk
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
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝¹.toFun (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun
⊢ toEquiv✝¹ = toEquiv✝

Tactic:
ext x

Goal state after:
case mk.mk
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
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝¹.toFun (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun
x : M
⊢ toEquiv✝¹ x = toEquiv✝ 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 : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
⊢ f = g

Tactic:
ext x

Goal state after:
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 : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝

Tactic:
exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions n
_ts✝ : Fin n → L[[γ]].Term α
ih : ∀ (a : Fin n), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Tactic:
ext x

Goal state after:
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: α : Type u'
n k : ℕ
⊢ relabelAux Sum.inl k = Sum.map id (natAdd n)

Tactic:
ext x

Goal state after:
α : Type u'
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl
α : Type u'
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)

Tactic:
simp [relabelAux]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)

Tactic:
simp [relabelAux]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case add
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ Group.IsSolvable (minpoly F (y + z)).Gal

Tactic:
apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin

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
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ y ∈ {y, z}

F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ z ∈ {y, z}
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ.inr
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✝ : ℕ
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)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Tactic:
exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = ⇑g ∘ fun i ↦ Term.realize v (_ts✝ i)

Tactic:
ext x

Goal state after:
case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
x : Fin l✝
⊢ Term.realize (⇑g ∘ v) (_ts✝ x) = (⇑g ∘ fun i ↦ Term.realize v (_ts✝ i)) x
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ lift.{max u u', 0} #ℕ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
      ciSup_le_iff' bddAbove_of_small]

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0
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
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
by
  have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
  rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h
  rw [eq_comm, h]

Goal state after:
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:
by rw [h]

Goal state after:
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:
by rw [h]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case zero
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
f : L.Functions 0
⊢ ClosedUnder f ∅

Tactic:
exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case zero
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs

Tactic:
exact Unique.exists_iff.symm

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case inr.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✝ S : L.Substructure M
A : Set M
h : A ⊆ ↑S
n✝ : ℕ
f : (constantsOn ↑A).Functions (n✝ + 1)
⊢ ClosedUnder (Sum.inr f) ↑S

Tactic:
exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.subtype.toHom.range = S

Tactic:
ext x

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ x ∈ S.subtype.toHom.range ↔ x ∈ S
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ ofPred ψ.Realize = ofPred ((LHom.addConstants (↑A) φ).onFormula ψ).Realize

Tactic:
ext x

Goal state after:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
x : α → M
⊢ x ∈ ofPred ψ.Realize ↔ x ∈ ofPred ((LHom.addConstants (↑A) φ).onFormula ψ).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ (fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize = ofPred (BoundedFormula.relabel id φ).exs.Realize

Tactic:
ext x

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize ↔ x ∈ ofPred (BoundedFormula.relabel id φ).exs.Realize
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ #((n : ℕ) × L.BoundedFormula α n) ≤ max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
refine lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)
  rw [mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0, max_le_iff]
  refine ⟨?_, le_max_left _ _⟩
  rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]
  simp only [lift_add, lift_lift, lift_aleph0]
  rw [← add_assoc, add_comm, ← add_assoc, ← add_assoc, aleph0_add_aleph0, add_assoc,
    add_eq_max le_rfl, add_assoc, card, Symbols, mk_sum, lift_add, lift_lift, lift_lift]

Goal state after:
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') ∧ ℵ₀ ≤ #↑s'

Tactic:
refine ⟨?_, h1⟩

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')
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K✝ : Type u_1
p : ℕ
K : Type u_2
inst✝ : Language.ring.Structure K
h : K ⊨ Theory.ACF p
⊢ Field K

Tactic:
have := modelField_of_modelACF p K
  exact fieldOfModelField K

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
f : (β → M) → M
h₁ : A.TermDefinable L f
h₂ : ∀ {n : ℕ} (g : L[[↑A]].Functions n), A.TermDefinable L' fun v ↦ Term.realize v g.term
⊢ A.TermDefinable L' f

Tactic:
obtain ⟨x, rfl⟩ := h₁
  choose c hc using @h₂
  simp only [funext_iff] at hc
  use x.substFunc c
  simp_rw [Term.realize_substFunc hc]

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

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

Tactic:
rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this

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

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

Tactic:
try assumption

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

Tactic:
try assumption

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b