mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨j, b⟩ < ⟨i, a⟩

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨i, b⟩ < ⟨i, a⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨j, b⟩ < ⟨i, a⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨j, b⟩

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨i, b⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨i, b⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.nil.nil
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = ss.think
m : a ∈ nil.append nil.join
this : Seq.destruct (nil.append nil.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s

pp: case h2.cons
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (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 = ss.think
m : a ∈ (cons x✝ s✝).append S.join
this : Seq.destruct ((cons x✝ s✝).append S.join) = Seq.destruct ss.think
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
case nil.nil | cons => simp at this

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (x ::ᵥ ⟨val✝, property✝⟩).reverse = (reverse ⟨val✝, property✝⟩).snoc x

Tactic:
simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]

Goal state after:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝.reverse ++ [x], ⋯⟩ = ⟨val✝.reverse, ⋯⟩ ++ ⟨[x], ⋯⟩
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (w✝.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x✝ ::ᵥ w✝).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
· simp [*]

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ ∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅

pp: case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅

Tactic:
· rintro a b rfl rfl; exact disjSum_eq_empty.1 h

Goal state after:
case refine_4
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

pp: case refine_2
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ ∀ (n_1 : Fin2 n), p ((a :: v) n_1.fs)

Tactic:
exacts [pa, h]

Goal state after:
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ fb y} (fa (g' y))

Tactic:
rw [← fa.surjective.image_preimage { x | g x ≤ fb y }, preimage_ofPred_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (⇑fa '' {a | g (fa a) ≤ fb y}) (fa (g' y))
Module: Mathlib.Dynamics.Ergodic.Action.Basic

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

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩

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 α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)

case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α}, MeasurableSet s → (∀ (g : IterateMulAct f), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s) → EventuallyConst s (ae μ)
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ |(f ^ 2 ^ n) 0 / 2 ^ n - ((f ^ 2 ^ n) ^ 2) 0 / (2 * 2 ^ n)| =
    |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0) / (2 * 2 ^ n)|

Tactic:
sq,

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ n * f ^ 2 ^ n) 0 / (2 * 2 ^ n)| =
    |(f ^ 2 ^ n) 0 / 2 ^ n - (f ^ 2 ^ n) ((f ^ 2 ^ n) 0) / (2 * 2 ^ n)|
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ sᶜ = 0
⊢ False

Tactic:
refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
    rwa [disjoint_right] at hd

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 : τ
⊢ ϕ.toFun t '' s ⊆ s

Tactic:
by rw [h t]

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

Goal state before:
pp: α : 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 : α
hx1 : f x ≠ 0
hx2 : f x ≠ ∞
⊢ f x * ((f x)⁻¹ * μ.rnDeriv ν x) = μ.rnDeriv ν x

Tactic:
simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]

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
    rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
    exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩

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₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
rintro (hy | hy)

Goal state after:
case mpr.inl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₁
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)

case mpr.inr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₂
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
x✝ : Nonempty ↥s
y : X
y_F : y ∈ F
key : ∀ (k : Fin n), ∃ z, y ∈ T^[m * ↑k] ⁻¹' ball (↑z) (dynEntourage T U m)
⊢ ∃ y_1 ∈ ↑sn.toFinset, (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)

Tactic:
choose! t ht using key

Goal state after:
case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝¹ : Nonempty X
s_nemp : s.Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
x✝ : Nonempty ↥s
y : X
y_F : y ∈ F
t : Fin n → ↥s
ht : ∀ (k : Fin n), y ∈ T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ ∃ y_1 ∈ ↑sn.toFinset, (y, y_1) ∈ dynEntourage T (U ○ U) (m * n)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst✝] (image2 ϕ.toFun u s) ∩ o).Nonempty
l₃ : (o ∩ image2 ϕ.toFun u s).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rcases l₃ with ⟨ϕra, ho, ⟨_, hr, _, ha, hϕra⟩⟩

Goal state after:
τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst✝] (image2 ϕ.toFun u s) ∩ o).Nonempty
ϕra : α
ho : ϕra ∈ o
w✝¹ : τ
hr : w✝¹ ∈ u
w✝ : α
ha : w✝ ∈ s
hϕra : ϕ.toFun w✝¹ w✝ = ϕra
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
filter_upwards [inv_rnDeriv hμν] with x hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.inl
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 = ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

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 < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
· simp [*]

Goal state after:
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 < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
⊢ s.card < (insert x s).card

Tactic:
refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
x_s : x ∈ s
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ

Tactic:
setIntegral_toReal_rnDeriv hμν Set.univ

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.real Set.univ = μ.real Set.univ
Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ ⁅b⁻¹, a⁻¹⁆ ∈ (commutator G).topologicalClosure

Tactic:
exact Subgroup.le_topologicalClosure _ (Subgroup.commutator_mem_commutator
            (Subgroup.mem_top b⁻¹) (Subgroup.mem_top a⁻¹))

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

Goal state before:
pp: case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
⊢ Nonempty (K ≃+* L)

Tactic:
let : CharZero K := CharP.charP_to_charZero K

Goal state after:
case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this : CharZero K := CharP.charP_to_charZero K
⊢ Nonempty (K ≃+* L)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u_1
inst✝ : (constantsOn α).Structure M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(L.con a)

Tactic:
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Tactic:
exact h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
Functions.apply₁,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (func f ![t]) = funMap f ![realize v t]
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ (funMap f fun i ↦ ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
change
    Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) =
      _
  rw [Quotient.finChoice_eq, Quotient.map_mk]

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: case func
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
ih : ∀ (a : Fin l✝), realize (fun i ↦ ⟦x i⟧) (_ts✝ a) = ⟦realize x (_ts✝ a)⟧
⊢ realize (fun i ↦ ⟦x i⟧) (func _f✝ _ts✝) = ⟦realize x (func _f✝ _ts✝)⟧

Tactic:
simp only [ih, funMap_quotient_mk', Term.realize]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ⋃ i,
        ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ∩
          (diagonal α)ᶜ

Tactic:
← iUnion_inter

Goal state after:
L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)) ∩
        (diagonal α)ᶜ)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ (L.lhomWithConstants ↑A).substructureReduct (((closure L).toFun (A ∪ s)).withConstants ⋯) ≤
    (L.lhomWithConstants ↑A).substructureReduct ((closure L[[↑A]]).toFun s)

Tactic:
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
    Set.union_subset_iff, and_true]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ A ⊆ ↑((closure L[[↑A]]).toFun s)
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
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
by
  let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin γ))
  rw [Formula.iExs]
  simp only [Nat.add_zero, realize_exs, realize_relabel, Function.comp_def,
    castAdd_zero, Sum.elim_map, id_eq]
  refine Equiv.exists_congr ?_ ?_
  · exact ⟨fun v => v ∘ e, fun v => v ∘ e.symm,
      fun _ => by simp [Function.comp_def],
      fun _ => by simp [Function.comp_def]⟩
  · intro x
    rw [Formula.Realize, iff_iff_eq]
    congr
    funext i
    exact i.elim0

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_2
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 ⊕ ℕ)
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 =
      some ⟨φ_n, ts i⟩
⊢ listDecode
      (drop φ_l (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)) ++ drop (φ_l - (finRange φ_l).length) l) =
    listDecode l

Tactic:
length_finRange,

Goal state after:
case rel.refine_2
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 ⊕ ℕ)
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 =
      some ⟨φ_n, ts i⟩
⊢ listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)) ++ drop (φ_l - φ_l) l) = listDecode l
Module: Mathlib.ModelTheory.Definability

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

Tactic:
Formula.realize_not

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ ¬φ.Realize v ↔ ¬φ.Realize v
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)
hf : A.Definable L s
⊢ A.Definable L sᶜ

Tactic:
rcases hf with ⟨φ, hφ⟩
  refine ⟨φ.not, ?_⟩
  ext v
  rw [hφ, compl_ofPred, mem_ofPred, mem_ofPred, Formula.realize_not]

Goal state after: