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

Goal state before:
pp: case node.node.refine_1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩

Goal state after:
case node.node.refine_1.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

case node.node.refine_1.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a

Tactic:
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)

Tactic:
simp only [liftp_iff]; constructor <;> intro h
  · rcases h with ⟨a', f', heq, h'⟩
    cases heq
    assumption
  repeat' first | constructor | assumption

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (x n.succ) = head' (x m.succ)

Tactic:
by
  suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
  intro n
  induction n with
  | zero => grind
  | succ n n_ih => grind +splitIndPred [Hconsistent (succ n), head']

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
⊢ m ∣ n ↔ n % m = 0

Tactic:
by
  rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]; rfl

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized

Tactic:
exact hr.dual.rotateL hl.dual

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ (r.dual.rotateL x l.dual).size = l.size + r.size + 1

Tactic:
hl.dual.rotateL_size,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ r.dual.size + l.dual.size + 1 = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1

Tactic:
eraseMax,

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.balanceL x (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMax).size + 1
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
⊢ (↑n).primeFactorsList.prod = ↑n

Tactic:
exact Nat.prod_primeFactorsList n.ne_zero

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

Goal state before:
pp: m n : ℕ+
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset

Tactic:
by
  apply le_antisymm
  · apply le_inf_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
    · exact gcd_dvd_left m n
    · exact gcd_dvd_right m n
  · rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
    apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']
    · exact inf_le_left
    · exact inf_le_right

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

Goal state before:
pp: case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
hr : nil.Balanced
sr : nil.Sized
⊢ (node ls ll lx lr).balance x nil = (node ls ll lx lr).balance' x nil

Tactic:
sl.eq_node'

Goal state after:
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (ll.node' lx lr).Balanced
sl : (node ls ll lx lr).Sized
hr : nil.Balanced
sr : nil.Sized
⊢ (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
exact Lex.left _ _ ha

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
exact Lex.left _ _ ha

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 : (i : ι) → α i
⊢ #(Icc a b) - 1 = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
card_Icc

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ ∏ i, #(Icc (a i) (b i)) - 1 = ∏ i, #(Icc (a i) (b i)) - 1
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 : (i : ι) → α i
⊢ #(Icc a b) - 2 = ∏ i, #(Icc (a i) (b i)) - 2

Tactic:
card_Icc

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ ∏ i, #(Icc (a i) (b i)) - 2 = ∏ i, #(Icc (a i) (b i)) - 2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
H1 : l.size = 0 → r.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
⊢ l.balanceL x r = l.balance x r

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r
  · rfl
  · obtain - | ⟨ls, ll, lx, lr⟩ := l
    · have : size rl = 0 ∧ size rr = 0 := by
        have := H1 rfl
        rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
      cases sr.2.1.size_eq_zero.1 this.1
      cases sr.2.2.size_eq_zero.1 this.2
      rw [sr.eq_node']; rfl
    · replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
      simp [balanceL, balance, H2]; split_ifs <;> simp [add_comm]

Goal state after:
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
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 (f₁ x) (f₀ x)
⊢ WEquiv ((P F).wMk a f' f₁) ((P F).wMk a f' f₀)

Tactic:
| ind a f' f₀ f₁ _h ih =>

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (corec g x).dest = corec g <$> g x

Tactic:
conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]
  dsimp
  rw [corecF_eq, abs_map, abs_repr, ← comp_map]; rfl

Goal state after:
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
g : α ⟹ β
x : ↑(P F).wp α
| Quot.mk WEquiv (g <$$> x) = g <$$> Quot.mk WEquiv x

Tactic:
rhs
      dsimp [MvFunctor.map]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α β : TypeVec.{u} n
g : α ⟹ β
x : ↑(P F).wp α
| Fix.map g (Quot.mk WEquiv x)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝¹ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝
s✝ u t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
obtain ⟨c, u⟩ := c

Goal state after:
case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u✝.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case h1
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (s.drop n).destruct (t.drop n).destruct

pp: case h2
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    ?R a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)

pp: case R
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Option (α × WSeq α) → Option (β × WSeq β) → Prop

Tactic:
· apply liftRel_dropn_destruct H n

Goal state after:
case h2
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) ds dt
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
rcases ds with - | a

Goal state after:
case none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none dt
⊢ Prod.fst <$> none ∈ t.head

case some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) dt
⊢ Prod.fst <$> some a ∈ t.head
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
exact Lex.left _ _ ha

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
exact Lex.left _ _ ha

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

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
· exact ⟨nil, S, by simp, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    s1.destruct s2.destruct

Tactic:
rw [h1, h2]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (s.append S.join).destruct (t.append T.join).destruct
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:
div_le_div_iff_of_pos_right this,

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist ((f ^ (n + 1)) 0) ((↑n + 1) * τ f) ≤ 1
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 : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
⊢ ∀ (i : ℤ), Disjoint (g ^ i • V) (a • V)

Tactic:
disjoint_left

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 : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
⊢ ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[>] 0)
j : ι
hj : 0 < δ j
⊢ d ∈ closedBall d (1 * δ j)

Tactic:
simp only [one_mul, mem_closedBall, dist_self]

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[>] 0)
j : ι
hj : 0 < δ j
⊢ 0 ≤ δ j
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
by
    conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsFiniteMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ}

Tactic:
by
  rw [mem_extremePoints_iff_left]
  refine ⟨⟨hμ.toMeasurePreserving, rfl⟩, ?_⟩
  rintro ν₁ ⟨hfν₁, hν₁μ⟩ ν₂ ⟨hfν₂, hν₂μ⟩ ⟨a, b, ha, hb, hab, rfl⟩
  have : IsFiniteMeasure ν₁ := ⟨by rw [hν₁μ]; apply measure_lt_top⟩
  apply hμ.eq_of_absolutelyContinuous_measure_univ_eq hfν₁ (.add_right _ _) hν₁μ
  apply absolutelyContinuous_smul ha.ne'

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (μ.rnDeriv ν) (ν.restrict s)

Tactic:
exact (Measure.measurable_rnDeriv _ _).aemeasurable

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ map φ φ ⁻¹' ⋂ k, ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
preimage_iInter₂

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ i, ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k \ n ⊆ ⋃ u ∈ f, j u

Tactic:
rw [this, sdiff_subset_comm, sdiff_iUnion]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case h
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 ↑s
⊢ IsDynCoverOf T F (U ○ U) 0 {x} ∧ 1 ≤ #s ^ n

Tactic:
exact ⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
      one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩

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

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
· obtain ⟨k, k_max⟩ := ENat.ne_top_iff_exists.mp h.ne
    rw [← k_max]
    simp only [Nat.cast_inj]
    -- The criterion we want to use is `Nat.sSup_mem`. We rewrite `netMaxcard` with an `sSup`,
    -- then check its `BddAbove` and `Nonempty` hypotheses.
    have : netMaxcard T F U n
      = sSup (WithTop.some '' Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      rw [netMaxcard, ← image_comp, sSup_image]
      simp only [mem_ofPred_eq, ENat.some_eq_natCast, Function.comp_apply]
      exact biSup_congr (fun _ _ ↦ rfl)
    rw [this] at k_max
    have h_bdda : BddAbove (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      refine ⟨k, mem_upperBounds.2 ?_⟩
      simp only [mem_image, mem_ofPred_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
      intro s h
      rw [← ENat.natCast_le_natCast, k_max]
      apply le_sSup
      exact Filter.frequently_principal.mp fun a ↦ a (by simpa using ⟨_, h, rfl⟩) rfl
    have h_nemp : (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}).Nonempty := by
      refine ⟨0, ?_⟩
      simp only [mem_image, mem_ofPred_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
      exact isDynNetIn_empty
    rw [← WithTop.coe_sSup' h_bdda] at k_max
    have key := Nat.sSup_mem h_nemp h_bdda
    rw [← Nat.cast_inj.mp k_max, mem_image] at key
    simp only [mem_ofPred_eq] at key
    exact key

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

Tactic:
exact (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after: