mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

pp: case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
· rw [Num.cast_bit0, two_mul]
    refine ⟨h₁, lt_of_not_ge fun h => ?_⟩
    obtain ⟨r₂, e'⟩ := Nat.le.dest h
    rw [← Num.to_of_nat r₂, add_comm] at e'
    cases e.symm.trans (this.2 e'.symm)

Goal state after:
case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
⊢ Agree ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n) ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n.succ)

Tactic:
have P' := x.2 (succ n)

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
P' : Agree (x.approx n.succ) (x.approx n.succ.succ)
⊢ Agree ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n) ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n.succ)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hm : Valid' (↑x) m ↑y
hr : Valid' (↑y) r o₂
Hm : 0 < m.size
H :
  l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ m.size ∧
        delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x m y r) o₂

Tactic:
by
  obtain - | ⟨s, ml, z, mr⟩ := m; · cases Hm
  suffices
    BalancedSz (size l) (size ml) ∧
      BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1) from
    Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
  rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
  · rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1
    rw [l0, m1.1, m1.2]; revert r0; rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]
  · rcases Nat.eq_zero_or_pos (size r) with r0 | r0
    · rw [r0] at mr₂; cases not_le_of_gt Hm mr₂
    rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
    by_cases mm : size ml + size mr ≤ 1
    · dsimp [delta, ratio] at lr₁ mr₁
      have r1 : r.size = 1 := by lia
      have l1 : l.size = 1 := by lia
      rw [r1, add_assoc] at lr₁
      rw [l1, r1]
      revert mm; cases size ml <;> cases size mr <;> intro mm
      · decide
      · rw [zero_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
        decide
      · rcases mm with (_ | ⟨⟨⟩⟩); decide
      · rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
    rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩
    rcases Nat.eq_zero_or_pos (size ml) with ml0 | ml0
    · rw [ml0, mul_zero, Nat.le_zero] at mm₂
      rw [ml0, mm₂] at mm; cases mm (by decide)
    have : 2 * size l ≤ size ml + size mr + 1 := by
      have := Nat.mul_le_mul_left ratio lr₁
      rw [mul_left_comm, mul_add] at this
      have := le_trans this (add_le_add_right mr₁ _)
      rw [← Nat.succ_mul] at this
      exact (mul_le_mul_iff_right₀ (by decide)).1 this
    refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
    · refine (mul_le_mul_iff_right₀ (by decide)).1 (le_trans this ?_)
      rw [two_mul, Nat.succ_le_iff]
      refine add_lt_add_of_lt_of_le ?_ mm₂
      simpa using! mul_lt_mul_of_pos_right (by decide : 1 < 3) ml0
    · exact Nat.le_of_lt_succ (Valid'.node4L_lemma₁ lr₂ mr₂ mm₁)
    · exact Valid'.node4L_lemma₂ mr₂
    · exact Valid'.node4L_lemma₃ mr₁ mm₁
    · exact Valid'.node4L_lemma₄ lr₁ mr₂ mm₁
    · exact Valid'.node4L_lemma₅ lr₂ mr₁ mm₂

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
⊢ (l.balance' x r).size = l.size + r.size + 1

Tactic:
unfold balance'; split_ifs
  · rfl
  · exact hr.rotateL_size
  · exact hl.rotateR_size
  · rfl

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
cases m <;> simp [node4L, all_node', All, all_node3L, and_assoc]

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

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset.prod = v.prod

Tactic:
to_ofPNatMultiset

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ v.prod = v.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (coePNatMonoidHom (u + v)).prod = u.prod * v.prod

Tactic:
rw [coePNatMonoidHom.map_add]

Goal state after:
u v : PrimeMultiset
⊢ (coePNatMonoidHom u + coePNatMonoidHom v).prod = u.prod * v.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n

Tactic:
← PrimeMultiset.prod_add,

Goal state after:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ (m.factorMultiset.prod.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y

Tactic:
rw [← h]

Goal state after:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
this : LiftP (fun i u ↦ u ∈ f i '' univ) x
⊢ u ∈ f i '' univ

Tactic:
exact h this

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂

Tactic:
OrderDual.Preorder.dual_dual

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case sz
α : 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
⊢ (Ordnode.node size✝ (map f l✝) (f x✝) (map f r✝)).Sized

Tactic:
constructor
      · rw [t_l_size, t_r_size]; exact h.sz.1
      · constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz

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

Goal state before:
pp: case h
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 : Cofix F α
r'xy : r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
cases r'xy with

Goal state after:
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 → LiftR (α.RelLast r) x.dest y.dest

Tactic:
by intros; rw [← LiftR_RelLast_iff]; apply h; assumption

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

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

pp: case inr.inl
⊢ (↑0).sign = ↑(Int.sign 0)

pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑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:
case inr.inl
⊢ (↑0).sign = ↑(Int.sign 0)

case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : (P F).B a → α
haf : abs ⟨a, f⟩ = x
this : Liftp (fun u ↦ u ∈ f '' univ) x
⊢ u ∈ f '' univ

Tactic:
exact h this

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct

Tactic:
rw [← h]

Goal state after:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s))) s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 ↦ x1 = x2) s.destruct t.destruct

Tactic:
rw [← h]

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 ↦ x1 = x2) s.destruct s.destruct
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : (i : ι) × α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨_, _⟩ ⟨_, _, b, h⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) s.head) = Computation.pure s.head

Tactic:
cases Seq.head s

Goal state after:
case none
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) none) = Computation.pure none

case some
α : Type u
s : Seq α
val✝ : α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) (some val✝)) = Computation.pure (some val✝)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case nil
α : Type u
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑Seq.nil.tail)) Seq.nil.head) = ↑Seq.nil.tail

Tactic:
simp only [ofSeq, Seq.tail_nil, Seq.head_nil,
    Option.map_none, Seq.tail_cons, Seq.head_cons, Option.map_some]

Goal state after:
case nil
α : Type u
⊢ nil = some <$> Seq.nil
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑(Seq.cons x✝ s✝).tail)) (Seq.cons x✝ s✝).head) =
    ↑(Seq.cons x✝ s✝).tail

Tactic:
simp only [ofSeq, Seq.tail_nil, Seq.head_nil,
    Option.map_none, Seq.tail_cons, Seq.head_cons, Option.map_some]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩

Tactic:
by
    obtain rfl | hij := eq_or_ne i j
    · simp
    · simp [hij, lt_def]

Goal state after:
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:
rw [h]; exact x

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

Goal state before:
pp: α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct s.destruct

Tactic:
rw [← h]

Goal state after:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) (map ret s).join.destruct s.destruct
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
by
  cases finite_or_infinite α
  · obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact card_sym_eq_multichoose _ _
  cases k <;> simp

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

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T

Tactic:
← aa

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T

Tactic:
← aa

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S

Tactic:
← aa

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S

Tactic:
← aa

Goal state after:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i h, v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a
i : ℕ
hi : i < n
h : v.toList.get (Fin.cast ⋯ ⟨i, hi⟩) = a
⊢ i < v.toList.length

Tactic:
rwa [toList_length]

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

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᵐ[μ] ∅
⊢ g ∈ aestabilizer G μ s

Tactic:
simp [aestabilizer_congr h]

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

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᵐ[μ] univ
⊢ g ∈ aestabilizer G μ s

Tactic:
simp [aestabilizer_congr h]

Goal state after:
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))
j : ι
hj : 0 < n j
⊢ 0 < 2 * ↑(n j)

Tactic:
positivity

Goal state after:
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
⊢ 0 < T⁻¹ * 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mp.refine_1
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (fun x ↦ x • (b / ↑r.den)) r.num = a

pp: case inr.mp.refine_2
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (fun x ↦ x • (b / ↑r.den)) ↑r.den = b

Tactic:
· simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]

Goal state after:
case inr.mp.refine_2
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (fun x ↦ x • (b / ↑r.den)) ↑r.den = b
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
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
⊢ 0 < T / (2 * ↑(n j))

Tactic:
positivity

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ Dense ↑s → ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

Tactic:
rintro hd a ha rfl
    rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd
    exact ha hd

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

Goal state before:
pp: 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))
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℕ
hn : 1 < n
⊢ 1 < |↑n|

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → X
inst✝ : R1Space X
⊢ HasCompactFixedSupport f ↔ ∃ K, IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
by
  rw [HasCompactFixedSupport_iff']
  refine ⟨fun ⟨K, hK₁, hK₂, hf⟩ ↦ ⟨K, hK₂, hf⟩, fun ⟨K, hK, hf⟩ ↦ ?_⟩
  exact ⟨closure K, isClosed_closure, hK.closure, hf.trans subset_closure⟩

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ dynEntourage T U n = ⋂ k, (map T T)^[↑k] ⁻¹' U

Tactic:
simp [dynEntourage]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
x y : X
⊢ (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Tactic:
simp [dynEntourage]

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

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
z : X
hz1 : ∀ i < n, (T^[i] xy.1, T^[i] z) ∈ U
hz2 : ∀ i < n, (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ b, ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
exact mem_ball_comp (hz1 k k_n) (hz2 k k_n)

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 0 = univ

Tactic:
simp [dynEntourage]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ dynEntourage T U 1 = U

Tactic:
simp [dynEntourage]

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

Goal state before:
pp: X : Type u_1
T : X → X
n : ℕ
⊢ dynEntourage T univ n = univ

Tactic:
simp [dynEntourage]

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

Goal state before:
pp: case inr.inr.refine_2
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := ⋯
⊢ Fintype.card (Fin n → ↥s) ≤ #s ^ n

Tactic:
simp only [Fintype.card_fun, Fintype.card_coe, Fintype.card_fin, le_refl]

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ ↑t.card

Tactic:
exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

Goal state after: