mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) (g <$$> a₁)) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) (g <$$> a₂))

Tactic:
M.dest_map,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) (g <$$> a₂))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) (g <$$> a₂))

Tactic:
M.dest_map,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> (g ::: fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordset α
h_mem : Ordnode.mem x ↑t = true
⊢ 0 < t.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ mk
      ((TypeVec.id ::: Sigma.fst) <$$>
        (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x') =
    mk x'

Tactic:
simp only [appendFun_id_id, MvFunctor.id_map] at ih

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
⊢ mk
      ((TypeVec.id ::: Sigma.fst) <$$>
        (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x') =
    mk x'
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ r.sign = 0 ↔ r = 0

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, neg_eq_zero] at h
    exact (one_ne_zero h).elim
  · rfl
  · rw [sign_of_pos hp] at h
    exact (one_ne_zero h).elim

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

Goal state before:
pp: α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ Computation.LiftRel (LiftRelO Eq fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s.destruct t.destruct

Tactic:
refine liftRel_def.2 ⟨?_, ?_⟩
    · rw [← head_terminates_iff, ← head_terminates_iff]
      exact terminates_congr (h 0)
    · intro a b ma mb
      rcases a with - | a <;> rcases b with - | b
      · trivial
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))
      · obtain ⟨a, s'⟩ := a
        obtain ⟨b, t'⟩ := b
        injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab
        refine ⟨ab, fun n => ?_⟩
        refine
          (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
            ((?_ : get? (tail s) n ~ get? (tail t) n).trans
              (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
        rw [get?_tail, get?_tail]
        apply h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
⊢ map f (ret a) = ret (f a)

Tactic:
simp [ret]

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

Goal state before:
pp: α : Type u
a : α
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s ∈ S, a ∈ s

Tactic:
suffices
    ∀ ss : WSeq α,
      a ∈ ss → ∀ s S, append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
    from fun S h => (this _ h nil S (by simp) (by simp [h])).resolve_left (notMem_nil _)
  intro ss h
  apply mem_rec_on h
  · intro b ss o s S ej m
    induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip] <;>
      have := congr_arg Seq.destruct ej
    case nil.nil | nil.cons | nil.think | think => simp at this
    case cons =>
      simp only [cons_append, seq_destruct_cons, Option.some.injEq, Prod.mk.injEq] at this
      cases this with
      | intro b' s =>
        subst b' ss
        simp? at m ⊢ says simp only [cons_append, mem_cons_iff] at m ⊢
        rcases o with e | IH
        · simp [e]
        rcases m with e | m
        · simp [e]
        exact Or.imp_left Or.inr (IH _ _ rfl m)
  · intro ss IH s S ej m
    induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip] <;>
      have := congr_arg Seq.destruct ej
    case nil.cons | nil.think | think => simp at this; simp_all
    case nil.nil | cons => simp at this

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

Goal state before:
pp: case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Nat.card (Sym α k) = (Nat.card α).multichoose k

Tactic:
Nat.card_eq_fintype_card

Goal state after:
case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card (Sym α k) = (Fintype.card α).multichoose k
Module: Mathlib.Data.Sym.NatCard

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

Tactic:
Nat.card_eq_fintype_card

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2
Module: Mathlib.Data.Sym.NatCard

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

Tactic:
Nat.card_eq_fintype_card

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
g : α → β
hg : MeasurePreserving g μ μ'
hf : PreErgodic f μ
f' : β → β
h_comm : Semiconj g f f'
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ EventuallyConst s (ae μ')

Tactic:
rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]
    apply hf.aeconst_set (hg.measurable hs₀)
    rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
e : α ≃ᵐ β
h : MeasurePreserving (⇑e) μ μ'
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

Tactic:
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
    rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
  replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
  exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
    fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩

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

Goal state before:
pp: f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g

Tactic:
refine tendsto_nhds_unique ?_
    (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
  simp only [transnumAuxSeq, ← add_div]
  refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
    (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
  rw [h.mul_pow, dist_comm]
  exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

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}) μ
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

Tactic:
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩

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
x : α
left✝ : x ∈ s
hxn : x ∈ {x | ∀ m ≥ n, f^[m] x ∉ s}
hxm : f^[m] x ∈ s
⊢ False
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ #Finset.univ = Nat.card ↥(AddSubgroup.zmultiples u)

Tactic:
Nat.card_eq_fintype_card

Goal state after:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ #Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x

Tactic:
refine (Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ f x * μ.rnDeriv ν x) ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
⊢ IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ v, {x | ¬p.mulOccursInAt x v})

Tactic:
refine isClosed_iInter (fun hp => ?_)

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
⊢ IsClosed[Pi.topologicalSpace] (⋂ v, {x | ¬p.mulOccursInAt x v})
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ ∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv ν' x = 0 x

Tactic:
change μ.rnDeriv ν' =ᵐ[ν.restrict t] 0

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᵐ[ν.restrict t] 0
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n (insert x ↑s)
⊢ False

Tactic:
rw [← s.coe_insert x] at larger_net

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:

Tactic:
∫ x in s, (μ.rnDeriv ν x).toReal ∂ν
    ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν := by
        refine setIntegral_mono_set ?_ ?_ (LE.le.eventuallyLE (subset_toMeasurable _ _))
        · exact integrableOn_toReal_rnDeriv hμt
        · exact ae_of_all _ (by simp)
  _ = (withDensity ν (rnDeriv μ ν)).real t := setIntegral_toReal_rnDeriv_eq_withDensity' ht_m
  _ ≤ μ.real t := by
        simp only [measureReal_def]
        gcongr
        apply withDensity_rnDeriv_le
  _ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]

Goal state after:
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 ν
s : Set β
hs : MeasurableSet s
⊢ (map f (ν.withDensity (μ.rnDeriv ν))) s = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s

Tactic:
rw [hf.map_apply, withDensity_apply _ (hf.measurable hs), withDensity_apply _ hs,
    setLIntegral_map hs (Measure.measurable_rnDeriv _ _) hf.measurable]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, (map f μ).rnDeriv (map f ν) (f x) ∂ν
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
⊢ (sum fun x ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
by rw [sum_const, lift_aleph0]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀)

Tactic:
let := isAlgClosure_of_transcendence_basis v hv
      simpa using Algebra.IsAlgebraic.cardinalMk_le_max (Algebra.adjoin R (Set.range v)) K

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), (⇑hnp ∘ ⇑hmn) (funMap f x) = funMap f ((⇑hnp ∘ ⇑hmn) ∘ x)

Tactic:
by intros; simp only [Function.comp_apply, map_fun]; trivial

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
⊢ ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), (⇑hnp ∘ ⇑hmn) (funMap f x) = funMap f ((⇑hnp ∘ ⇑hmn) ∘ x)

Tactic:
by intros; simp only [Function.comp_apply, map_fun]; trivial

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: 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
x : L.Term β
⊢ realize v (x.substFunc fun {n} ↦ c) = realize v x

Tactic:
by
  induction x with
  | var => simp
  | func f ts ih => simp [← ih, ← hc]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case inr
p : ℕ
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K p
hp : p = 0
⊢ K ⊨ if p = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}

Tactic:
subst hp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K 0
⊢ K ⊨ if 0 = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime 0 then {eqZero 0} else {⊥}
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ (φ.comp ψ).onBoundedFormula (equal t₁✝ t₂✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁✝ t₂✝)

Tactic:
simp [Term.bdEqual]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v xs) ((ts✝ x✝).restrictVarLeft (f ∘ Set.inclusion ⋯)) = realize (Sum.elim v' xs) (ts✝ x✝)

Tactic:
rw [realize_restrictVarLeft v' (by simp [hv'])]

Goal state after:
case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts✝ x✝) = realize (Sum.elim v' xs) (ts✝ x✝)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
t : L.Term { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'

Tactic:
exact t.realize_mem _ fun i => hS' i.2

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim x✝ xs✝) (((fun x ↦ Term.constantsVarsEquivLeft) n✝).symm t✝) =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝

Tactic:
simp only [Term.constantsVarsEquivLeft_symm_apply, Term.realize_varsToConstants,
    coe_con, Term.realize_relabel]

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) t✝ =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : A.Definable L s
hAB : A ⊆ B
⊢ B.Definable L s

Tactic:
definable_iff_empty_definable_with_params

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : ∅.Definable L[[↑A]] s
hAB : A ⊆ B
⊢ ∅.Definable L[[↑B]] s