mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
h : (fib a + (map fib l).sum).greatestFib = a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
      add_tsub_cancel_left, zeckendorf_sum_fib hl.2]

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
t : ℕ
ht : f t = nth p 0
⊢ {i | p (f i)}.Nonempty

Tactic:
exact ⟨t, Set.mem_ofPred_eq ▸ ht ▸ h⟩

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a

Tactic:
refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ Set.ofPred p ⊆ ↑(range n)

Tactic:
intro n' hn'

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ Set.ofPred p
⊢ n' ∈ ↑(range n)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).toZNum.succ = ZNum.ofInt' ↑(n + 1)

Tactic:
ofInt'_toZNum n,

Goal state after:
n : ℕ
⊢ (ZNum.ofInt' ↑n).succ = ZNum.ofInt' ↑(n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = head' (x.approx 1)

Tactic:
rw [← head_succ' n, h, head']

Goal state after:
case Hconsistent
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ AllAgree x.approx
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / ↑d

Tactic:
d.to_int_eq_succ_pred,

Goal state after:
n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -↑d

Tactic:
d.to_int_eq_succ_pred,

Goal state after:
n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ∀ (x y : P.last.M),
    (∃ x_1 y_1, R x_1 y_1 ∧ x_1.fst = x ∧ y_1.fst = y) →
      ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i

Tactic:
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
⊢ ∃ a f f',
    PFunctor.M.dest ⟨a₁, f₁⟩.fst = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

Tactic:
rw [← agree_iff_agree']

Goal state after:
case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (x.approx (i + 1))
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, splitFun (dropFun fx) (lastFun fx)⟩ ∧
    ⟨ax, fy⟩ = ⟨ax, splitFun (dropFun fx) (lastFun fy)⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)

Tactic:
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, fx⟩ ∧ ⟨ax, fy⟩ = ⟨ax, fy⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size

Tactic:
rw [node', size_node, size_node]; generalize size r₂ = m at H ⊢
  rcases H with (rfl | rfl)
  · exact Or.inl rfl
  · exact Or.inr rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) l
⊢ Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size

Tactic:
induction l generalizing o₁ o₂ r with
  | nil => exact ⟨hr, (zero_add _).symm⟩
  | node ls ll lx lr _ IHlr => ?_
  induction r generalizing o₁ o₂ with
  | nil => exact ⟨hl, rfl⟩
  | node rs rl rx rr IHrl _ => ?_
  rw [merge_node]; split_ifs with h h_1
  · obtain ⟨v, e⟩ := IHrl (hl.of_lt hr.1.1.to_nil <| sep.imp fun x h => h.2.1) hr.left
      (sep.imp fun x h => h.1)
    exact Valid'.merge_aux₁ hl hr h v e
  · obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2
    have := Valid'.merge_aux₁ hr.dual hl.dual h_1 v.dual
    rw [size_dual, add_comm, size_dual, ← dual_balanceR, ← Valid'.dual_iff, size_dual,
      add_comm rs] at this
    exact this e
  · refine Valid'.glue_aux hl hr sep (Or.inr ⟨not_lt.1 h_1, not_lt.1 h⟩)

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

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
a✝ : (P F).M α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr a✝) y → Quot.mk Mcongr a✝ = y

Tactic:
rename M (P F) α => x

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x : (P F).M α
⊢ ∀ (y : Cofix F α), r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.bal.right.left
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f l✝).Balanced

pp: case node.bal.right.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f r✝).Balanced

Tactic:
· exact t_l_valid.bal

Goal state after:
case node.bal.right.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f r✝).Balanced
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 → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x y : Cofix F α
⊢ r x y → x = y

Tactic:
rxy

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 → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: 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
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 α
⊢ r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
rxy

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
⊢ (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 n
⊢ ∀ (j : (P F).B a a✝.fs), α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)

Tactic:
intro j
        apply Eq.refl

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

Goal state before:
pp: 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
⊢ r x y → x = y

Tactic:
rxy

Goal state after:
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
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
⊢ r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest

Tactic:
rxy

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
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 (α ::: (Cofix F α ⊕ β))
x : β
⊢ (corec' g x).dest = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
by
  rw [Cofix.corec', Cofix.dest_corec]; dsimp
  congr!; ext (i | i) <;> erw [corec_roll] <;> dsimp [Cofix.corec']
  · mv_bisim i with R a b x Ha Hb
    rw [Ha, Hb, Cofix.dest_corec]
    dsimp [Function.comp_def]
    repeat rw [MvFunctor.map_map, ← appendFun_comp_id]
    apply liftR_map_last'
    dsimp [Function.comp_def]
    intros
    exact ⟨_, rfl, rfl⟩
  · congr 1 with y
    erw [appendFun_id_id]
    simp [MvFunctor.id_map, Sum.elim]

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

Goal state before:
pp: α : 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

Tactic:
simp at this; simp_all

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

Goal state before:
pp: α : 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

Tactic:
simp at this; simp_all

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

Goal state before:
pp: α : 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:
simp at this; simp_all

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

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

Tactic:
obtain ⟨_⟩ := nonempty_fintype α

Goal state after:
case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
obtain ⟨_⟩ := nonempty_fintype α

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
obtain ⟨_⟩ := nonempty_fintype α

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m : ℕ
v : Vector3 α (m + 1)
x✝¹ : ℕ
x✝ : Vector3 α x✝¹
a : α
_t : Vector3 α m
⊢ ((a :: _t) +-+ x✝) (left x✝¹ fz) = (a :: _t) fz

Tactic:
by simp [*, left]

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

Goal state before:
pp: case bc
f g : CircleDeg1Lift
⊢ ↑⌈g 0⌉ < g 0 + 1

Tactic:
exact ceil_lt_add_one _

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

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

Tactic:
simp [translationNumber_pow f n]

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

Goal state before:
pp: case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ (∃ x, f x = x + ↑m) → τ f = ↑m

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
x : ℝ
hx : f x = x + ↑m
⊢ τ f = ↑m
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
⊢ EventuallyConst s (ae μ)

Tactic:
by
  borelize M
  refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_
  rwa [dense_iff_closure_eq, IsClosed.closure_eq, eq_univ_iff_forall] at hd
  let f : C(M × X, X) := ⟨(· • ·).uncurry, continuous_smul⟩
  exact isClosed_setOfPred_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm
    (measure_ne_top _ _)

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

Goal state after:
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
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
⊢ (DenseRange fun x ↦ x • a) ↔ addOrderOf a = 0

Tactic:
by
  rcases QuotientAddGroup.mk_surjective a with ⟨a, rfl⟩
  simp [denseRange_zsmul_coe_iff, isOfFinAddOrder_iff_exists_rat_eq_div, Irrational]

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

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

pp: case refine_3
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : ↥G), QuasiMeasurePreserving (fun x ↦ g +ᵥ x) volume volume

pp: case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
· -- `∀ (g : G), g ≠ 0 → AEDisjoint volume (g +ᵥ I) I`
    rintro ⟨g, hg⟩ hg'
    replace hg' : g ≠ 0 := by simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'
    change AEDisjoint volume (g +ᵥ I) I
    refine AEDisjoint.congr (Disjoint.aedisjoint ?_)
      ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI
    have hBg : g +ᵥ B = ball (g + x) (T / (2 * n)) := by
      rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
    rw [hBg]
    apply ball_disjoint_ball
    rw [dist_eq_norm, add_sub_cancel_right, div_mul_eq_div_div, ← add_div, ← add_div,
      add_self_div_two, div_le_iff₀' (by positivity : 0 < (n : ℝ)), ← nsmul_eq_mul]
    refine (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans
      (nsmul_le_nsmul_left (norm_nonneg g) ?_)
    exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)

Goal state after:
case refine_3
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : ↥G), QuasiMeasurePreserving (fun x ↦ g +ᵥ x) volume volume

case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))

Tactic:
use hfμ.measurable

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
⊢ map f (ν.withDensity (μ.rnDeriv ν)) = ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
ENNReal.toReal_eq_toReal_iff,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = (ν.withDensity (μ.rnDeriv ν)) s ∨
    ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
ENNReal.toReal_eq_toReal_iff,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = (ν.withDensity (μ.rnDeriv ν)) s ∨
    ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf (MapsTo.restrict S G G hG) (val ⁻¹' F)

Tactic:
apply (coverEntropyInf_image_le_of_uniformContinuous hφ
    (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (G.domRestrict φ '' val ⁻¹' F) = coverEntropyInf T (φ '' F)