mathlib-initiative/mathlib-tactics huggingface dataset:
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 (Ordnode.node rs rl rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1

Tactic:
rw [this] at H ⊢

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
⊢ Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax ↑(findMax' x (rl.node' rx rr)) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i ↦ g <$$> f i

Tactic:
change _ = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
  have : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩ := by
    ext i : 1
    dsimp [Function.comp_def]
    cases f i
    rfl
  rw [this]
  have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
    ext1 x
    cases f x
    rfl
  rw [this]
  dsimp
  rw [wMk_eq, wMk_eq]
  have h := MvPFunctor.map_eq P.wp g
  rw [h, comp_wPathCasesOn]

Goal state after:
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 (Ordnode.node rs rl rx rr)) o₂
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1

Tactic:
have := H.2.2.2.eq_node'; rw [this] at H ⊢
    rcases IHrr H.right with ⟨h, e⟩
    refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
    rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
    rw [size_node, e]; rfl

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

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩

Goal state after:
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p

Tactic:
intro q h

Goal state after:
case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
constructor
  · rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use a, fun i j => (f i j).val
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]; rfl
    intro i j
    apply (f i j).property
  rintro ⟨a, f, h₀, h₁⟩
  use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
  rw [← abs_map, h₀]; rfl

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

Goal state before:
pp: case node.node.hnc
α : 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
⊢ ¬ls + rs ≤ 1

Tactic:
· exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
conv =>
      rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ abs ⟨a, (TypeVec.id ::: fixToW) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: wrepr) ⊚ (P F).appendContents f' f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refl
α : Type u_1
inst✝ : Preorder α
⊢ (↑∅).empty = true

Tactic:
exact rfl

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

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ⟨a, g₁ ∘ fun x ↦ ⟦f x⟧⟩ = abs ⟨a, g₂ ∘ fun x ↦ ⟦f x⟧⟩

Tactic:
congr 2 with x

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
x : (P F).B a
⊢ (g₁ ∘ fun x ↦ ⟦f x⟧) x = (g₂ ∘ fun x ↦ ⟦f x⟧) x
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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x

Tactic:
apply Quot.ind
  intro x
  induction x using q.P.wInd
  case ih a f' f ih =>
    change g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧
    rw [← Fix.ind_aux a f' f]
    apply h
    rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
    congr 2
    rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
    have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
      ext x
      exact ih x
    rw [this]

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 := fun x y ↦ abs y.repr = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest

Tactic:
rintro x y h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
x y : Cofix F α
h : R x y
⊢ LiftR' (α.RelLast' R) x.dest y.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' g) (Sum.inl i)

Tactic:
dsimp [Cofix.corec']

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl i) =
    i
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) val) fun val ↦ g val)
      (Sum.inr i) =
    Sum.elim _root_.id (corec' g) (Sum.inr i)

Tactic:
dsimp [Cofix.corec']

Goal state after:
case inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inr i) =
    corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i)
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:
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.WSeq.Basic

Goal state before:
pp: α : Type u
l : List α
s : WSeq α
⊢ Computation.corec
      (fun x ↦
        match x with
        | (l, s) =>
          match Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s) =
    (fun x ↦ l.reverse ++ x) <$> s.toList

Tactic:
refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l' : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨l, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a::l, s')) (l' ++ l, s) ∧
            c2 = Computation.map (l.reverse ++ ·) (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l', s)))
      ?_ ⟨[], s, rfl, rfl⟩

Goal state after:
α : Type u
l : List α
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 ↦
    ∃ l' s,
      c1 =
          Computation.corec
            (fun x ↦
              match x with
              | (l, s) =>
                match Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l' ++ l, s) ∧
        c2 =
          Computation.map (fun x ↦ l.reverse ++ x)
            (Computation.corec
              (fun x ↦
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l', s))
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ map (g ∘ f) s = map g (map f s)

Tactic:
dsimp [map]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)
Module: Mathlib.Data.Sum.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
⊢ ∀ (x y z : α ⊕ₗ β), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
simp only [Lex.forall, Sum.forall, inr_le_inr_iff,
      le_sup_left, inl_le_inr, sup_of_le_right, and_self,
      inf_of_le_left, implies_true, inf_of_le_right, sup_of_le_left, ← inl_sup,
      ← inr_sup, ← inl_inf, ← inr_inf, sup_inf_left, le_rfl]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
S : WSeq (Computation α)
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) tail✝) =
    match
      match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) tail✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b
⊢ List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) (head✝ :: tail✝)) =
    match
      match
        List.foldr
          (fun c o ↦
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) (head✝ :: tail✝) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b

Tactic:
| cons =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot

Tactic:
try with_reducible_and_instances rfl -- fails
  try rfl -- fails
  exact Subsingleton.elim _ _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' g ⁻¹' s = g ⁻¹' s

Tactic:
← preimage_comp,

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ g ∘ f ⁻¹' s = g ⁻¹' s
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f' ∘ g ⁻¹' s = g ⁻¹' s

Tactic:
preimage_comp,

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ g ⁻¹' f' ⁻¹' s = g ⁻¹' s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x ↦ ((f ^ 2 ^ x) 0 + (g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))

Tactic:
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
    (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_

Goal state after:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (((f * g) ^ n) 0) ((f ^ n) 0 + (g ^ n) 0) ≤ 1
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
⊢ ε / 2 ≠ 0

Tactic:
simp [hε.ne']

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

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m

Tactic:
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]

Goal state after:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, (f ^ n) x = x + ↑m
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ (DenseRange fun x ↦ x • ↑a) ↔ Irrational (a / p)

Tactic:
← dense_addSubgroupClosure_pair_iff,

Goal state after:
a p : ℝ
⊢ (DenseRange fun x ↦ x • ↑a) ↔ Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ f ⁻¹' g ⁻¹' U ↔ x ∈ g ⁻¹' U

Tactic:
← preimage_comp,

Goal state after:
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ g ∘ f ⁻¹' U ↔ x ∈ g ⁻¹' U
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' g ⁻¹' U = g ⁻¹' U

Tactic:
← preimage_comp,

Goal state after:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ g ∘ f ⁻¹' U = g ⁻¹' U
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ∀ s ∈ Iio '' t, y ∈ s ↔ x ∈ s

Tactic:
simpa only [iff_comm] using h

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 k : ℕ
x✝ : k < n
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U

Tactic:
← preimage_comp,

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 k : ℕ
x✝ : k < n
⊢ (map T T)^[k] ∘ map φ φ ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
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 k : ℕ
x✝ : k < n
⊢ (map T T)^[k] ∘ map φ φ ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U

Tactic:
← preimage_comp,

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 k : ℕ
x✝ : k < n
⊢ (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ (map S S)^[k] ⁻¹' U
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s

Tactic:
by
  rw [setIntegral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν]

Goal state after: