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

Goal state before:
pp: case pure
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ match a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
cases (destruct a).destruct

Goal state after:
case pure.inl
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Option (α × WSeq α)
⊢ match Sum.inl val✝, Sum.inl val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

case pure.inr
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Computation (Option (α × WSeq α))
⊢ match Sum.inr val✝, Sum.inr val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
s : WSeq α
n : ℕ
⊢ (cons a s).drop (n + 1) = s.drop n

Tactic:
by
  induction n with
  | zero => simp [drop]
  | succ n n_ih =>
    simp [drop, ← n_ih]

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

Goal state before:
pp: case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

pp: case mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f

Tactic:
· apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left
    intro
    injections

Goal state after:
case mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨i, b⟩ ≤ ⟨i, a⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨j, b⟩ ≤ ⟨i, a⟩

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨j, b⟩ ≤ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨i, b⟩ < ⟨i, a⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨j, b⟩ < ⟨i, a⟩

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨j, b⟩ < ⟨i, a⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨i, b⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨j, b⟩

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨j, b⟩
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨i, b⟩

pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨j, b⟩
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 }.next { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next =
    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 }

pp: case case1.hc
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
⊢ { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
· simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm

Goal state after:
case case1.hc
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
⊢ { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
Module: Mathlib.Data.String.Basic

Goal state before:
pp: s : String
h : s ≠ ""
⊢ s.toList = Legacy.front s :: (Legacy.drop s 1).toList

Tactic:
obtain ⟨l, rfl⟩ := s.exists_eq_ofList
    match l with
    | [] => simp at h
    | c::cs => simp [Legacy.front, Pos.Raw.get, Pos.Raw.utf8GetAux]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝² : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
x✝¹ : LiftRelO R (LiftRel R) none none
x✝ : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb

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

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ (Nat.card α).multichoose k = (Nat.card α + k - 1).choose k

Tactic:
Nat.multichoose_eq

Goal state after:
α : Type u_1
k : ℕ
⊢ (Nat.card α + k - 1).choose k = (Nat.card α + k - 1).choose k
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inr
α : Type u_1
h✝ : Infinite α
⊢ Nat.card { a // ¬a.IsDiag } = (Nat.card α).choose 2

Tactic:
· simp

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

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

Tactic:
· simp

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map (map fun c ↦ c.1) T

Tactic:
rw [← WSeq.map_comp]

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map ((map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c) S
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
by
  dsimp [bind]
  rw [map_comp]
  apply join_map_ret

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
⊢ 1 < n.natAbs

Tactic:
rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn

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

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

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

Goal state after:
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 • μ = μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
by
  have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _
  rw [haveLebesgueDecomposition_add μ ν]
  have h₁ := rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) (ν + ν')
  have h₂ := rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) ν
  refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm
  have h₃ := rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular
    (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hνν'
  have h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
    refine h_ac.ae_eq ?_
    simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]
    exact ⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩
  have h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0 := rnDeriv_singularPart μ ν
  filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
  simp only [Pi.add_apply]
  rw [hx₃, hx₄, hx₅]

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

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
key : ∃ x ∈ {s | IsDynNetIn T F U n ↑s}, x.card = k
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
simp only [mem_ofPred_eq] at key

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
key : ∃ x, IsDynNetIn T F U n ↑x ∧ x.card = k
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
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 _ | _

Goal state after:
case inl
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
h✝ : IsEmpty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

case inr
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
h✝ : Nonempty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inl
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : U.IsSymm
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n

pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
· simp

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ 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 := UniformSpace.comap φ u
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)

Tactic:
simp only [uniformity_comap φ, mem_comap] at U_uni

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
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

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
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top 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 := UniformSpace.comap φ u
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
simp only [uniformity_comap φ, mem_comap] at U_uni

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
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
⊢ coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy T F

Tactic:
by
  rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ((μ - μ.singularPart ν) Set.univ).toReal

Tactic:
Measure.measure_sub_singularPart,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) Set.univ).toReal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
simp [ha_lt_top.ne]

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

Goal state before:
pp: case h0
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0

pp: case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
· simp

Goal state after:
case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
simp [ha_lt_top.ne]

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α

Tactic:
by
  rw [withConstants, card_sum, card_constantsOn]

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1.inr.succ
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin (n + 1) → M
c : (constantsOn ↑A).Functions (n + 1)
⊢ f.toFun (funMap (Sum.inr c) x) = funMap (Sum.inr c) (f.toFun ∘ x)

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ Quotient.lift (RelMap r) ⋯ ⟦x⟧ ↔ RelMap r x

Tactic:
Quotient.lift_mk

Goal state after:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap r x ↔ RelMap r x
Module: Mathlib.ModelTheory.Syntax

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

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

pp: 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

Tactic:
· simp

Goal state after:
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.Syntax

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

pp: 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

Tactic:
· simp

Goal state after:
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