mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons
α : 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'
m : s.think ∈ c :: l
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
⊢ s ∈ l'

Tactic:
simp only [List.mem_cons] at m

Goal state after:
case cons
α : 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' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think = c ∨ s.think ∈ l
⊢ s ∈ l'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).destruct.destruct = Sum.inl (some (a, s))

Tactic:
simp [destruct, cons, Computation.rmap]

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

Goal state before:
pp: case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
⊢ enumerate sel s (m' + 1) = none

Tactic:
| succ m' =>

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

Goal state before:
pp: α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c.destruct c.destruct

Tactic:
by cases c.destruct <;> simp

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

Goal state before:
pp: case step
α : Type u
s : WSeq α
m n m✝ : ℕ
a✝ : m.le m✝
IH : (s.get? m✝).Terminates → (s.get? m).Terminates
⊢ (s.get? m✝.succ).Terminates → (s.get? m).Terminates

Tactic:
exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

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

Goal state before:
pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.tail.get? n ~ t.tail.get? n

Tactic:
get?_tail,

Goal state after:
case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.get? (n + 1) ~ t.tail.get? n
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ ∃ c ∈ S, a ∈ c

Tactic:
suffices
    ∀ C, a ∈ C → ∀ (l : List (Computation α)) (S),
      corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c from
    let ⟨c, h1, h2⟩ := this _ h [] S rfl
    ⟨c, h1.resolve_left <| List.not_mem_nil, h2⟩

Goal state after:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ ∀ (C : Computation α),
    a ∈ C →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
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.nil.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
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = ss.think
m : a ∈ nil.append (cons x✝ s✝).join
this : Seq.destruct (nil.append (cons x✝ s✝).join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s

pp: case h2.nil.think
α : 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 α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
this : Seq.destruct (nil.append s✝.think.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, 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

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

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

Goal state after:
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

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
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
refine ⟨List.Lex.rel, fun e ↦ ?_⟩

Goal state after:
case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
⊢ c₁ < c₂
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
c : Computation (Option (α × WSeq α))
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c.destruct
    c.destruct

Tactic:
by cases c.destruct <;> simp

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inr
α : Type u_1
k : ℕ
h✝ : Infinite α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
cases k <;> simp

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l <*>
      traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))

Tactic:
hl,

Goal state after:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l) <*>
      traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r = pure (node (f v) (map f l) (map f r))

Tactic:
hl,

Goal state after:
case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : BinaryTree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r = pure (node (f v) (map f l) (map f r))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join ~ʷ S.join.append T.join

Tactic:
refine
    ⟨fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)),
      ⟨nil, S, T, by simp, by simp⟩, ?_⟩
  intro s1 s2 h
  apply
    liftRel_rec
      (fun c1 c2 =>
        ∃ (s : WSeq α) (S T : _),
          c1 = destruct (append s (join (append S T))) ∧
            c2 = destruct (append s (append (join S) (join T))))
      _ _ _
      (let ⟨s, S, T, h1, h2⟩ := h
      ⟨s, S, T, congr_arg destruct h1, congr_arg destruct h2⟩)
  rintro c1 c2 ⟨s, S, T, rfl, rfl⟩
  induction s using WSeq.recOn with
  | nil =>
    induction S using WSeq.recOn with
    | nil =>
      simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
    | cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
    | think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
  | cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
  | think s => simpa using ⟨s, S, T, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ node <$> (fun {α} ↦ η.app α) (f v) <*> (fun {α} ↦ η.app α) (traverse f l) <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r

Tactic:
hl,

Goal state after:
case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : BinaryTree α
hl : (fun {α} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ node <$> (fun {α} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> (fun {α} ↦ η.app α) (traverse f r) =
    node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
refine funext fun j => j.cases' ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: 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, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
    have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
      Continuous.tendsto' (by fun_prop) _ _ (by simp)
    rw [nhds_prod_eq] at this
    simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ closedBall x ε =ᵐ[volume] ball x ε

Tactic:
by
  rcases le_or_gt ε 0 with hε | hε
  · rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall,
      min_eq_right (by linarith [hT.out] : 2 * ε ≤ T), ENNReal.ofReal_eq_zero]
    exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε
  · suffices volume (closedBall x ε) ≤ volume (ball x ε) from
      (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this
        measurableSet_ball.nullMeasurableSet (measure_ne_top _ _)).symm
    have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) := by
      simp_rw [volume_closedBall]
      refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
      exact nhdsWithin_le_nhds
    refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_
    exact measure_mono (closedBall_subset_ball hr.2)

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ |n| ^ j ∣ n ^ j

Tactic:
← abs_pow,

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ |n ^ j| ∣ n ^ j
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |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
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic f volume

Tactic:
rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h

Goal state after:
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
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y

Tactic:
abel

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

Goal state before:
pp: 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
⊢ f ⁻¹' sᶜ = sᶜ

Tactic:
preimage_compl,

Goal state after:
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
⊢ (f ⁻¹' s)ᶜ = sᶜ
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : ¬p.mulOccursInAt x (h * g)
⊢ ¬p.mulOccursInAt (mulShift h x) g

Tactic:
contrapose! hx

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : p.mulOccursInAt (mulShift h x) g
⊢ p.mulOccursInAt x (h * g)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
let t := hνν'.nullSet

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.Dynamics.OmegaLimit

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

Tactic:
simp only [omegaLimit_image_eq, ← map_add]

Goal state after:
τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddMonoid τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x ↦ x + t) f f
⊢ ω f (fun t_1 x ↦ ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
← setLIntegral_univ,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∫⁻ (x : α) in Set.univ, μ.rnDeriv ν x ∂ν = μ Set.univ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
by
  rw [setIntegral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν,
    measureReal_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
⊢ ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹ → μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
h6

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
⊢ μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹

Tactic:
filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
h6

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹