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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual

Tactic:
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl

Goal state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
apply sup_le_iff.mpr

Goal state after:
case a
m n : ℕ+
⊢ m.factorMultiset ≤ (m.lcm n).factorMultiset ∧ n.factorMultiset ≤ (m.lcm n).factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ls
⊢ delta ≤ ll.size + lr.size

Tactic:
sl.1,

Goal state after:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ll.size + lr.size + 1
⊢ delta ≤ ll.size + lr.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r'

Tactic:
show IsPrecongr r'

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r'
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 a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp (abs ⟨a, f⟩) i = supp ⟨a', f'⟩ i

Tactic:
h',

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' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp (abs ⟨a', f'⟩) i = supp ⟨a', f'⟩ i
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
simp only [LiftPPreservation] at h

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : ↑(P F) α), LiftP p (abs x) ↔ LiftP p x
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

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

Tactic:
q.P.w_map_wMk

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

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

Tactic:
q.P.w_map_wMk

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(P F).wp α), Quot.mk WEquiv (f <$$> p) = f <$$> Quot.mk WEquiv p

Tactic:
intro α β g x
    conv =>
      rhs
      dsimp [MvFunctor.map]
    rfl

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 : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
by
  rintro ⟨x⟩ ⟨y⟩ rxy
  apply Quot.sound
  let r' x y := r (Quot.mk _ x) (Quot.mk _ y)
  have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest a) =
        Quot.mk r <$> Quot.mk Mcongr <$> abs (PFunctor.M.dest b) :=
      h _ _ r'ab
    have h₁ : ∀ u v : q.P.M, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      simp only [r']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁) <| by
        rintro ⟨c⟩ ⟨d⟩ rcd
        exact Quot.sound rcd
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, ← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map,
      abs_map, h₀]
    rw [← PFunctor.map_map _ _ f, ← PFunctor.map_map _ _ (Quot.mk r), abs_map, abs_map, abs_map]
  exact ⟨r', this, rxy⟩

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ (-0).sign = -0

Tactic:
neg_zero,

Goal state after:
case inr.inl
⊢ sign 0 = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_neg hn]

Goal state after:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r
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 a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp (abs ⟨a, f⟩) = supp ⟨a', f'⟩

Tactic:
h',

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' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp (abs ⟨a', f'⟩) = supp ⟨a', f'⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
⊢ nil.head = Computation.pure none

Tactic:
by simp [head]

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).head = Computation.pure (some a)

Tactic:
by simp [head]

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think.head = s.head.think

Tactic:
by simp [head]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap R) s2 s1

Tactic:
refine ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO (swap R) (swap (LiftRel R))) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ (s.get? n).Terminates → (s.get? m).Terminates

Tactic:
induction h with
  | refl => exact id
  | step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
⊢ a ∈ s

Tactic:
have ⟨n, e⟩ := h

Goal state after:
α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
n : ℕ
e : (fun b ↦ some (some a) = b) ((↑s.tail).get n)
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
by
    rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩
    have := Computation.mem_unique (Computation.mem_map _ om) h
    rcases o with - | o
    · injection this
    injection this with i
    obtain ⟨a', s'⟩ := o
    dsimp at i
    rw [i] at om
    exact ⟨_, om⟩

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

Goal state before:
pp: case succ
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n✝ : ℕ
a✝ :
  ∀ (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:
case succ n IH =>
    rcases o with a | a
    · exact terminates_parallel.aux a T
    rcases h : parallel.aux2 l with a | l'
    · have C : corec parallel.aux1 (l, S) = pure a := by
        apply destruct_eq_pure
        rw [corec_eq, parallel.aux1]
        rw [h]
        simp only [rmap]
      rw [C]
      infer_instance
    · have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h])
      rw [C]
      refine @Computation.think_terminates _ _ ?_
      have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
        intro
        apply IH _ _ _ (Or.inr _) T
        rw [a, Seq.get?_tail]
      rcases e : Seq.get? S 0 with - | o
      · grind [Seq.get?_zero_eq_none, Seq.get?_nil]
      · have D : Seq.destruct S = some (o, S.tail) := by
          dsimp [Seq.destruct]
          rw [e]
          rfl
        rw [D]
        cases o <;> simp [TT]

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

Goal state before:
pp: case hi
α : 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
x : α
⊢ ⟨t, x⟩ ∈ ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset) →
    (fun x ↦
          match x with
          | ⟨t, x⟩ => x)
        ⟨t, x⟩ ∈
      ↑hs.toFinset

Tactic:
simp +contextual

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
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Tactic:
by
  classical
  have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
  have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
  suffices hs' : _ by
    rw [finsum_def, dif_pos hs']
    simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]
    rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]
    rw [← Finset.card_sigma, eq_comm]
    apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
    · rintro ⟨t, x⟩
      simp +contextual
    · intro x
      simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
      intro hx
      refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
      simp only [nonempty_subtype, Set.mem_inter_iff]
      use x, hx, (hP.2 x).exists.choose_spec.2
    · rintro ⟨t, x⟩
      simp only [Finset.mem_sigma, Set.Finite.mem_toFinset, Function.mem_support, Nat.card_ne_zero,
        Set.mem_inter_iff, Sigma.mk.inj_iff, heq_eq_eq, and_true, and_imp, Finset.mem_coe]
      simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]
      intro y hy hyt _ hxs hxt
      rw [← Subtype.coe_inj]
      exact (hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩
    · intro t
      simp only [implies_true]
  let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩
  have hf (t : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard)) :
      ↑↑t ∈ P ∧ (f t : α) ∈ (t : Set α) :=
    ⟨(↑t : P).prop, (Set.nonempty_of_ncard_ne_zero t.prop).choose_spec.2⟩
  have : Finite ↑s := hs
  apply Finite.of_injective f
  intro t t' h
  simp only [← Subtype.coe_inj]
  exact (hP.2 (f t)).unique (hf t) (h ▸ hf t')

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ (↑s).destruct.destruct = Sum.inl (Option.map (fun a ↦ (a, ↑s.tail)) s.head)

Tactic:
simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]
    rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
    rcases Seq.get? s 0 with - | a
    · rfl
    dsimp only [(· <$> ·)]
    simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
by
      simp only [destruct_join]
      exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩

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

Goal state before:
pp: case nil.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)
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ s_1 S T_1,
    (s.append T.join).destruct = (s_1.append (S.append T_1).join).destruct ∧
      (s.append T.join).destruct = (s_1.append (S.join.append T_1.join)).destruct

Tactic:
refine ⟨s, nil, T, ?_, ?_⟩

Goal state after:
case nil.nil.cons.refine_1
α : 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 : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.append T).join).destruct

case nil.nil.cons.refine_2
α : 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 : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.join.append T.join)).destruct
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (xs.snoc x) s =
    let q := f x s;
    let r := mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs
  · rfl
  · simp [*]

Goal state after:
Module: Mathlib.Data.ZMod.Factorial

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

Tactic:
intro x hx

Goal state after:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
⊢ Ergodic (fun x ↦ g • x) μ

Tactic:
by
  borelize M
  refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
  refine aeconst_of_dense_setOfPred_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)
  refine range_subset_iff.2 fun n ↦ ?_
  rw [mem_ofPred, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense ↑(MulAction.aestabilizer G μ s)
g : G
hg : g ∈ Inv.inv ⁻¹' ↑(MulAction.aestabilizer G μ s)
⊢ g ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
by
    simpa only [preimage_smul] using! hg

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 : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ addOrderOf g ≤ n

Tactic:
exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)

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
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ n.natAbs ^ j) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt hn

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

Goal state before:
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:
replace hI := hI.trans closedBall_ae_eq_ball.symm
    have : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype
    have hG_card : #(Finset.univ : Finset G) = n := by
      change _ = addOrderOf u
      rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]; rfl
    simp_rw [measure_vadd]
    rw [AddCircle.measure_univ, tsum_fintype, Finset.sum_const, measure_congr hI,
      volume_closedBall, ← ENNReal.ofReal_nsmul, mul_div, mul_div_mul_comm,
      div_self, one_mul, min_eq_right (div_le_self hT.out.le hn), hG_card,
      nsmul_eq_mul, mul_div_cancel₀ T (lt_of_lt_of_le zero_lt_one hn).ne.symm]
    exact two_ne_zero

Goal state after:
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝ : α
⊢ ϕ.toFun (-0) x✝ = x✝

Tactic:
neg_zero,

Goal state after:
τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝ : α
⊢ ϕ.toFun 0 x✝ = x✝
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
· refine ae_restrict_of_ae ?_
      filter_upwards [hf_ne_top] with x hx using hx.lt_top

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Tactic:
nonempty_subtype,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬∃ a, IsDynCoverOf T F U n ↑a
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x

Tactic:
exact hx.symm

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

Tactic:
refine iSup₂_le fun V V_uni ↦
      (coverEntropyEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyEntourage_image_le h F _).trans ?_

Goal state after:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ coverEntropyEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropy S F
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᵐ[κ] μ.rnDeriv κ

Tactic:
rw [Measure.withDensity_rnDeriv_eq _ _ hμν]

Goal state after: