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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
    ls + rs

Tactic:
rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).size = ls + (rl.size + rr.size + 1)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
i : Fin2 n
u : α i
⊢ u ∈ supp x i → u ∈ supp x i

Tactic:
exact id

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

Goal state before:
pp: case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
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 : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
x y z : (P F).W α
_e₁ : WEquiv x y
⊢ WEquiv y z → recF u x = recF u y → recF u y = recF u z → recF u x = recF u z

Tactic:
_e₂

Goal state after:
case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
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 : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
x y z : (P F).W α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
⊢ recF u x = recF u y → recF u y = recF u z → recF u x = recF u z
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
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✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
h₁ : ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
a✝ : Cofix F
c : (P F).M
b✝ : Cofix F
d : (P F).M
rcd : r (Quot.mk Mcongr c) (Quot.mk Mcongr d)
⊢ Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr d)

Tactic:
exact Quot.sound rcd

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
u : α
⊢ u ∈ supp x → u ∈ supp x

Tactic:
exact id

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)) → ∀ u ∈ supp (abs ⟨a, f⟩), p u

Tactic:
rintro ⟨a', f', abseq, hf⟩ u
    rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
    rintro ⟨i, _, hi⟩
    rw [← hi]
    apply hf

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

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

Tactic:
exact id

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

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hab : ⟨j✝, a⟩ < ⟨i✝, b⟩
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab

Goal state after:
case refine_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hij : j✝ < i✝
⊢ False

case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hji : i✝ < i✝
hab : a < b
⊢ False
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : ⟨i✝, a⟩ < ⟨i✝, b⟩
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab

Goal state after:
case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hij : i✝ < i✝
⊢ False

case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : a < b
⊢ False
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } =
    ltb s₁.next s₂.next

Tactic:
ltb,

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    ltb s₁.next s₂.next
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } =
    decide (s₁.curr < s₂.curr)

Tactic:
ltb,

Goal state after:
case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    decide (s₁.curr < s₂.curr)
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } = true

Tactic:
ltb,

Goal state after:
case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case4
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } = false

Tactic:
ltb,

Goal state after:
case case4
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
      else true
    else false) =
    false
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
⊢ a' ∈ parallel S

Tactic:
have aa := parallel_promises h2 h
    rw [← aa]
    rw [← aa] at h
    exact
      let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_right H sS
      let aT := (st _).2 as
      mem_parallel h1 tT aT

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
or_iff_right

Goal state after:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).1 (f₂ x y s₂).1
right✝ : (f₁ x y s₁).2 = (f₂ x y s₂).2
⊢ R (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).1 (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).1 ∧
    (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).2 = (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2

Tactic:
simp only [mapAccumr₂_snoc, ih hR, true_and]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).1 (f₂ x y s₂).1
right✝ : (f₁ x y s₁).2 = (f₂ x y s₂).2
⊢ (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₁ x y s₁).2 = (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₂ x y s₂).2
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ (mapAccumr f xs s).2 = map f' xs

Tactic:
rw [mapAccumr_eq_map Set.univ (Set.mem_univ _) (fun _ _ _ => Set.mem_univ _)
    (fun a s s' _ _ => by rw [h, h])]
  simp_all

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x

Tactic:
simpa only [not_le] using not_congr (f.iterate_pos_le_iff hn)

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

Goal state before:
pp: case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + ↑m

Tactic:
simp only [← h]

Goal state after:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + τ f
Module: Mathlib.Dynamics.Ergodic.Extreme

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

Tactic:
by
  have hf : MeasurePreserving f μ μ := h.1.1
  rcases eq_or_ne c 0 with rfl | hc₀
  · convert! zero_measure hf.measurable
    rw [← measure_univ_eq_zero, h.1.2]
  · refine ⟨hf, ⟨?_⟩⟩
    have : IsFiniteMeasure μ := by
      constructor
      rwa [h.1.2, lt_top_iff_ne_top]
    set S := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
    have {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s) (hμs : μ s ≠ 0) :
        c • μ[|s] ∈ S := by
      refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
      · convert! hf.restrict_preimage hsm
        exact hfs.symm
      · rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
    intro s hsm hfs
    by_contra H
    obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by
      simpa [eventuallyConst_set, ae_iff, and_comm] using! H
    have hcond : c • μ[|s] = μ := by
      apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
      refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
      · rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
      · simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel,
          ENNReal.mul_inv_cancel, *]
    rw [← hcond] at hs'
    simp [ProbabilityTheory.cond_apply, hsm] at hs'

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
| ∫⁻ (a : α) in s, f a ∂μ

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

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
| ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
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
| μ s

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

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
| (ν.withDensity (μ.rnDeriv ν)) s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x
hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν).rnDeriv (ν + ν') x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x =
    (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x

Tactic:
rw [hx₃, hx₄, hx₅]

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

Goal state before:
pp: 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 : ℕ
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨t, t_cover, t_card⟩ := (coverMincard_finite_iff T (φ '' F) V n).1 h'
  obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h
  rw [← t_card]
  exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

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 := ⋯
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ 𝓤 X

Tactic:
uniformity_comap φ,

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
⊢ Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ Filter.comap (Prod.map φ φ) (𝓤 Y)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h | h

Goal state after:
case inl
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n
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 S F ≤ coverEntropy T (φ '' F)

Tactic:
refine iSup₂_le fun U U_uni ↦ ?_
    simp only [uniformity_comap φ, mem_comap] at U_uni
    obtain ⟨V, V_uni, V_sub⟩ := U_uni
    obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
    apply (coverEntropyEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
    apply (le_coverEntropyEntourage_image h F).trans
    exact coverEntropyEntourage_le_coverEntropy T (φ '' F) W_uni

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ μ t ≠ ∞

Tactic:
ht,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ μ (toMeasurable μ s) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x

Tactic:
rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C (i 1) = 1

Tactic:
i.map_one,

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C 1 = 1