mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∃ r', Raised (erase x t_r).size r' ∧ BalancedSz t_l.size r'

Tactic:
exists t_r.size

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Raised (erase x t_r).size t_r.size ∧ BalancedSz t_l.size t_r.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := ⋯
⊢ y.fst = x

Tactic:
dsimp [y]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
⊢ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst = x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_pos hp, one_mul]
    exact hp.le

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (s : Computation α),
    (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
intro C'

Goal state after:
case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
⊢ (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
    ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = C'.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons b ss
m : a ∈ (cons x✝ s✝).append S.join
this : x✝ = b ∧ s✝.append S.join = ss
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
cases this with
      | intro b' s =>
        subst b' ss
        simp? at m ⊢ says simp only [cons_append, mem_cons_iff] at m ⊢
        rcases o with e | IH
        · simp [e]
        rcases m with e | m
        · simp [e]
        exact Or.imp_left Or.inr (IH _ _ rfl m)

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
refine funext fun j => j.cases' ?_ ?_ <;> intros

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n✝ : Fin2 n
⊢ insert a v fz n✝.fs = (a :: v) n✝.fs
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝¹ : g ∈ ⊤
x✝ : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ
⊢ g ∈ aestabilizer G μ s

Tactic:
cases eventuallyConst_set'.mp hs with

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s

Tactic:
intro h
    contrapose! h
    obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a := by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective
    exact ⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s

Tactic:
· intro h
    contrapose! h
    obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a := by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective
    exact ⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_sdiff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s)
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
⊢ ∀ᵐ (a : X) ∂ν, (μ.rnDeriv ν ∘ f) a < c ↔ μ.rnDeriv ν a < c

Tactic:
suffices f ⁻¹' s =ᵐ[ν] s from this.mem_iff

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_sdiff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s)
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
⊢ f ⁻¹' s =ᵐ[ν] s
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ μ (f ⁻¹' s \ s) ≠ μ (s \ f ⁻¹' s)

Tactic:
apply ne_of_gt

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ μ (s \ f ⁻¹' s) < μ (f ⁻¹' s \ s)
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
⊢ fixedSupport f = closure (fixedPoints f)ᶜ

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ f ⁻¹' sᶜ = sᶜ

Tactic:
by rw [preimage_compl, hfs]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
⊢ HasCompactFixedSupport f ↔ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨K, hK₁, hK₂, hf⟩ ↦ ?_⟩
  · exact ⟨closure (fixedPoints f)ᶜ, isClosed_closure, hf, subset_closure⟩
  · exact hK₂.of_isClosed_subset isClosed_closure (hK₁.closure_subset_iff.mpr hf)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f a)⁻¹ * μ.rnDeriv ν a ∂ν.withDensity f

Tactic:
rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f * fun a ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)
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 < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})

Tactic:
← image_comp,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = sSup (WithTop.some ∘ Finset.card '' {s | IsDynNetIn T F U n ↑s})
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x

Tactic:
simp only [Pi.inv_apply, ← hx, inv_inv]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
nth_rw 1 [h4, h6]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ IsEmpty Language.empty.Symbols

Tactic:
by
  simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]
  exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
m : ℕ
f : L.Functions m
xs : Fin m → L.Term α
this : DecidableEq (L.Term α) := instDecidableEq
g : L.Functions m
ys : Fin m → L.Term α
⊢ (f = ⋯ ▸ g ∧ ∀ (i : Fin m), xs i = ys (Fin.cast ⋯ i)) ↔ func f xs = func g ys

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
v : Fin n → M
f : L.Functions n
⊢ realize v f.term = funMap f v

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinset → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinset), v (f a_1) = v' ↑a_1) → realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinset → β
hv' : ∀ (a : ↥(func _f✝ _ts✝).varFinset), v (f a) = v' ↑a
⊢ realize v ((func _f✝ _ts✝).restrictVar f) = realize v' (func _f✝ _ts✝)

Tactic:
exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a✝ : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((var a✝).listEncode ++ l) = var a✝ :: listDecode l

Tactic:
listEncode,

Goal state after:
case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a✝ : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ([Sum.inl a✝] ++ l) = var a✝ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func
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)
⊢ listDecode ((func f ts).listEncode ++ l) = func f ts :: listDecode l

Tactic:
listEncode,

Goal state after:
case func
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)
⊢ listDecode (Sum.inr ⟨n, f⟩ :: flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = func f ts :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l

Tactic:
listEncode,

Goal state after:
case falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ([Sum.inr (Sum.inr (⟨n✝, falsum⟩.fst + 2))] ++ l) = ⟨n✝, falsum⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case equal
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, equal t₁✝ t₂✝⟩.snd.listEncode ++ l) = ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l

Tactic:
listEncode,

Goal state after:
case equal
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ([Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₁✝⟩, Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₂✝⟩] ++ l) =
    ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l) = ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
listEncode,

Goal state after:
case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode
      ([Sum.inr (Sum.inl ⟨φ_l, φ_R⟩), Sum.inr (Sum.inr ⟨φ_n, rel φ_R ts⟩.fst)] ++
          List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++
        l) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l) = ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]

Goal state after:
case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h :
          ∀ (i : Fin φ_l),
            (List.map Sum.getLeft?
                      (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
              true then
        if h' :
            ∀ (i : Fin φ_l),
              ((List.map Sum.getLeft?
                            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                    ⋯).fst =
                ⟨φ_n, rel φ_R ts⟩.fst then
          ⟨⟨φ_n, rel φ_R ts⟩.fst,
            rel φ_R fun i ↦
              ⋯.mp
                ((List.map Sum.getLeft?
                            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                    ⋯).snd⟩
        else default
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l
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
φ : M →[L] N
S : L.Substructure N
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S
⊢ funMap f x ∈ ⇑φ ⁻¹' ↑S

Tactic:
by
    rw [mem_preimage, φ.map_fun]
    exact S.fun_mem f (φ ∘ x) hx

Goal state after:
Module: Mathlib.ModelTheory.Substructures

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

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

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∃ xs,
      Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        xs (natAdd (Classical.choose ⋯) x)) ↔
    ∃ i, φ.Realize (Sum.elim v i)

Tactic:
refine Equiv.exists_congr ?_ ?_

Goal state after:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (γ → M)

case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize (Sum.elim v (?refine_1 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:
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.Encoding

Goal state before:
pp: case imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁✝.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂✝.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ((f₁✝ ⟹ f₂✝).listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l

Tactic:
listEncode,

Goal state after:
case imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁✝.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂✝.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (Sum.inr (Sum.inr 0) :: f₁✝.listEncode ++ f₂✝.listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l