mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d

pp: case right.right.right
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
· exact eq hb''

Goal state after:
case right.right.right
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑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.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) (corecF g x)) = (TypeVec.id ::: corec g) <$$> g x

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map, ← appendFun_comp]

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
⊢ id <$> x = x

Tactic:
rw [← abs_repr x]
  obtain ⟨a, f⟩ := repr x
  rw [← abs_map]
  rfl

Goal state after:
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₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (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))
      a₂ ∧
    Raised
      (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
      (t_l.size + t_r.size + 1)

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₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (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))
      a₂ ∧
    Raised
      (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
      (t_l.size + t_r.size + 1)

Tactic:
· have h_glue := Valid'.glue h.left h.right h.bal.1
      obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
      constructor
      · exact h_glue_valid
      · right; rw [h_glue_sized]

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₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (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))
      a₂ ∧
    Raised
      (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
      (t_l.size + t_r.size + 1)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    (Quot.factor r (fun x y ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest

Tactic:
@comp_map _ q _ _ _ (Quot.mk r)

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
z : ℤ
hn : z < 0
⊢ (↑z).sign = ↑z.sign

Tactic:
rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg,
      Int.cast_one]

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

Goal state before:
pp: α : 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 α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro s IH l S m

Goal state after:
α : 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
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C (Seq.cons none s')

Tactic:
apply h2
    cases h
    · contradiction
    · assumption

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

Goal state before:
pp: α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
⊢ (⋃ x, K x) ×ˢ ⋃ x, K' x = s ×ˢ t

Tactic:
K.iUnion_eq,

Goal state after:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
⊢ s ×ˢ ⋃ x, K' x = s ×ˢ t
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
n : ℕ
⊢ (K.prod K') n = K n ×ˢ K' n

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ op a ∈ s.op ↔ a ∈ s

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ unop a ∈ s.unop ↔ a ∈ s

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rcases o with a | a

Goal state after:
case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

case inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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 α
o : c ∈ l ∨ some (some c) = S.get? (n + 1)
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rcases o with a | a

Goal state after:
case inl
α : 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 : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

case inr
α : 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)
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
i₀ : ι
f : (j : { i // i ≠ i₀ }) → M ↑j
x : M i₀
i : ι
h : i = i₀
⊢ M i

Tactic:
by rw [h]; exact x

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

Goal state before:
pp: case nil.cons
α : 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 α)
s : WSeq α
S : 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 ((cons s S).append T).join).destruct.destruct
    (nil.append ((cons s S).join.append T.join)).destruct.destruct

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩

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

Goal state before:
pp: case cons
α : 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)
S T : WSeq (WSeq α)
a : α
s : 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)
    ((cons a s).append (S.append T).join).destruct.destruct ((cons a s).append (S.join.append T.join)).destruct.destruct

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩

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

Goal state before:
pp: case think
α : 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)
S T : WSeq (WSeq α)
s : 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)
    (s.think.append (S.append T).join).destruct.destruct (s.think.append (S.join.append T.join)).destruct.destruct

Tactic:
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
⊢ (fun {α} ↦ η.app α) (traverse f (node v l r)) = traverse (η.app β ∘ f) (node v l r)

Tactic:
rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val

Tactic:
rw [snoc_cons, ih]

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

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

Tactic:
rw [sumLexLift, mem_map]
      rintro ⟨c, hc, rfl⟩
      exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Goal state after:
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: case succ
α : Type u_1
n✝ : ℕ
a : α
n : ℕ
a✝ : ∀ (v : Vector α n), a ∈ v.tail.toList → a ∈ v.toList
v : Vector α (n + 1)
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
exact (mem_succ_iff a v).2 (Or.inr ha)

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ (mapAccumr f xs s).2 = map f' xs

Tactic:
by
  rw [mapAccumr_eq_map Set.univ (Set.mem_univ _) (fun _ _ _ => Set.mem_univ _)
    (fun a s s' _ _ => by rw [h, h])]
  simp_all

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᵐ[μ] t
g : G
⊢ g • s =ᵐ[μ] t ↔ g • t =ᵐ[μ] t

Tactic:
((smul_set_ae_eq g).2 h).congr_left

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᵐ[μ] t
g : G
⊢ g • t =ᵐ[μ] t ↔ g • t =ᵐ[μ] t
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
Nat.cast_add_one,

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ ↑n * τ f + τ f = (↑n + 1) * τ f
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) / (↑n + 1) ≤ 1 / ↑(n + 1)

Tactic:
Nat.cast_add_one,

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) ((↑n + 1) * τ f) / (↑n + 1) ≤ 1 / (↑n + 1)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : ∀ {μ : Measure X} [IsFiniteMeasure μ], MeasurePreserving f μ μ → μ ≪ ν → μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

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μν : μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

Tactic:
· specialize this (hfμ.withDensity_rnDeriv hfν) (withDensity_absolutelyContinuous _ _)
    refine .trans (.trans ?_ this) (rnDeriv_withDensity ν (measurable_rnDeriv μ ν))
    apply hfν.quasiMeasurePreserving.ae_eq_comp
    exact (rnDeriv_withDensity ν (measurable_rnDeriv μ ν)).symm

Goal state after:
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μν : μ ≪ ν
⊢ μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
refine setIntegral_mono_set ?_ ?_ (LE.le.eventuallyLE (subset_toMeasurable _ _))

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) t ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ 0 ≤ᵐ[ν.restrict t] fun x ↦ (μ.rnDeriv ν x).toReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ 0 ≤ᵐ[ν.restrict t] fun x ↦ (μ.rnDeriv ν x).toReal

Tactic:
· exact integrableOn_toReal_rnDeriv hμt

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ 0 ≤ᵐ[ν.restrict t] fun x ↦ (μ.rnDeriv ν x).toReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.singularPart ν).rnDeriv κ x = 0 x → (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x

Tactic:
hx3

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case refine_1
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

Tactic:
apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add
    rw [Pi.add_apply, ← ENat.toENNReal_add]
    exact ENat.toENNReal_mono (coverMincard_union_le T F G U n)

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this :
  { toFun := coverEntropy T, map_sup' := ⋯ } (⋃ x ∈ s, F x) =
    ⨆ a ∈ s, (⇑{ toFun := coverEntropy T, map_sup' := ⋯ } ∘ F) a
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)

Tactic:
SupHom.coe_mk

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n - (aeval b) (C a) = 0
⊢ (σ * τ) b = (τ * σ) b

Tactic:
aeval_C,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n - (algebraMap F (X ^ n - C a).SplittingField) a = 0
⊢ (σ * τ) b = (τ * σ) b
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ∈ (X ^ n - C a).rootSet (X ^ n - C a).SplittingField
⊢ (σ * τ) b = (τ * σ) b

Tactic:
rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
⊢ (σ * τ) b = (τ * σ) b