mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case H
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
        (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct

pp: case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct

Tactic:
· exact fun {c1 c2} h =>
      match c1, c2, h with
      | _, _, ⟨s, rfl, rfl⟩ => by
        clear h
        have (s : WSeq α) : ∃ s' : WSeq α,
            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
          ⟨s, rfl, rfl⟩
        induction s using WSeq.recOn <;> simp [ret, this]

Goal state after:
case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this : some val✝ ∈ (s.drop (n + 1)).head
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none

Tactic:
obtain ⟨a', h'⟩ := head_some_of_head_tail_some this

Goal state after:
case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this : some val✝ ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: case cons
α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s) ∧
    s2 =
      Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))
⊢ Computation.BisimO
    (fun c1 c2 ↦
      ∃ l s,
        c1 =
            Computation.corec
              (fun x ↦
                match x with
                | (n, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map List.length
              (Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, cons a s)).destruct
    (Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, cons a s))).destruct

Tactic:
simpa using ⟨a::l, s, by simp, by simp⟩

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
⊢ ErgodicSMul G G μ

Tactic:
by
  refine ⟨fun {s} hsm hs ↦ ?_⟩
  suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
  intro hμs
  obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (b * a ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs b).mem_iff
    · exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
  simpa [has] using (MeasureTheory.quasiMeasurePreserving_mul_right μ a⁻¹).ae ha

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

Tactic:
IsClosed.closure_eq,

Goal state after:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.closure {c})

Tactic:
← hc

Goal state after:
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.closure {a, b})
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
j : ℕ
⊢ u j +ᵥ s =ᵐ[volume] s

Tactic:
vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)

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
j : ℕ
⊢ s =ᵐ[volume] s
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U

Tactic:
rw [← preimage_comp, mem_preimage, mem_preimage, hx]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure[inst✝] (image2 ϕ u s)

Tactic:
rw [omegaLimit_eq_iInter]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s) ⊆ closure[inst✝] (image2 ϕ u s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
have h₁ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) (ν + ν')

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
⊢ ∀ (x : X), x ∉ F

Tactic:
intro x x_F

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
← ν.haveLebesgueDecomposition_add μ

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
← ν.haveLebesgueDecomposition_add μ

Goal state after:
case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv ν x ≠ 0 → p x
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ coverMincard T F (U ○ U) n ≤ ↑s.card

Tactic:
apply IsDynCoverOf.coverMincard_le_card

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ IsDynCoverOf T F (U ○ U) n ↑s
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
cv_mono : Monotone fun m ↦ ↑(coverMincard T F (U ○ U) m)
h :
  (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) =
    (expGrowthSup fun m ↦ ↑(coverMincard T F (U ○ U) m)) * ↑n
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
← div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (Nat.cast_ne_zero.2 n_pos)

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
cv_mono : Monotone fun m ↦ ↑(coverMincard T F (U ○ U) m)
h :
  (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) / ↑n =
    expGrowthSup fun m ↦ ↑(coverMincard T F (U ○ U) m)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n
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 : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ b * ((algebraMap F (X ^ n - C a).SplittingField) c * (algebraMap F (X ^ n - C a).SplittingField) d) =
    b * ((algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c)

Tactic:
mul_right_inj' hb',

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 = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ (algebraMap F (X ^ n - C a).SplittingField) c * (algebraMap F (X ^ n - C a).SplittingField) d =
    (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c
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)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ n = 0

Tactic:
rw [← @natDegree_C F, ← h'.2, natDegree_X_pow]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 0 → R), funMap zeroFunc x = 0

Tactic:
simp only [Fin.forall_fin_zero_pi]

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ funMap zeroFunc finZeroElim = 0
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 0 → R), funMap oneFunc x = 1

Tactic:
simp only [Fin.forall_fin_zero_pi]

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ funMap oneFunc finZeroElim = 1
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ i,
        ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)

Tactic:
simp only [prodMk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion,
      mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right]

Goal state after:
L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔ ∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func.refine_2
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
simp only [length_map, length_finRange, drop_left']

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_2
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
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ M ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls ↔ φ.Realize x

Tactic:
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff]
      rfl

Goal state after:
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
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
⊢ {x | x 0 ∈ D} =
    ofPred
      (Formula.Realize
        (BoundedFormula.subst
          (Formula.relabel (Sum.elim Empty.elim id) ((L.lhomWithConstants ↑A).onBoundedFormula φ).toFormula) fun i ↦
          Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) i))

Tactic:
ext v

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
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
⊢ v ∈ {x | x 0 ∈ D} ↔
    v ∈
      ofPred
        (Formula.Realize
          (BoundedFormula.subst
            (Formula.relabel (Sum.elim Empty.elim id) ((L.lhomWithConstants ↑A).onBoundedFormula φ).toFormula) fun i ↦
            Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) i))
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
⊢ sᶜ = ofPred φ.not.Realize

Tactic:
ext v

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ ofPred φ.not.Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
⊢ {v | ∃ u, Sum.elim v u ∈ S} = ofPred (Formula.iExs β φ).Realize

Tactic:
ext v

Goal state after:
M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
v : α → M
⊢ v ∈ {v | ∃ u, Sum.elim v u ∈ S} ↔ v ∈ ofPred (Formula.iExs β φ).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
v : α → M
⊢ v ∈ {v | ∃ u, Sum.elim v u ∈ S} ↔ v ∈ ofPred (Formula.iExs β φ).Realize

Tactic:
simp [hφ]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
⊢ {v | ∀ (u : β → M), Sum.elim v u ∈ S} = ofPred (Formula.iAlls β φ).Realize

Tactic:
ext v

Goal state after:
M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
v : α → M
⊢ v ∈ {v | ∀ (u : β → M), Sum.elim v u ∈ S} ↔ v ∈ ofPred (Formula.iAlls β φ).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
φ : L[[↑A]].Formula (α ⊕ β)
hφ : S = ofPred φ.Realize
v : α → M
⊢ v ∈ {v | ∀ (u : β → M), Sum.elim v u ∈ S} ↔ v ∈ ofPred (Formula.iAlls β φ).Realize

Tactic:
simp [hφ]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
⊢ (tupleGraph fun v ↦ Term.realize v t) = ofPred ((Term.relabel some t).equal (var none)).Realize

Tactic:
ext v

Goal state after:
M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
v : Option α → M
⊢ (v ∈ tupleGraph fun v ↦ Term.realize v t) ↔ v ∈ ofPred ((Term.relabel some t).equal (var none)).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L {w | w ∘ Sum.inr ∈ S}
⊢ F ⁻¹' S = {v | ∃ u, Sum.elim v u ∈ {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w | w ∘ Sum.inr ∈ S}}

Tactic:
ext v

Goal state after:
M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L {w | w ∘ Sum.inr ∈ S}
v : α → M
⊢ v ∈ F ⁻¹' S ↔ v ∈ {v | ∃ u, Sum.elim v u ∈ {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w | w ∘ Sum.inr ∈ S}}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : lift.{w', w} #↑s ≤ lift.{w, w'} #M
this : Inhabited M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
rw [Cardinal.lift_mk_le'] at h

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this : Inhabited M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
by
  cases hp with
  | inl hp =>
    have : Fact p.Prime := ⟨hp⟩
    let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
    exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
  | inr hp =>
    subst hp
    let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
    exact ⟨⟨AlgebraicClosure ℚ⟩⟩

Goal state after: