mathlib-initiative/mathlib-tactics huggingface dataset:
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
aa : a = a'
⊢ a ∈ parallel S

Tactic:
rw [← aa] at 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.Snoc

Goal state before:
pp: α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| val ::ᵥ replicate (n + 1) val = (replicate (n + 1) val).snoc val

Tactic:
rhs; rw [replicate_succ]

Goal state after:
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| (val ::ᵥ replicate n val).snoc val
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
⊢ Tendsto (fun j ↦ addOrderOf (u j)) atTop atTop

Tactic:
hu₀

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
⊢ Tendsto (fun j ↦ n.natAbs ^ j) atTop atTop
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_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
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 ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x

Tactic:
ext1 s 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
⊢ (μ.withDensity f) s = (0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x) s
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddGroup τ
ϕ : Flow τ α
t : τ
x : α
⊢ ϕ.toFun (-t) (ϕ.toFun t x) = x

Tactic:
simp [← map_add]

Goal state after:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddGroup τ
ϕ : Flow τ α
t : τ
x : α
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x

Tactic:
simp [← map_add]

Goal state after:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddGroup τ
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s ⊆ s
t : τ
x✝ : α
hx : x✝ ∈ s
⊢ ϕ.toFun t (ϕ.toFun (-t) x✝) = x✝

Tactic:
simp [← map_add]

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✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
ext1 s 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
⊢ μ s = (0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) s
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
ex : ∃ w ∈ p.support, v * w = h := mulShift._proof_2 p v h hmem
⊢ A

Tactic:
exact p.config (Classical.choose ex)

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = coverMincard T F U n

Tactic:
rw [← k_min]

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = ↑k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ∀ (x : Finset X), ¬IsDynCoverOf T F U n ↑x
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Tactic:
exact h

Goal state after:
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)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
have h := cv_mono.expGrowthSup_comp_mul 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.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F

Tactic:
obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni

Goal state after:
X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F

Tactic:
obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni

Goal state after:
X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
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
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹

Tactic:
have h := add_mul (μ.rnDeriv ν a) 1 (μ.rnDeriv ν a + 1)⁻¹

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
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
⊢ Group.IsSolvable q.Gal

Tactic:
by
  let K := p.SplittingField
  let L := q.SplittingField
  have : Fact ((p.map (algebraMap F L)).Splits) := ⟨hpq⟩
  let ϕ : Gal(L/K) ≃* (q.map (algebraMap F K)).Gal :=
    (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr
  have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
  have : Group.IsSolvable Gal(K/F) := hp
  have : Group.IsSolvable Gal(L/K) := Group.isSolvable_of_isSolvable_injective ϕ_inj
  exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ ↥(Algebra.adjoin R (Set.range v)) ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
refine hv.1.aevalEquiv.symm.toRingEquiv.trans ?_

Goal state after:
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))
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
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
s : Subalgebra F E :=
  { carrier := {x | ∃ (hx : x ∈ solvableByRad F E), motive x hx}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
    zero_mem' := ⋯, algebraMap_mem' := ⋯ }
t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField ⋯
ht : ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ t → x ∈ t
w✝ : x ∈ solvableByRad F E
h : motive x w✝
⊢ motive x hx

Tactic:
exact h

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ ((∀' φ).Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (∀' φ).Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
| @all k φ ih =>

Goal state after:
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 ∘ 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

Tactic:
refine h.trans ?_

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
      (((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) ↔
    φ.Realize v xs
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]

Goal state after:
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
⊢ BoundedFormula.Realize φ (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ ((relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs

Tactic:
by
  simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]
  refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl
  simp only [relabelEquiv_apply, Term.realize_relabel]
  refine congr (congr rfl ?_) rfl
  ext (i | i) <;> rfl

Goal state after:
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
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap f x ∈ S
⊢ funMap f x ∈ ↑S

Tactic:
exact h

Goal state after:
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
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S T : L'.Substructure M
h : S = T
⊢ S = T

Tactic:
exact 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₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) t✝ =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝

Tactic:
congr 1 with a

Goal state after:
case e_v
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
a : (↑A ⊕ α) ⊕ Fin n✝
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) a =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ a
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
⊢ (∃ i,
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize ((fun a ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g)))) fun a ↦
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.Realize, Function.comp_def, Term.equal, Term.relabel, realize_iInf,
    realize_bdEqual, Term.realize_var, Sum.elim_inl, Sum.elim_inr, funext_iff]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize φ (fun x ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ x, Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
φ : L.Formula α
⊢ M ⊨ φ.exClosure ↔ ∃ v, Realize (BoundedFormula.restrictFreeVar φ id) v

Tactic:
by
  simp [Sentence.Realize, Formula.exClosure, Formula.realize_iExs]

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case w
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
⊢ funMap φ' (Subtype.val ∘ x) ∈ LHom.sumInl.substructureReduct S

Tactic:
exact S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by
      exact fun i => (x i).2)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ

Tactic:
exact h

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
let S' : Set (ι → Algebra.adjoin K (s : Set R)) :=
    (fun v => Subtype.val ∘ v) ⁻¹' S

Goal state after:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ ∀ (v : α → AlgebraicClosure (ZMod p)) (p_1 : { p_1 // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    have f := fun v i ↦ (eval v) (↑p_1 i);
    have S := {x | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
rintro v ⟨f, _⟩

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
v : α → AlgebraicClosure (ZMod p)
f : ι → MvPolynomial ι (AlgebraicClosure (ZMod p))
property✝ : ∀ (i : ι), (f i).support ⊆ mons i
⊢ have f := fun v i ↦ (eval v) (↑⟨f, property✝⟩ i);
  have S := {x | φ.Realize (Sum.elim v x)};
  Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ (Derivation.liftOfSurjective ⋯ ⋯) ((AdjoinRoot.mk p).toIntAlgHom (C a)) = (algebraMap F (AdjoinRoot p)) a′

Tactic:
Derivation.liftOfSurjective_apply,

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ (AdjoinRoot.mk p).toIntAlgHom
      ((implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯)
            (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
        (C a)) =
    (algebraMap F (AdjoinRoot p)) a′