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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b

Tactic:
intro a b

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
by
    obtain rfl | ha := eq_bot_or_bot_lt a
    · exact Lex.right _ _ bot_le
    · exact Lex.left _ _ ha

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = (map (map f) S).join

Tactic:
apply
    Seq.eq_of_bisim fun s1 s2 =>
      ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join

case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
· simpa using ⟨_, _, rfl, rfl⟩

Goal state after:
case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
· simpa using ⟨_, _, rfl, rfl⟩

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

Goal state before:
pp: case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
⊢ f ⁻¹' s = s → EventuallyConst s (ae μ)

Tactic:
hs

Goal state after:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
⊢ EventuallyConst s (ae μ)
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
⊢ (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)

Tactic:
hs

Goal state after:
case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
hs : ∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

Tactic:
hs

Goal state after:
G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ s =ᵐ[μ] s
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := ⋯
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ a✝ > x✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝

Tactic:
gt_iff_lt,

Goal state after:
case e'_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ x✝ < a✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T
⊢ ENNReal.ofReal T * μ (s ∩ I j) =
    μ (I j) * (↑(addOrderOf (u j)) * volume (s ∩ closedBall d (T / (2 * ↑(addOrderOf (u j))))))

Tactic:
←
    mul_assoc,

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T
⊢ ENNReal.ofReal T * μ (s ∩ I j) =
    μ (I j) * ↑(addOrderOf (u j)) * volume (s ∩ closedBall d (T / (2 * ↑(addOrderOf (u j)))))
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))

Tactic:
by
  use hfμ.measurable
  ext s hs
  rw [← ENNReal.add_left_inj (measure_ne_top (μ.singularPart ν) s), map_apply hfμ.measurable hs,
    ← add_apply, rnDeriv_add_singularPart,
    ← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet, ← add_apply,
    rnDeriv_add_singularPart, hfμ.measure_preimage hs.nullMeasurableSet]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
intro h _ hu _ hn

Goal state after:
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
⊢ (t✝ ∩ image2 ϕ i✝ s).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
exact dynEntourage_comp_subset T U U n (mem_ball_comp z_By z_Bx)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
refine rnDeriv_eq_zero_of_mutuallySingular (mutuallySingular_singularPart ν μ).symm ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ν.singularPart μ ≪ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
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 : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm

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 (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddMonoid τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)

Tactic:
by
  refine fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))
  exact
    mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm)
      (continuous_const.flow ϕ continuous_id)

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)

Tactic:
· refine iSup₂_le fun U U_uni ↦ ?_
    simp only [uniformity_comap φ, mem_comap] at U_uni
    obtain ⟨V, V_uni, V_sub⟩ := U_uni
    obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
    apply (coverEntropyEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
    apply (le_coverEntropyEntourage_image h F).trans
    exact coverEntropyEntourage_le_coverEntropy T (φ '' F) W_uni

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

Goal state before:
pp: case inr.inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑(#s) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ ↑(#s) ^ n

Tactic:
exact t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)

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 : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑(#s) = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
by
  -- Otherwise, there is a ball which does not intersect `F`. Removing it yields a smaller cover.
  classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_sdiff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ

Tactic:
by
  obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν
  filter_upwards [hνκ <| Measure.rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) κ,
    hνκ <| Measure.rnDeriv_withDensity_left_of_absolutelyContinuous hνκ h_meas.aemeasurable,
    Measure.rnDeriv_eq_zero_of_mutuallySingular h_sing hνκ] with x hx1 hx2 hx3
  nth_rw 2 [hμν]
  rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
⊢ funMap (ϕ.onFunction f) xs = funMap f xs

Tactic:
have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩

Goal state after:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : ϕ.onFunction f ∈ Set.range fun f ↦ ϕ.onFunction f
⊢ funMap (ϕ.onFunction f) xs = funMap f xs
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
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)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
⊢ q ∈ Multiset.map (fun p_1 ↦ p_1.comp (X ^ n)) (Multiset.map (fun x ↦ X - C x) s) → Group.IsSolvable q.Gal

Tactic:
hq

Goal state after:
case hq.refine_2
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)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
hq : q ∈ Multiset.map (fun p_1 ↦ p_1.comp (X ^ n)) (Multiset.map (fun x ↦ X - C x) s)
⊢ Group.IsSolvable q.Gal
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs)

Tactic:
funext x

Goal state after:
case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) x
Module: Mathlib.ModelTheory.Encoding

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

pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
· refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩
      refine max_le (le_max_left _ _) ?_
      grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
⊢ N ⊨ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : N ⊨ φ
⊢ M ⊨ φ
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
mk_nat

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ x, eval x p = 0

Tactic:
realize_genericMonicPolyHasRoot

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : ∀ (p_1 : { p_1 // p_1.Monic ∧ p_1.natDegree = p.natDegree }), ∃ x, eval x ↑p_1 = 0
⊢ ∃ x, eval x p = 0
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
⊢ ↑s ⊆ ⋃ i, T i → IsSatisfiable ↑s

Tactic:
hs

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑s
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ Formula.Realize φ default ∨ ¬Formula.Realize φ default

Tactic:
or_not

Goal state after: