mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct

Tactic:
by
      simp only [destruct_flatten]; apply liftRel_bind _ _ h
      intro a b ab; apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)
      intro a b; apply LiftRelO.imp_right
      intro s t h; refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩ <;> simp [h]

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

Goal state before:
pp: case right_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
t : α
⊢ t ∈ ↑hs.toFinset →
    (fun x ↦
          match x with
          | ⟨t, x⟩ => x)
        ((fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩) t) =
      t

Tactic:
simp only [implies_true]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a ≤ c ∧ c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
exists_and_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k), ⋯ ▸ a ≤ c ∧ ∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a ≤ c ∧ c < ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
exists_and_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k), ⋯ ▸ a ≤ c ∧ ∃ (x : j = k), c < ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a ≤ c) ∧ ∃ (h : k = j), ⋯ ▸ c < b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a < c ∧ c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
exists_and_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k), ⋯ ▸ a < c ∧ ∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c ≤ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k) (h_1 : j = k), ⋯ ▸ a < c ∧ c < ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
exists_and_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝² x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ (∃ (h : i = k), ⋯ ▸ a < c ∧ ∃ (x : j = k), c < ⋯ ▸ b) ↔ (∃ (h : i = k), ⋯ ▸ a < c) ∧ ∃ (h : k = j), ⋯ ▸ c < b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case nil
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append t).destruct.destruct (nil.destruct.bind (destruct_append.aux t)).destruct

pp: case cons
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x✝ : α
s✝ : WSeq α
h : c1 = ((cons x✝ s✝).append t).destruct ∧ c2 = (cons x✝ s✝).destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x✝ s✝).append t).destruct.destruct ((cons x✝ s✝).destruct.bind (destruct_append.aux t)).destruct

pp: case think
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s✝ : WSeq α
h : c1 = (s✝.think.append t).destruct ∧ c2 = s✝.think.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s✝.think.append t).destruct.destruct (s✝.think.destruct.bind (destruct_append.aux t)).destruct

Tactic:
case nil =>
    induction t using WSeq.recOn
    case nil | cons => simp
    case think t => exact ⟨nil, t, by simp⟩

Goal state after:
case cons
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x✝ : α
s✝ : WSeq α
h : c1 = ((cons x✝ s✝).append t).destruct ∧ c2 = (cons x✝ s✝).destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x✝ s✝).append t).destruct.destruct ((cons x✝ s✝).destruct.bind (destruct_append.aux t)).destruct

case think
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s✝ : WSeq α
h : c1 = (s✝.think.append t).destruct ∧ c2 = s✝.think.destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s✝.think.append t).destruct.destruct (s✝.think.destruct.bind (destruct_append.aux t)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right.HU
α : 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
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ swap (LiftRel R) s t ∧ LiftRel (swap (LiftRel R)) S T) →
      ∃ s t S T, s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T

Tactic:
← LiftRel.swap (LiftRel R)

Goal state after:
case right.HU
α : 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
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ swap (LiftRel R) s t ∧ swap (LiftRel (LiftRel R)) S T) →
      ∃ s t S T, s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = s.append (S.append SS.join).join
h2 : s2 = s.append (S.join.append (map join SS).join)
⊢ s1.destruct = (s.append (S.append SS.join).join).destruct

Tactic:
simp [h1]

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

Goal state before:
pp: case nil.nil.cons
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩

Goal state after:
case nil.nil.cons.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (cons S SS).join.join.destruct.tail = (nil.append (S.append SS.join).join).destruct

case nil.nil.cons.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (map join (cons S SS)).join.destruct.tail = (nil.append (S.join.append (map join SS).join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.think
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (nil.append (S.think.append SS.join).join).destruct.destruct
    (nil.append (S.think.join.append (map join SS).join)).destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩

Goal state after:
case nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.append SS.join).join).destruct.tail = (nil.append (S.append SS.join).join).destruct

case nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append (map join SS).join)).destruct.tail =
    (nil.append (S.join.append (map join SS).join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ (snoc ⟨val✝, property✝⟩ x).reverse = x ::ᵥ reverse ⟨val✝, property✝⟩

Tactic:
simp only [reverse, snoc, cons, toList_mk]

Goal state after:
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨(⟨val✝, property✝⟩ ++ ⟨[x], ⋯⟩).toList.reverse, ⋯⟩ = ⟨x :: val✝.reverse, ⋯⟩
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_4.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inl val✝¹ = inl a₁ → inr val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝¹) (inr val✝) = ∅

Tactic:
simp [h.2.1 _ _ rfl rfl]

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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
      (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty

Tactic:
by
  simp only [nonempty_iff_ne_empty, Ne, sumLexLift_eq_empty, not_and_or, exists_prop, not_forall]

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n

Tactic:
rw [div_div, ← pow_succ', ← abs_of_pos this]

Goal state after:
f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |2 ^ (n + 1)|
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
hs : NullMeasurableSet s volume
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[volume] s
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
⊢ s =ᵐ[volume] ∅ ∨ s =ᵐ[volume] univ

Tactic:
set μ := (volume : Measure <| AddCircle T)
  set n : ι → ℕ := addOrderOf ∘ u
  have hT₀ : 0 < T := hT.out
  have hT₁ : ENNReal.ofReal T ≠ 0 := by simpa
  rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]
  rcases eq_or_ne (μ s) 0 with h | h; · exact Or.inl h
  right
  obtain ⟨d, -, hd⟩ : ∃ d, d ∈ s ∧ ∀ {ι'} {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) :=
    exists_mem_of_measure_ne_zero_of_ae h
      (IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div μ s 1)
  let I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
  replace hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1) := by
    let δ : ι → ℝ := fun j => T / (2 * ↑(n j))
    have hδ₀ : ∀ᶠ j in l, 0 < δ j :=
      (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
    have hδ₁ : Tendsto δ l (𝓝[>] 0) := by
      refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩
      replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
        (tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
      convert! hu₂.inv_tendsto_atTop
      ext j
      simp only [δ, Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]
    have hw : ∀ᶠ j in l, d ∈ closedBall d (1 * δ j) := hδ₀.mono fun j hj => by
      simp only [one_mul, mem_closedBall, dist_self]
      apply hj.le
    exact hd _ δ hδ₁ hw
  suffices ∀ᶠ j in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T by
    replace hd := hd.congr' this
    rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
  refine (hu₂.eventually_gt_atTop 0).mono fun j hj => ?_
  have : addOrderOf (u j) = n j := rfl
  have huj : IsOfFinAddOrder (u j) := addOrderOf_pos_iff.mp hj
  have huj' : 1 ≤ (↑(n j) : ℝ) := by norm_cast
  have hI₀ : μ (I j) ≠ 0 := (measure_closedBall_pos _ d <| by positivity).ne.symm
  have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _
  have hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T := by
    rw [volume_closedBall, mul_div, mul_div_mul_left T _ two_ne_zero,
      min_eq_right (div_le_self hT₀.le huj'), mul_comm, ← nsmul_eq_mul, ← ENNReal.ofReal_nsmul,
      nsmul_eq_mul, mul_div_cancel₀]
    exact Nat.cast_ne_zero.mpr hj.ne'
  rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ae_all_iff.2 fun k => ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
⊢ ∃ i, ∃ (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U

Tactic:
use k, lt_of_lt_of_le k_m m_n

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ coverEntropyEntourage T ∅ U = ⊥

Tactic:
by
  simp only [coverEntropyEntourage, coverMincard_empty]
  rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]

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

Goal state before:
pp: X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s

Tactic:
rcases (hasBasis_symmetric.mem_iff' V).1 V_uni with ⟨W, ⟨W_uni, W_symm⟩, W_V⟩

Goal state after:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
by
  rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 h'
  exact s_coverMincard ▸ (s_cover.closure h V_uni).coverMincard_le_card

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
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 : eval₂ i b (X ^ n - C a) = 0
⊢ (map i (X ^ n - 1)).Splits

Tactic:
eval₂_sub,

Goal state after:
case neg
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 : eval₂ i b (X ^ n) - eval₂ i b (C a) = 0
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ (L.lhomWithConstants α).comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]

Tactic:
simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]
    exact _root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r (f.symm.toFun ∘ x) ↔ RelMap r x

Tactic:
simp only [Equiv.toFun_as_coe]
      refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_
      rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 2 → R), funMap addFunc x = x 0 + x 1

Tactic:
by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 2 → R), funMap mulFunc x = x 0 * x 1

Tactic:
by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (x : Fin 1 → R), funMap negFunc x = -x 0

Tactic:
by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L[[γ]].Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
obtain - | f := f

Goal state after:
case func.succ.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions (n✝ + 1)
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + 1 + n' ≤ x✝ + n' + 1

Tactic:
add_assoc,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + (1 + n') ≤ x✝ + n' + 1