mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ rec (Functor.map mk)) <$> x = id <$> x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
id_map,

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ rec (Functor.map mk)) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 ≤ sign 0 * 0

Tactic:
rw [mul_zero]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ u ∈ supp x ↔ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

Tactic:
supp

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ u ∈ {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y} ↔ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
S : WSeq (Computation α)
m : pure a ∈ []
⊢ ∃ a, parallel.aux2 [] = Sum.inl a

Tactic:
simp at m

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

Goal state before:
pp: case nil
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
m : s.think ∈ []
l' : List (Computation α)
e' : parallel.aux2 [] = Sum.inr l'
⊢ s ∈ l'

Tactic:
simp at m

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
cases finite_or_infinite α
  · obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact card_subtype_not_diag
  · simp

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

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
⊢ a' ∈ parallel S

Tactic:
have aa := parallel_promises h2 h

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
⊢ b ∈ (map f v).toList ↔ ∃ a, a ∈ v.toList ∧ f a = b

Tactic:
rw [Vector.toList_map, List.mem_map]

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f

Tactic:
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]

Goal state after:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f
Module: Mathlib.Data.ZMod.Coprime

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬¬↑p ∣ a

Tactic:
Classical.not_not,

Goal state after:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ↑p ∣ a
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T

Tactic:
linarith [hT.out]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
← map_add_atTop_eq_nat k,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in Filter.map (fun a ↦ a + k) atTop, f^[n] x ∈ s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ'.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x

Tactic:
have h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν :=
    Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddMonoid τ
ϕ : Flow τ α
s : Set α
hs : IsInvariant ϕ.toFun s
x✝ x : ↑s
⊢ x ∈ (ϕ.restrict hs).orbit x✝ ↔ x ∈ Subtype.val ⁻¹' ϕ.orbit ↑x✝

Tactic:
by simp [orbit_eq_range, Subtype.ext_iff]

Goal state after:
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
v h : G
hmem : h ∉ Finset.image (fun x ↦ v * x) p.support
⊢ A

Tactic:
else

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v h : G
hmem : h ∉ Finset.image (fun x ↦ v * x) p.support
⊢ A
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ map φ φ ⁻¹' dynEntourage T U n = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
by
  rw [dynEntourage, preimage_iInter₂]
  refine iInter₂_congr fun k _ ↦ ?_
  rw [← preimage_comp, ← preimage_comp, map_iterate S S k, map_iterate T T k, map_comp_map,
    map_comp_map, (Function.Semiconj.iterate_right h k).comp_eq]

Goal state after:
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
⊢ F = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

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
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ G.domRestrict φ (MapsTo.restrict S G G hG x) = T (G.domRestrict φ x)

Tactic:
G.domRestrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG x) = T (G.domRestrict φ x)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG x) = T (G.domRestrict φ x)

Tactic:
G.domRestrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG x) = T (φ ↑x)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ G.domRestrict φ (MapsTo.restrict S G G hG a) = T (G.domRestrict φ a)

Tactic:
G.domRestrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG a) = T (G.domRestrict φ a)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG a) = T (G.domRestrict φ a)

Tactic:
G.domRestrict_apply,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
a : ↑G
⊢ φ ↑(MapsTo.restrict S G G hG a) = T (φ ↑a)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
by
  classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.natCast_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
⊢ (aeval x) (p.comp (X ^ n)) = 0

Tactic:
simpa [aeval_comp]

Goal state after:
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
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
by
  let p := minpoly F (x ^ n)
  have hp : p.comp (X ^ n) ≠ 0 := by
    intro h
    rcases comp_eq_zero_iff.mp h with h' | h'
    · exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'
    · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
  apply gal_isSolvable_of_splits
  · exact ⟨(SplittingField.splits (p.comp (X ^ n))).of_dvd (map_ne_zero hp)
      ((map_dvd_map' _).mpr (minpoly.dvd F x (by rw [aeval_comp, aeval_X_pow, minpoly.aeval])))⟩
  · refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
    · exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])
    · obtain ⟨s, hs⟩ := splits_iff_exists_multiset.1 (SplittingField.splits p)
      rw [map_comp, Polynomial.map_pow, map_X, hs, mul_comp, C_comp]
      apply gal_mul_isSolvable (gal_C_isSolvable _)
      rw [multiset_prod_comp]
      apply gal_prod_isSolvable
      intro q hq
      rw [Multiset.mem_map] at hq
      obtain ⟨q, hq, rfl⟩ := hq
      rw [Multiset.mem_map] at hq
      obtain ⟨q, _, rfl⟩ := hq
      rw [sub_comp, X_comp, C_comp]
      exact gal_X_pow_sub_C_isSolvable n q

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
k : ℕ
φ : L.BoundedFormula α k
⊢ ∀ {m n : ℕ} (km : k ≤ m) (mn : m ≤ n), castLE mn (castLE km φ) = castLE ⋯ φ

Tactic:
induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
by
  simp only [max]
  tauto

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

Tactic:
cons_append,

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.Semantics

Goal state before:
pp: case all.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ ↑(Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    ↑(if ↑i < m then castAdd n' i else i.addNat n').castSucc

Tactic:
simp only [val_castSucc, val_cast]

Goal state after:
case all.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ ↑(if ↑i < m then castAdd n' i.castSucc else i.castSucc.addNat n') = ↑(if ↑i < m then castAdd n' i else i.addNat n')
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize
      (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ 1 ≤ #(L.Term (α ⊕ Fin 1))

Tactic:
Cardinal.one_le_iff_ne_zero,

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ #(L.Term (α ⊕ Fin 1)) ≠ 0
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 ([Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₁✝⟩, Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₂✝⟩] ++ l) =
    ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l

Tactic:
cons_append,

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 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

Tactic:
cons_append,

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
      ([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

Tactic:
cons_append,

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
      (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

Tactic:
cons_append,

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
      (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

Tactic:
cons_append,

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.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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ (⇑f ∘ x) x✝ = (⇑g ∘ x) x✝

Tactic:
rw [Function.comp_apply]

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ f (x x✝) = (⇑g ∘ x) x✝
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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ f (x x✝) = (⇑g ∘ x) x✝

Tactic:
rw [Function.comp_apply]

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ f (x x✝) = g (x x✝)
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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ f (x x✝) = g (x x✝)

Tactic:
rw [Function.comp_apply]

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ f (x x✝) = g (x x✝)