mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
⊢ u ∈ f' '' univ

Tactic:
have : u ∈ supp x := by rw [← hfi]; apply h'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
obtain ⟨b, t⟩ := b

Goal state after:
case some.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝¹ t✝¹ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝
s✝ u t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq β
f : Set (α → β)
s : Set α
inst✝¹ : Fintype ↑f
inst✝ : Fintype ↑s
⊢ Fintype ↑(f.seq s)

Tactic:
seq_def

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq β
f : Set (α → β)
s : Set α
inst✝¹ : Fintype ↑f
inst✝ : Fintype ↑s
⊢ Fintype ↑(⋃ f_1 ∈ f, f_1 '' s)
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(f.seq s)

Tactic:
seq_def

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(⋃ f_1 ∈ f, f_1 '' s)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (Sum.inr [])

Tactic:
intro a h
      assumption

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t : WSeq β
h✝ : LiftRel R s✝ t
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some b))

Tactic:
obtain ⟨b, t⟩ := b

Goal state after:
case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t✝ : WSeq β
h✝ : LiftRel R s✝ t✝
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some (b, t)))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case think
α : Type u
l : List α
s : WSeq α
s1 s2 : Computation (List α)
l' : List α
s✝ : WSeq α
h :
  s1 =
      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✝.think) ∧
    s2 =
      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✝.think))
⊢ BisimO
    (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)))
    (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✝.think)).destruct
    (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✝.think))).destruct

Tactic:
case think s => refine ⟨l', s, ?_, ?_⟩ <;> simp

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

Goal state before:
pp: case some.some
α : 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
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (a, s))) (destruct_append.aux t2 (some b))

Tactic:
obtain ⟨b, t⟩ := b

Goal state after:
case some.some
α : 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✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (a, s))) (destruct_append.aux t2 (some (b, t)))
Module: Mathlib.Data.String.Basic

Goal state before:
pp: s₁ s₂ : String
⊢ ltb (Legacy.iter s₁) (Legacy.iter s₂) = true ↔ s₁ < s₂

Tactic:
obtain ⟨s₁, rfl⟩ := s₁.exists_eq_ofList

Goal state after:
s₂ : String
s₁ : List Char
⊢ ltb (Legacy.iter (ofList s₁)) (Legacy.iter s₂) = true ↔ ofList s₁ < s₂
Module: Mathlib.Data.String.Basic

Goal state before:
pp: l : List Char
c : Char
cs : List Char
h : ofList (c :: cs) ≠ ""
⊢ (ofList (c :: cs)).toList = Legacy.front (ofList (c :: cs)) :: (Legacy.drop (ofList (c :: cs)) 1).toList

Tactic:
simp [Legacy.front, Pos.Raw.get, Pos.Raw.utf8GetAux]

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

pp: case inr
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
· obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact Sym2.card

Goal state after:
case inr
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
⊢ Nat.card (Sym2 α) = (Nat.card α + 1).choose 2

Tactic:
cases finite_or_infinite α
  · obtain ⟨_⟩ := nonempty_fintype α; let := Classical.decEq α
    simp_rw [Nat.card_eq_fintype_card]
    exact Sym2.card
  · simp

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
x✝ : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)

Tactic:
by
          refine i.cases' ?_ ?_
          exacts [pa, h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : Ergodic f μ
hs : NullMeasurableSet s μ
hs' : f '' s ≤ᵐ[μ] s
h_fin : μ s ≠ ∞
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
by
  replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
    (LE.le.eventuallyLE (subset_preimage_image f s)).trans
      (hf.quasiMeasurePreserving.preimage_mono_ae hs')
  exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f x - ↑⌊x⌋ - (x - ↑⌊x⌋) = f x - x

Tactic:
sub_sub_sub_cancel_right

Goal state after:
f : CircleDeg1Lift
x : ℝ
⊢ f x - x = f x - x
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
⊢ Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)

Tactic:
let δ : ι → ℝ := fun j => T / (2 * ↑(n j))

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
⊢ Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a b : ℝ
⊢ Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)

Tactic:
rcases eq_or_ne b 0 with rfl | hb
  · rw [pair_comm]
    simpa [← AddSubgroup.zmultiples_eq_closure] using! not_denseRange_zsmul
  constructor
  · rintro hd ⟨r, hr⟩
    refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_
    rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]
    refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
    · simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]
    · simp [field]
  · intro h
    contrapose h
    rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩
    have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by
      rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
      apply AddSubgroup.subset_closure
    rcases pair_subset_iff.1 this with ⟨⟨m, rfl⟩, n, rfl⟩
    simp_all [mul_div_mul_right]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
| (μ.withDensity f).rnDeriv ν

Tactic:
μ.haveLebesgueDecomposition_add ν,

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
| ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
| μ.rnDeriv (ν.withDensity f)

Tactic:
μ.haveLebesgueDecomposition_add ν,

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
| (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
have : Nonempty {s : Finset X // IsDynCoverOf T F U n s} := by
    by_contra h
    apply ENat.natCast_ne_top k
    rw [k_min, coverMincard, iInf₂_eq_top]
    simp only [ENat.natCast_ne_top, imp_false]
    rw [nonempty_subtype, not_exists] at h
    exact h

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(coverMincard T F U n)) ≠ 0

Tactic:
rw [ne_eq, funext_iff.not, not_forall]
    use 0
    rw [coverMincard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
    exact one_ne_zero

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone fun m ↦ ↑(coverMincard T F (U ○ U) m)
h :
  (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) / ↑n =
    expGrowthSup fun m ↦ ↑(coverMincard T F (U ○ U) m)
m : ℕ
⊢ ↑(coverMincard T F (U ○ U) (n * m)) ≤ ↑(coverMincard T F U n ^ m)

Tactic:
exact ENat.toENNReal_mono (coverMincard_mul_le_pow F_inv n m)

Goal state after:
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:
refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m : ℕ
m_pos : 1 ≤ m
⊢ coverEntropyEntourage T F (U ○ U) ≤ ((fun n ↦ ↑(coverMincard T F U n)) m).log / ↑m
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x ↦ (map f μ).rnDeriv (map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν

Tactic:
μ.haveLebesgueDecomposition_add ν,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x ↦ (map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

Tactic:
by
  rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]
  exacts [measurable_rnDeriv _ _, ae_restrict_of_ae (rnDeriv_lt_top _ _), hs]

Goal state after:
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✝² : SigmaFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : SigmaFinite ν₁
inst✝ : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = ν₁ ∗ₘ ν₂

Tactic:
withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂)

Goal state after:
G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SigmaFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : SigmaFinite ν₁
inst✝ : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
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

Goal state after:
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)).leadingCoeff = 0
⊢ (X ^ n).natDegree ≠ 0
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ relabel id (var a✝) = var a✝

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
a✝ : α
⊢ relabel g (relabel f (var a✝)) = relabel (g ∘ f) (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
a✝ : α
⊢ (var a✝).constantsToVars.varsToConstants = var a✝

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ (LHom.id L).onTerm (var a✝) = id (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
a✝ : α
⊢ (φ.comp ψ).onTerm (var a✝) = (φ.onTerm ∘ ψ.onTerm) (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
a✝ : α
⊢ realize v (relabel g (var a✝)) = realize (v ∘ g) (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
a✝ : α
⊢ realize v ((var a✝).subst tf) = realize (fun a ↦ realize v (tf a)) (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
β : Type v'
inst✝ : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
a✝ : β
⊢ realize v ((var a✝).substFunc fun {n} ↦ c) = realize v (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
a✝ : α
f : ↥(var a✝).varFinset → β
hv' : ∀ (a : ↥(var a✝).varFinset), v (f a) = v' ↑a
⊢ realize v ((var a✝).restrictVar f) = realize v' (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: case var
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
a✝ : β
⊢ realize (fun i ↦ ⟦x i⟧) (var a✝) = ⟦realize x (var a✝)⟧

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
a✝ : β
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (var a✝).constantsToVars = realize v (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔ ∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1

Tactic:
refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩

Goal state after:
case refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

case refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
a✝ : α
⊢ Term.realize v (φ.onTerm (var a✝)) = Term.realize v (var a✝)

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3.var
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
a✝ : β
⊢ Term.realize (fun i ↦ x i a) (var a✝) = Term.realize x (var a✝) a

Tactic:
| var =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a✝ : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((var a✝).listEncode ++ l) = var a✝ :: listDecode l

Tactic:
| var =>

Goal state after: