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
⊢ SuppPreservation → LiftpPreservation

Tactic:
intro h

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
⊢ LiftpPreservation → SuppPreservation

Tactic:
intro h

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ some a = some b → a = b

Tactic:
intro h

Goal state after:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h✝ : some a = some b ∨ C s'
h : some a = some b
⊢ a = b
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
intro h

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

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

Tactic:
intro h

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.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
⊢ some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
intro h

Goal state after:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
⊢ some a ∈ s.get? 0 → a ∈ s

Tactic:
intro h

Goal state after:
case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
⊢ some a ∈ s.get? (n✝ + 1) → a ∈ s

Tactic:
intro h

Goal state after:
case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n✝ + 1)
⊢ a ∈ s
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) c.destruct)

Tactic:
rcases h : destruct c with a | c' <;> simp only [rmap]

Goal state after:
case inr.inl
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)

case inr.inr
α : 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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (Sum.inr (c' :: val✝))
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
⊢ ⟨k, c⟩ ∈ sigmaLift (fun x ↦ Ioo) ⟨i, a⟩ ⟨j, b⟩ ↔ ⟨i, a⟩ < ⟨k, c⟩ ∧ ⟨k, c⟩ < ⟨j, b⟩

Tactic:
simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]

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.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2

Tactic:
exact card_subtype_not_diag

Goal state after:
Module: Mathlib.Data.UInt

Goal state before:
pp: n : UInt8
⊢ 2 ^ 8 < 55296

Tactic:
by decide

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ x.elim = f x

Tactic:
cases x

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty.{u + 1}
⊢ x.elim = f x

Tactic:
cases x

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

Goal state before:
pp: α : Type u
s : WSeq α
inst✝ : s.Productive
n m : ℕ
⊢ ((s.drop n).get? m).Terminates

Tactic:
by rw [← get?_add]; infer_instance

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.Productive ↔ t.Productive

Tactic:
simp only [productive_iff]

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates
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

Goal state after:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + ↑m
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mpr
a b : ℝ
hb : b ≠ 0
⊢ Irrational (a / b) → Dense ↑(AddSubgroup.closure {a, b})

Tactic:
intro h

Goal state after:
case inr.mpr
a b : ℝ
hb : b ≠ 0
h : Irrational (a / b)
⊢ Dense ↑(AddSubgroup.closure {a, b})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mpr
a b : ℝ
hb : b ≠ 0
⊢ Irrational (a / b) → Dense ↑(AddSubgroup.closure {a, b})

Tactic:
· 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.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
⊢ DenseRange fun x ↦ g ^ x

Tactic:
by
  intro a
  by_contra h
  obtain ⟨V, hV₁, hVo, hV⟩ :
      ∃ V : Set G, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ m : ℤ, g ^ m ≠ a * x / y := by
    rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
    have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
      Continuous.tendsto' (by fun_prop) _ _ (by simp)
    rw [nhds_prod_eq] at this
    simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h
  set s := ⋃ m : ℤ, g ^ m • V
  have hso : IsOpen s := isOpen_iUnion fun m ↦ hVo.smul _
  have hsne : s.Nonempty := ⟨1, mem_iUnion.2 ⟨0, by simpa⟩⟩
  have hd : Disjoint s (a • V) := by
    simp_rw [s, disjoint_iUnion_left, disjoint_left]
    rintro m _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
    apply hV y hy x hx m
    simp_all
  have hgs : (g * ·) ⁻¹' s = s := by
    simp only [s, preimage_iUnion, ← smul_eq_mul, preimage_smul]
    refine iUnion_congr_of_surjective _ (add_left_surjective (-1)) fun m ↦ ?_
    simp [zpow_add, mul_smul]
  cases hg.measure_self_or_compl_eq_zero hso.measurableSet hgs with
  | inl h => exact hso.measure_ne_zero _ hsne h
  | inr h =>
    refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
    rwa [disjoint_right] at hd

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s

Tactic:
intro h

Goal state after:
case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a
⊢ Dense ↑s
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
hf : HasCompactFixedSupport f
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f

Tactic:
· exact ⟨closure (fixedPoints f)ᶜ, isClosed_closure, hf, subset_closure⟩

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
huniv : ν univ = μ univ
⊢ ν = μ

Tactic:
rcases hμ.eq_smul_of_absolutelyContinuous hfν hνμ with ⟨c, rfl⟩
  rcases eq_or_ne μ 0 with rfl | hμ₀
  · simp
  · simp_all [ENNReal.mul_eq_right]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
h : G
⊢ mulShift 1 x h = x h

Tactic:
simp [mulShift]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v : G
⊢ G → A

Tactic:
intro h

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v h : G
⊢ A
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
intro h

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
⊢ ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
intro h

Goal state after:
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
⊢ ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
⊢ {p | p.support = U}.Finite

Tactic:
cases nonempty_fintype A
  classical
  -- Patterns with support U biject with (U → A) via restriction/extension
  let e : { p : Pattern A G // p.support = U } ≃ (U → A) :=
  { toFun := fun p i => p.1.config i.1
    invFun := fun f => ⟨{ config := fun g => if h : g ∈ U then f ⟨g, h⟩ else default,
                           support := U,
                           condition := fun g hg => by simp [hg] }, rfl⟩
    left_inv := by
      rintro ⟨⟨cfg, dom, cond⟩, hU⟩
      simp only at hU; subst hU
      apply Subtype.ext
      simp only [Pattern.mk.injEq, and_true]
      funext g
      by_cases hg : g ∈ dom
      · simp [hg]
      · simp [hg, cond g hg]
    right_inv := fun f => by ext i; simp [i.2] }
  let : Fintype { p : Pattern A G | p.support = U } := Fintype.ofEquiv (U → A) e.symm
  apply toFinite

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ

Tactic:
union_comm,

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ nᶜ ⊆ kᶜ ∪ k \ n
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 : ℕ
⊢ netMaxcard T F U n < ⊤ → ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

Tactic:
intro h

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 < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n) → netMaxcard T F U n < ⊤

Tactic:
intro h

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
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 : ℕ
⊢ netMaxcard T F U n = ⊤ → ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
intro h

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 : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ (∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card) → netMaxcard T F U n = ⊤

Tactic:
intro h

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤
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 : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
intro k
    rw [netMaxcard, iSup_subtype', iSup_eq_top] at h
    specialize h k (ENat.natCast_lt_top k)
    simp only [Nat.cast_lt, Subtype.exists, exists_prop] at h
    obtain ⟨s, s_net, s_k⟩ := h
    exact ⟨s, s_net, s_k.le⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
rw [← coverEntropyInf_restrict_subset hF hG]
  have hφ : Semiconj (G.domRestrict φ) (hG.restrict S G G) T := by
    intro a
    rw [G.domRestrict_apply, G.domRestrict_apply, hG.val_restrict_apply, h.eq a]
  apply (coverEntropyInf_image_le_of_uniformContinuous hφ
    (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'
  rw [← image_image_val_eq_domRestrict_image, image_preimage_coe G F, inter_eq_right.2 hF]

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

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

Tactic:
ha2

Goal state after:
α : 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)
⊢ μ.rnDeriv ν a < ∞ → μ.rnDeriv ν a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) 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 < ∞
hs_eq : s = f ⁻¹' f '' s
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
have : SigmaFinite (ν.map f) := hf.sigmaFinite_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 < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
← Measure.withDensity_rnDeriv_eq μ ν hμν

Goal state after:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
⊢ (fun x ↦
          let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        x =
      (fun x ↦
          let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
          ⟨↑p, ⟨x, ⋯⟩⟩)
        y →
    x = y

Tactic:
intro h

Goal state after:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  (fun x ↦
        let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      x =
    (fun x ↦
        let p := Classical.indefiniteDescription (fun x_1 ↦ x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯;
        ⟨↑p, ⟨x, ⋯⟩⟩)
      y
⊢ x = y
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
  · have : Fact p.Prime := ⟨hp⟩
    exact ringEquiv_of_Cardinal_eq_of_charP p hK hKL
  · simp only [hp] at *
    let : CharZero K := CharP.charP_to_charZero K
    let : CharZero L := CharP.charP_to_charZero L
    exact ringEquiv_of_equiv_of_charZero hK hKL

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
⊢ p.comp (X ^ n) ≠ 0

Tactic:
intro h

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
⊢ False
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
cases x

Goal state after:
case var.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val✝ : γ
⊢ (var (Sum.inl val✝)).varsToConstants.constantsToVars = var (Sum.inl val✝)

case var.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
val✝ : α
⊢ (var (Sum.inr val✝)).varsToConstants.constantsToVars = var (Sum.inr val✝)
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:
rw [add_assoc, add_comm 1, add_assoc]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: α : Type u'
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x

Tactic:
cases x

Goal state after:
case inl
α : Type u'
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)

case inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mul
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ Group.IsSolvable (minpoly F (y * z)).Gal

Tactic:
apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ y ∈ {y, z}

F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ z ∈ {y, z}