mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ((f ⊚ prod.fst) ⊚ prod.diag) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ prod.fst ⊚ prod.diag) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ ((prod.snd ⊚ subtypeVal R) ⊚ h) <$$> x = g <$$> x

Tactic:
comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R ⊚ h) <$$> x = g <$$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ ((g ⊚ prod.snd) ⊚ prod.diag) <$$> x = g <$$> x

Tactic:
comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ prod.snd ⊚ prod.diag) <$$> x = g <$$> x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Tactic:
rw [sign_of_pos hp] at h

Goal state after:
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
h : r.sign = 0
hp : 0 < r
⊢ r = 0

Tactic:
rw [sign_of_pos hp] at h
    exact (one_ne_zero h).elim

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ a f f',
        (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
x✝¹ : α
Qx : Q x✝¹
R : Cofix F → Cofix F → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
x✝ : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs ⟨a, f⟩
vx'eq : (v x').dest = abs ⟨a, f'⟩
h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∃ a f₀ f₁, x.dest = abs ⟨a, f₀⟩ ∧ y.dest = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)

Tactic:
exact ⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑(x.num * x.den ^ (n - 1)) * (↑x.den)⁻¹ ^ n

Tactic:
push_cast

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * ↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : s.think = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ s :: ls✝ = l' → s ∈ l'

Tactic:
rintro rfl

Goal state after:
case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
e : s.think = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ s ∈ s :: ls✝
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).destruct.destruct = Sum.inl (Option.map (fun a ↦ (a, ↑s.tail)) s.head)

Tactic:
by
    simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]
    rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
    rcases Seq.get? s 0 with - | a
    · rfl
    dsimp only [(· <$> ·)]
    simp

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (↑(s.drop n)).head = Computation.pure (s.get? n)

Tactic:
head_ofSeq,

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ Computation.pure (s.drop n).head = Computation.pure (s.get? n)
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < ⟨i, a⟩

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩

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

Goal state before:
pp: case H
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
        (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct

Tactic:
exact fun {c1 c2} h =>
      match c1, c2, h with
      | _, _, ⟨s, rfl, rfl⟩ => by
        clear h
        have (s : WSeq α) : ∃ s' : WSeq α,
            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
          ⟨s, rfl, rfl⟩
        induction s using WSeq.recOn <;> simp [ret, this]

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False

Tactic:
let ⟨c, cs, _⟩ := exists_of_mem_parallel m
    let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
    let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
    injection h h'

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map ((join ∘ map g) ∘ f) s).join

Tactic:
comp_assoc,

Goal state after:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map (join ∘ map g ∘ f) s).join
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 S
⊢ a' ∈ parallel T

Tactic:
have aa := parallel_promises h1 h
    rw [← aa]
    rw [← aa] at h
    exact
      let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_left H sS
      let aT := (st _).1 as
      mem_parallel h2 tT aT

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
hs : f ⁻¹' s = s
⊢ EventuallyConst s (ae μ)

Tactic:
refine h₂ hm fun n ↦ ?_

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
n : IterateMulAct f
⊢ (fun x ↦ n • x) ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case inr
α : 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
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

Tactic:
have H : 0 < ε / 3 := ENNReal.div_pos hε.ne' ENNReal.coe_ne_top

Goal state after:
case inr
α : 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
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
push_cast

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

Tactic:
set F₂ := toOrderIso.comp f₂.toHomUnits

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ Disjoint (ball (g + x) (T / (2 * ↑n))) B

Tactic:
apply ball_disjoint_ball

Goal state after:
case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := ⋯
n : ℕ := ⋯
B : Set (AddCircle T) := ⋯
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ dist (g + x) x
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c

Tactic:
refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_

Goal state after:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, g x ∉ U
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := ⋯
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ μ (s \ f ⁻¹' s) < μ (f ⁻¹' s \ s)

Tactic:
calc
    μ (s \ f ⁻¹' s) = ∫⁻ a in s \ f ⁻¹' s, μ.rnDeriv ν a ∂ν := (setLIntegral_rnDeriv hμν _).symm
    _ < ∫⁻ _ in s \ f ⁻¹' s, c ∂ν := by
      apply setLIntegral_strict_mono (hsm.diff (hfμ.measurable hsm)) (hν_sdiff ▸ h₀)
        measurable_const
      · rw [setLIntegral_rnDeriv hμν]
        finiteness
      · exact .of_forall fun x hx ↦ hx.1
    _ = ∫⁻ _ in f ⁻¹' s \ s, c ∂ν := by simp [hν_sdiff]
    _ ≤ ∫⁻ a in f ⁻¹' s \ s, μ.rnDeriv ν a ∂ν :=
      setLIntegral_mono (by fun_prop) (fun x hx ↦ not_lt.mp hx.2)
    _ = μ (f ⁻¹' s \ s) := setLIntegral_rnDeriv hμν _

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
U : Finset G
x : G → A
⊢ cylinder U x = (↑U).pi fun i ↦ {x i}

Tactic:
ext y; simp [cylinder, Set.pi]

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

Goal state before:
pp: case h
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
⊢ IsDynCoverOf T F U n {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s

Tactic:
refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩

Goal state after:
case h
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
y : X
y_F : y ∈ F
⊢ ∃ y_1 ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, (y, y_1) ∈ dynEntourage T U n
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
hc₂ : ∃ v ∈ f, closure[inst✝] (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n

Tactic:
rcases hc₂ with ⟨v, hv₁, hv₂⟩
  let k := closure (image2 ϕ v s)
  have hk : IsCompact (k \ n) :=
    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
  let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
  have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
  have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u := by
    have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
    rw [this, sdiff_subset_comm, sdiff_iUnion]
    rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
    simp_rw [j, sdiff_compl]
    rw [← inter_iInter]
    exact Subset.trans inter_subset_right hn₂
  rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
  let w := (⋂ u ∈ g, u) ∩ v
  have hw₂ : w ∈ f := by simpa [w, *]
  have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ := by
    apply Subset.trans hg₃
    simp only [j, iUnion_subset_iff, compl_subset_compl]
    intro u hu
    unfold w
    gcongr
    refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
    all_goals exact Subset.rfl
  have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ := by
    simp only [compl_subset_compl]
    exact closure_mono (image2_subset inter_subset_right Subset.rfl)
  have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, sdiff_eq, inter_comm]
  have hw : closure (image2 ϕ w s) ⊆ n :=
    compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
  exact ⟨_, hw₂, hw⟩

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ netMaxcard T F U n ↔ F.Nonempty

Tactic:
Order.one_le_iff_ne_zero,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F.Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ coverMincard T ∅ U n ≤ 0

Tactic:
exact sInf_le (by simp [IsDynCoverOf])

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 : ℕ
⊢ 1 ≤ coverMincard T F U n ↔ F.Nonempty

Tactic:
Order.one_le_iff_ne_zero,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n ≠ 0 ↔ F.Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h✝ : x ∈ F
⊢ coverMincard T F U 0 ≤ 1

Tactic:
have := isDynCoverOf_zero T F U (singleton_nonempty x)

Goal state after:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 {x}
⊢ coverMincard T F U 0 ≤ 1
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
⊢ ((fun x1 x2 ↦ x1 * x2) a b)⁻¹ * (fun x1 x2 ↦ x1 * x2) b a ∈ (commutator G).topologicalClosure

Tactic:
have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆ := by group
          rw [h]
          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: R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
by simpa using hR

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_2
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 : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = ((fun f ↦ f.comp h) f).comp h.symm

Tactic:
comp_assoc,

Goal state after:
case e'_2
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 : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = f.comp (h.comp h.symm)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case e'_3
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 : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = ((fun f ↦ f.comp h) g).comp h.symm

Tactic:
comp_assoc,

Goal state after:
case e'_3
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 : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ g = g.comp (h.comp h.symm)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case imp
α : 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
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin n✝ → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) →
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a) ↔
    ∀ᶠ (a : α) in ↑u, (f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) → f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
rw [Ultrafilter.eventually_imp]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
mk_sum,

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(α ⊕ (i : ℕ) × L.Functions i)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
mk_sum,

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(α ⊕ (i : ℕ) × L.Functions i)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
mk_sum,

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))