mathlib-initiative/mathlib-tactics huggingface dataset:
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:
exact x

Goal state after:
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i

Tactic:
subst h

Goal state after:
case pos
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i : ι
⊢ subtypeNeLift i (fun i_1 ↦ φ ↑i_1) (φ i) i = φ i
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
dsimp only [destruct_append.aux, Computation.LiftRel]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ (∀ {a : Option (α × WSeq α)},
      a ∈ S.join.destruct →
        ∃ b ∈ T.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b) ∧
    ∀ {b : Option (β × WSeq β)},
      b ∈ T.join.destruct →
        ∃ a ∈ S.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → WSeq β
⊢ (ret a).bind f ~ʷ f a

Tactic:
by simp [bind]

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

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

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

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

Tactic:
· rfl

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

case refine_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅
Module: Mathlib.Data.Sum.Interval

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

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

Tactic:
· rfl

Goal state after:
case refine_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (nil.snoc x) s =
    let q := f x s;
    let r := mapAccumr f nil q.1;
    (r.1, r.2.snoc q.2)

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (w✝.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x✝ ::ᵥ w✝).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
· rfl

Goal state after:
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (w✝.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x✝ ::ᵥ w✝).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.1;
    (r.1, r.2.snoc q.2)
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e✝ : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn e (i.add 0)) = Eq.recOn e ([] +-+ insert a v i)

pp: case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)

Tactic:
· rfl

Goal state after:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ insert a ((b :: t) +-+ v) (Eq.recOn x✝ (i.add (k + 1))) = Eq.recOn x✝ ((b :: t) +-+ insert a v i)
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_4.inr.inl
α₁ : 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₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝¹ = inl a₁ → inl val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inl val✝) = ∅

pp: case refine_4.inr.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₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝¹ = inl a₁ → inr val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inr val✝) = ∅

Tactic:
· rfl

Goal state after:
case refine_4.inr.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₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝¹ = inl a₁ → inr val✝ = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inr val✝) = ∅
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

Tactic:
intro h
    simp only [← h]
    exact f.exists_eq_add_translationNumber hf

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 μ
n : ℕ
H : ¬μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
this : NullMeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) μ
⊢ False

Tactic:
rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
this : NullMeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) μ
m : ℕ
hmn : m > n
hm : μ (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s})) ≠ 0
⊢ False
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y

Tactic:
have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) := by
    conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
    rw [sub_smul, one_smul, sub_add_cancel]

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case 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
hlt : x < y
hne : (Ioo x y).Nonempty
⊢ False

Tactic:
| inr hne =>

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

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
hμ : Ergodic f μ
c : ℝ≥0∞
inst✝ : IsFiniteMeasure (c • μ)
hfν : MeasurePreserving f (c • μ) (c • μ)
hνμ : c • μ ≪ μ
huniv : (c • μ) univ = μ univ
hμ₀ : μ ≠ 0
⊢ c • μ = μ

Tactic:
· simp_all [ENNReal.mul_eq_right]

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

Goal state before:
pp: X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y : X
h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
rcases h with ⟨z, z_Bx, z_By⟩

Goal state after:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inl
X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst✝ : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m ↑s
⊢ ∃ t, IsDynCoverOf T ∅ (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
exact ⟨∅, by simp⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
rcases isEmpty_or_nonempty X with _ | _
  · exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le⟩⟩
  -- If `t` is a dynamical cover of `φ '' F`, then we want to choose one preimage by `φ` for each
  -- element of `t`. This is complicated by the fact that `t` may not be a subset of `φ '' F`,
  -- and may not even be in the range of `φ`. Hence, we first modify `t` to make it a subset
  -- of `φ '' F`. This requires taking larger entourages.
  obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter
  choose! g g_rel g_mem using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)
  choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ hy
  refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
  simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
    mem_preimage, map_apply, exists_exists_and_eq_and]
  obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)
  refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩
  rw [φ_f _ (g_mem _ hy)]
  exact g_rel _ hy

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ expGrowthSup 0 = ⊥

Tactic:
expGrowthSup_zero

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
⊢ ⊥ = ⊥
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
⊢ coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U

Tactic:
by
  refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)
  exact coverEntropyEntourage_le_log_coverMincard_div F_inv (Nat.one_le_iff_ne_zero.1 m_pos)

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
by
  refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)
  obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
  exact (coverEntropyEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
⊢ (σ * τ) a = (τ * σ) a

Tactic:
obtain ⟨d, hd⟩ := key τ

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (σ * τ) a = (τ * σ) a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
← hf.lintegral_map,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ

Tactic:
← withDensity_eq_iff (by fun_prop) (by fun_prop),

Goal state after:
G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
⊢ (σ * τ) b = (τ * σ) b

Tactic:
obtain ⟨d, hd⟩ := key τ

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ (σ * τ) b = (τ * σ) b
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
⊢ (map i (X ^ n - C a)).degree ≠ 0

Tactic:
rwa [degree_map]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : p.comp (X ^ n) = 0
⊢ p.leadingCoeff = 0

Tactic:
rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h
    rwa [natDegree_X_pow]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
m : ℕ
f : L.Functions m
xs : Fin m → L.Term α
n : ℕ
g : L.Functions n
ys : Fin n → L.Term α
h : m = n
this : DecidableEq (L.Term α) := instDecidableEq
⊢ (f = ⋯ ▸ g ∧ ∀ (i : Fin m), xs i = ys (Fin.cast h i)) ↔ func f xs = func g ys

Tactic:
subst h

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
m : ℕ
f : L.Functions m
xs : Fin m → L.Term α
this : DecidableEq (L.Term α) := instDecidableEq
g : L.Functions m
ys : Fin m → L.Term α
⊢ (f = ⋯ ▸ g ∧ ∀ (i : Fin m), xs i = ys (Fin.cast ⋯ i)) ↔ func f xs = func g ys
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ ((var a✝).substFunc fun {n} ↦ Functions.term) = var a✝

pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝

Tactic:
· rfl

Goal state after:
case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
Function.leftInverse_iff_comp,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ φ.invLHom.onTerm ∘ φ.toLHom.onTerm = id
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) φ) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) φ

Tactic:
by
  induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) φ = φ

Tactic:
by
  induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel]
  | rel => simp [mapTermRel]
  | imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
  | all _ ih3 => simp [mapTermRel, ih3]

Goal state after: