mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
      le_trans (Nat.dist_tri_left' _ _)
        (le_trans (add_le_add hr (le_trans (Nat.le_add_left _ _) h)) (by lia))

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (u.prod ^ m).factorMultiset = m • u.prod.factorMultiset

Tactic:
← PrimeMultiset.prod_smul

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
rw [hlt₁.antisymm hlt₂]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
⊢ (x ∈ piFinset fun i ↦ Icc (a i) (b i)) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
⊢ let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
a'

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
⊢ let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
⊢ ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ

Tactic:
a'

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' ⟹ α), abs ⟨a', f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a : (P F).A
⊢ ∀ (a' : (P F).A) (f : (P F).B a ⟹ α) (f' : (P F).B a' ⟹ α),
    abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ

Tactic:
a'

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
⊢ ∀ (f : (P F).B a ⟹ α) (f' : (P F).B a' ⟹ α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (match Ordering.lt with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    (match Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
      (node size✝ t_l t_x t_r).size - 1

Tactic:
intro h_mem

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem :
  (match Ordering.lt with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
⊢ (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
    (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (match Ordering.eq with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    (match Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
      (node size✝ t_l t_x t_r).size - 1

Tactic:
intro h_mem

Goal state after:
case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem :
  (match Ordering.eq with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
⊢ (match Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
    (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (match Ordering.gt with
      | Ordering.lt => mem x t_l
      | Ordering.eq => true
      | Ordering.gt => mem x t_r) =
      true →
    (match Ordering.gt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
      (node size✝ t_l t_x t_r).size - 1

Tactic:
intro h_mem

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem :
  (match Ordering.gt with
    | Ordering.lt => mem x t_l
    | Ordering.eq => true
    | Ordering.gt => mem x t_r) =
    true
⊢ (match Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size =
    (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₀⟩ = MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₁⟩

Tactic:
← split_dropFun_lastFun f₀,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
⊢ MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ splitFun (dropFun f₀) (lastFun f₀)⟩ =
    MvQPF.abs ⟨a, (TypeVec.id ::: Quot.mk r) ⊚ f₁⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
conv =>
        lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

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

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α β : Type u
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
⊢ f <$> abs ⟨b, fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩ = ?m.190

Tactic:
symm
      apply abs_map

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

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
⊢ ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ

Tactic:
a'

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' → α), abs ⟨a', f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a : (P F).A
⊢ ∀ (a' : (P F).A) (f : (P F).B a → α) (f' : (P F).B a' → α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ

Tactic:
a'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
⊢ ∀ (f : (P F).B a → α) (f' : (P F).B a' → α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Symm R
s1 s2 : WSeq α
h : Function.swap (LiftRel R) s2 s1
⊢ LiftRel R s2 s1

Tactic:
by rwa [LiftRel.swap, Std.Symm.swap_eq] at h

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

Goal state before:
pp: case inr.inr.some
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
D : S.destruct = some (o, S.tail)
⊢ (corec parallel.aux1
      (match some (o, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates

Tactic:
cases o <;> simp [TT]

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
t : ↑P
ht : t ∈ ⋯.toFinset
⊢ Nat.card ↑(s ∩ ↑t) = ?m.54 t

Tactic:
by exact hst' ↑t

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∧ ¬⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]

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

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

Tactic:
by
  dsimp [get?]; rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]

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

Goal state before:
pp: a b : String
⊢ a ≤ b ∨ b ≤ a

Tactic:
by
    simp only [le_iff_toList_le]
    apply le_total

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

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

Tactic:
simp only [nil_append, join_nil]

Goal state after:
case nil.nil
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    T.join.destruct.destruct T.join.destruct.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ s.bind (ret ∘ f) ~ʷ map f s

Tactic:
dsimp [bind]

Goal state after:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map (ret ∘ f) s).join ~ʷ map f s
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)
    (nil.append (nil.append SS.join).join).destruct.destruct
    (nil.append (nil.join.append (map join SS).join)).destruct.destruct

Tactic:
simp only [nil_append, join_nil]

Goal state after:
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
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
⊢ ↑((p - 1).descFactorial n) = (-1) ^ n * ↑n !

Tactic:
rw [descFactorial_eq_prod_range, factorial_eq_prod_range_add_one]
  simp only [cast_prod]
  nth_rw 2 [← card_range n]
  rw [pow_card_mul_prod]
  refine prod_congr rfl ?_
  intro x hx
  rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]

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 β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
by
  have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
    rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
  replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
  exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
    fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩

Goal state after:
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
⊢ ErgodicSMul Gᵐᵒᵖ G μ

Tactic:
refine ⟨fun {s} hsm hs ↦ ?_⟩
  suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
  intro hμs
  obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (a * b ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff
    · exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
  simpa [has] using (quasiMeasurePreserving_mul_left μ a⁻¹).ae ha

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

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

Tactic:
← abs_of_pos this

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
rw [Real.dist_eq, div_sub' (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this,
    Nat.cast_add_one, div_le_div_iff_of_pos_right this, ← Nat.cast_add_one]

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
⊢ IsClosed[inst✝²] {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}

Tactic:
by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro z hz
  replace hz : ∀ᶠ ε : ℝ≥0∞ in 𝓝 0, ε < μ ((f z ⁻¹' t) ∆ s) := by
    apply gt_mem_nhds
    rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
  filter_upwards [(tendsto_measure_symmDiff_preimage_nhds_zero (hf.tendsto z)
    (.of_forall hfm) (hfm z) htm ht).eventually hz] with w hw
  intro (hw' : f w ⁻¹' t =ᵐ[μ] s)
  rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw
  exact hw.false

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
by
  rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩
  rcases hf.exists_mem_iterate_mem' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩
  exact ⟨x, hsub hxt, m, hm₀, hsub hmt⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
congr with x
      rw [mul_comm]
      simp only [Pi.mul_apply]

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

Goal state before:
pp: case intro
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
e : { p // p.support = U } ≃ (↥U → A) :=
  { toFun := fun p i ↦ (↑p).config ↑i,
    invFun := fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ {p | p.support = U}.Finite

Tactic:
let : Fintype { p : Pattern A G | p.support = U } := Fintype.ofEquiv (U → A) e.symm

Goal state after:
case intro
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
e : { p // p.support = U } ≃ (↥U → A) :=
  { toFun := fun p i ↦ (↑p).config ↑i,
    invFun := fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
this : Fintype ↑{p | p.support = U} := Fintype.ofEquiv (↥U → A) e.symm
⊢ {p | p.support = U}.Finite
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
have h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
    refine h_ac.ae_eq ?_
    simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]
    exact ⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν