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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rw [wrepr, recF_eq', q.P.wDest'_wMk]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, splitFun f' f⟩)) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec.{u} n} (x : Sigma F α), Sigma.abs F (Sigma.repr F x) = x

Tactic:
by rintro α ⟨x, f⟩; simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv (g <$$> (P F).wMk a f' f₀) (g <$$> (P F).wMk a f' f₁)

Tactic:
q.P.w_map_wMk,

Goal state after:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv ((P F).wMk a (g ⊚ f') fun i ↦ g <$$> f₀ i) (g <$$> (P F).wMk a f' f₁)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv (g <$$> (P F).wMk a₀ f'₀ f₀) (g <$$> (P F).wMk a₁ f'₁ f₁)

Tactic:
q.P.w_map_wMk,

Goal state after:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₀ (g ⊚ f'₀) fun i ↦ g <$$> f₀ i) (g <$$> (P F).wMk a₁ f'₁ f₁)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
rintro ⟨u, xeq, yeq⟩
    rcases h : repr u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, ← abs_repr u, h, ← abs_map]
      rfl
    constructor
    · rw [← yeq, ← abs_repr u, h, ← abs_map]
      rfl
    intro i
    exact (f i).property

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ((P F).wDest' ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ (recF g ∘ fixToW) (Quot.mk (⇑Wsetoid) x) = rec g (Quot.mk (⇑Wsetoid) x)

Tactic:
apply recF_eq_of_Wequiv

Goal state after:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (fixToW (Quot.mk (⇑Wsetoid) x)) x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x

Tactic:
rw [← appendFun_comp, id_comp]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation

pp: case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation

Tactic:
· rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_uniform] at h'
    dsimp only [SuppPreservation, supp] at h
    rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
    simp

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case zero.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
⊢ 0 = 0 + (m + 1)

Tactic:
| succ m =>

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
⊢ k + 1 = k + 1 + m

Tactic:
rw [show k + 1 + m = (k + m) + 1 by lia] at h₂
    cases h : sel s <;> simp_all [enumerate]; tauto

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

Goal state before:
pp: case h1.inr
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : ∃ n, some a ∈ s'.get? n
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
· obtain ⟨n, h⟩ := h
      exists n + 1
      simpa [get?]

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ hs.toFinset.card = (⋯.toFinset.sigma fun t ↦ ⋯.toFinset).card

Tactic:
eq_comm

Goal state after:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ (⋯.toFinset.sigma fun t ↦ ⋯.toFinset).card = hs.toFinset.card
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ n * ∏ i ∈ range n, ↑(i + 1)

Tactic:
nth_rw 2 [← card_range n]

Goal state after:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ #(range n) * ∏ i ∈ range n, ↑(i + 1)
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ MeasurePreserving (f ∘ ⇑e.symm) μ' μ ↔ MeasurePreserving f μ μ

Tactic:
(MeasurePreserving.symm e h).comp_right_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ MeasurePreserving f μ μ ↔ MeasurePreserving f μ μ
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s

Tactic:
rw [ae_ae_comm]

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s

G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet {x | x.2 * x.1 ∈ s ↔ x.1 ∈ s}
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s

Tactic:
rw [ae_ae_comm]

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s

G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet {x | x.1 * x.2 ∈ s ↔ x.1 ∈ s}
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f (1 + x) = 1 + f x

Tactic:
add_comm,

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ f (x + 1) = 1 + f x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ⇑F ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ⇑F ⇑↑f₁ ⇑↑f₂

Tactic:
simpa using hF (Multiplicative.ofAdd 1)

Goal state after:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ IsAddFundamentalDomain (↥G) I volume

Tactic:
set n := addOrderOf u

Goal state after:
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
hI : I =ᵐ[volume] ball x (T / (2 * ↑n))
⊢ IsAddFundamentalDomain (↥G) I volume
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[k + n] x ∈ s
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = n • DivisibleBy.div x (n - 1) - DivisibleBy.div x (n - 1) + DivisibleBy.div x (n - 1)

Tactic:
sub_add_cancel

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = n • DivisibleBy.div x (n - 1)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_6
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
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ.singularPart ν = μ.restrict (f ⁻¹' s)

Tactic:
refine singularPart_eq_restrict ?_ (hfν.preimage_null hνs)
    rw [← mem_ae_iff, ← Filter.eventuallyEq_univ,
      ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]
    calc
      μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) := by
        rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
        rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
      _ = μ.singularPart ν s := by
        rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
      _ = μ.singularPart ν univ := by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]

Goal state after:
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 ≠ ∞
| ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν

Tactic:
add_comm,

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
| ((ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).withDensity f).rnDeriv ν
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s + μ sᶜ) / c = 1

Tactic:
measure_add_measure_compl hsm,

Goal state after:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ univ / c = 1
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ IsClosed[Pi.topologicalSpace] (cylinder U x)

Tactic:
simpa [cylinder_eq_set_pi U x] using isClosed_set_pi (by simp)

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

Goal state before:
pp: case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ {x | p.mulOccursInAt x g} → x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)

Tactic:
intro H

Goal state after:
case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}

Tactic:
intro H

Goal state after:
case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
⊢ x ∈ {x | p.mulOccursInAt x g}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
⊢ Function.LeftInverse
    (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩) fun p i ↦
    (↑p).config ↑i

Tactic:
by
      rintro ⟨⟨cfg, dom, cond⟩, hU⟩
      simp only at hU; subst hU
      apply Subtype.ext
      simp only [Pattern.mk.injEq, and_true]
      funext g
      by_cases hg : g ∈ dom
      · simp [hg]
      · simp [hg, cond g hg]

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

Goal state before:
pp: case inl
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
t : Fin n → ↥s
inter_empt : ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) = ∅
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
exact inter_empt ▸ ⟨x, empty_subset _⟩

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 α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen[inst✝¹] v
hv₂ : ω f ϕ s ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v

Tactic:
rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ with ⟨u, hu_mem, hu⟩

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen[inst✝¹] v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure[inst✝¹] (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F univ n).2 h)
  obtain ⟨x, _⟩ := h
  have := isDynCoverOf_univ T F n (singleton_nonempty x)
  rw [← Finset.coe_singleton] at this
  apply this.coverMincard_le_card.trans_eq
  rw [Finset.card_singleton, Nat.cast_one]

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μ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
⊢ 0 < (μ + ν).rnDeriv ξ a → μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
h_pos

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv ξ a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)
  have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right' _)
  have h_ac : μ + ν ≪ ξ := hμ.add_left hν
  filter_upwards [h_ac h1, h_ac h2, h_ac <| (μ + ν).rnDeriv_lt_top ξ, ν.rnDeriv_lt_top (μ + ν),
    Measure.rnDeriv_pos h_ac] with a h1 h2 h_lt_top1 h_lt_top2 h_pos
  rw [← h1, ← h2, Pi.mul_apply, Pi.mul_apply, div_eq_mul_inv,
    ENNReal.mul_inv (Or.inr h_lt_top1.ne) (Or.inl h_lt_top2.ne), div_eq_mul_inv, mul_assoc,
    mul_comm ((μ + ν).rnDeriv ξ a), mul_assoc, ENNReal.inv_mul_cancel h_pos.ne' h_lt_top1.ne,
    mul_one]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ (a ^ c)

Tactic:
map_pow,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ a ^ c
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (a ^ d) = (a ^ d) ^ c

Tactic:
map_pow,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ a ^ d = (a ^ d) ^ c
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β) in f '' s, (map f μ).rnDeriv (map f ν) a ∂map f ν = μ (f ⁻¹' f '' s)

Tactic:
Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ (map f μ) (f '' s) = μ (f ⁻¹' f '' s)