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

Goal state before:
pp: case nil.nil
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.join.join.destruct.destruct (map join SS).join.destruct.destruct

Tactic:
induction SS using WSeq.recOn with

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

Goal state before:
pp: case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ g a b
⊢ (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ Embedding.inr c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ Embedding.inr c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ EventuallyConst s (ae μ')

Tactic:
by
    rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]
    apply hf.aeconst_set (hg.measurable hs₀)
    rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + ↑⌈g 0⌉ < f 0 + (g 0 + 1)

Tactic:
gcongr

Goal state after:
case bc
f g : CircleDeg1Lift
⊢ ↑⌈g 0⌉ < g 0 + 1
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + (g 0 - 1) < f 0 + ↑⌊g 0⌋

Tactic:
gcongr

Goal state after:
case bc
f g : CircleDeg1Lift
⊢ g 0 - 1 < ↑⌊g 0⌋
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤
    μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s))

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' U)) ≤ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
gcongr

Goal state after:
case h
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) < 1
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) + μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) + μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤
    ε / 3 + ε / 3 + ε / 3

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑(f a) ⁻¹' U)) ≤ ε / 3

case h₂
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ μ ((⇑g ⁻¹' U) ∆ (⇑g ⁻¹' s)) ≤ ε / 3
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ n) + τ f = ↑(n + 1) * τ f

Tactic:
translationNumber_pow n,

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ ↑n * τ f + τ f = ↑(n + 1) * τ f
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 / ↑n ≤ (g ^ n) 0 / ↑n

Tactic:
gcongr

Goal state after:
case hab
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 ≤ (g ^ n) 0
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ x + ↑⌊τ f⌋ + 1 ≤ x + τ f + 1

Tactic:
gcongr

Goal state after:
case h₂
f : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n

Tactic:
translationNumber_pow,

Goal state after:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : ↑n * τ f = ↑m
⊢ τ f = ↑m / ↑n
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, f x = x + ↑m

Tactic:
by
  constructor
  · intro h
    simp only [← h]
    exact f.exists_eq_add_translationNumber hf
  · rintro ⟨x, hx⟩
    exact f.translationNumber_of_eq_add_int hx

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ (⇑(f a) ⁻¹' s \ K) + μ (⇑g ⁻¹' s \ K) ≤ ε / 2 + ε / 2

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ (⇑(f a) ⁻¹' s \ K) ≤ ε / 2
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.zmultiples c)

Tactic:
AddSubgroup.zmultiples_eq_closure,

Goal state after:
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.closure {c})
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)

Goal state after:
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
⊢ a • V ⊆ sᶜ
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense ↑(AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples p) ↔ Dense ↑(AddSubgroup.closure {a, p})

Tactic:
AddSubgroup.zmultiples_eq_closure,

Goal state after:
a p : ℝ
⊢ Dense ↑(AddSubgroup.closure {a} ⊔ AddSubgroup.zmultiples p) ↔ Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense ↑(AddSubgroup.closure {a} ⊔ AddSubgroup.zmultiples p) ↔ Dense ↑(AddSubgroup.closure {a, p})

Tactic:
AddSubgroup.zmultiples_eq_closure,

Goal state after:
a p : ℝ
⊢ Dense ↑(AddSubgroup.closure {a} ⊔ AddSubgroup.closure {p}) ↔ Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0

pp: case succ.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[n + 1]^[m] (f^[k] x) ∈ s

Tactic:
· intro hm
    rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
    exact this.not_gt hkl

Goal state after:
case succ.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[n + 1]^[m] (f^[k] x) ∈ s
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (map f (ν.withDensity (μ.rnDeriv ν))) s + (μ.singularPart ν) s =
    (ν.withDensity (μ.rnDeriv ν)) s + (μ.singularPart ν) s

Tactic:
map_apply hfμ.measurable hs,

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s =
    (ν.withDensity (μ.rnDeriv ν)) s + (μ.singularPart ν) s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
| (μ.withDensity f).rnDeriv ν

Tactic:
rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]

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

Tactic:
refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm

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 ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ μ.singularPart ν ⟂ₘ ν.withDensity f
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F s : Set X
m n : ℕ
m_n : m ≤ n
h : IsDynCoverOf T F U n s
⊢ dynEntourage T U n ⊆ dynEntourage T U m

Tactic:
gcongr

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

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
F s : Set X
n : ℕ
U_V : U ⊆ V
h : IsDynCoverOf T F U n s
⊢ dynEntourage T U n ⊆ dynEntourage T V n

Tactic:
gcongr

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ closure[inst✝] (image2 ϕ ((⋂ u ∈ g, u) ∩ v) s) ⊆ closure[inst✝] (image2 ϕ (u ∩ v) s)

Tactic:
gcongr

Goal state after:
case h₁
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := ⋯
hk : IsCompact (k \ n)
j : Set τ → Set β := ⋯
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := ⋯
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ ⋂ u ∈ g, u ⊆ u
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 : α),
    (∀ n ∈ 𝓝 x, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty) →
      ∀ n ∈ 𝓝 x, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
intro _ h n hn u hu

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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
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
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n ↑{x}
⊢ False

Tactic:
replace key := key.card_le_netMaxcard

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 : x ∈ F
key : ↑{x}.card ≤ netMaxcard T F U n
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
    simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)) t).toReal ≤ (μ t).toReal

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := ⋯
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
obtain ⟨y, hxy, hy⟩ := mem_closure_iff_nhds.1 hx _ (ball_dynEntourage_mem_nhds h W_uni n x)

Goal state after:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤

Tactic:
exact le_top

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, (fun x ↦ m • x) ⁻¹' U)

Tactic:
simp only [dense_iff_inter_open, inter_iUnion, nonempty_iUnion, ← image_inter_nonempty_iff]
  exact ⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h.1 h₃ h₄ h₁ h₂, fun h ↦ ⟨fun h₁ h₂ h₃ h₄ ↦ h h₃ h₄ _ h₁ h₂⟩⟩

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U

Tactic:
refine ⟨fun _ _ h₀ h₁ h₂ ↦ h₀.dense_of_preimage_smul_invariant M h₁ h₂, fun h₄ ↦ ?_⟩

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U
⊢ IsTopologicallyTransitive M α
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤

Tactic:
exact le_top

Goal state after: