mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ ↑(chineseRemainderOfList a s l co) < (List.map s l).prod

Tactic:
cases l with

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
h : n < p
⊢ IsUnit ↑n !

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
    refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
    rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact Nat.not_dvd_of_pos_of_lt (by lia) h

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
induction k with

Goal state after:
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 1 m k = m + k

Tactic:
induction k with

Goal state after:
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 2 m k = m * k

Tactic:
induction k with

Goal state after:
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 3 m k = m ^ k

Tactic:
induction k with

Goal state after:
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0

Tactic:
induction k with

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ 1 ∈ Icc 1 (n - 1) ∧ n.choose 1 ≠ 0

Tactic:
by simp; grind [IsPrimePow.two_le h]

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ ↑hf.toFinset = Set.ofPred p

Tactic:
Set.Finite.coe_toFinset

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ Set.ofPred p = Set.ofPred p
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

pp: case node.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
· rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1
    rw [l0, m1.1, m1.2]; revert r0; rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]

Goal state after:
case node.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (-[n + 1+1] + 1) = ZNum.ofInt' -[n + 1+1] + 1

Tactic:
by
    change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i n.succ)

Tactic:
induction n generalizing i with

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Goal state after:
case a
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Goal state after:
case a
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
← factorMultiset_le_iff'

Goal state after:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hn
m n : ℕ+
⊢ n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
← factorMultiset_le_iff'

Goal state after:
case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrx : α
hl : (nil.node' lx (node lrs nil lrx nil)).Balanced
sl : (node ls nil lx (node lrs nil lrx nil)).Sized
this : nil.size = 0 ∧ nil.size = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (nil.node' lx (node lrs nil lrx nil)).node' x nil
    else (nil.node' lx (node lrs nil lrx nil)).rotateR x nil

Tactic:
obtain rfl : lrs = 1 := sl.2.2.1

Goal state after:
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrx : α
this : nil.size = 0 ∧ nil.size = 0
hl : (nil.node' lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + 1 + 1 ≤ 1 then (nil.node' lx (node 1 nil lrx nil)).node' x nil
    else (nil.node' lx (node 1 nil lrx nil)).rotateR x nil
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ (wp + 1) * (zp + 1) = x * y + 1

Tactic:
simp_all [← h]

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hij : i < j
⊢ ⟨i, a⟩ ≤ ⟨j, b⟩ ∨ ⟨j, b⟩ ≤ ⟨i, a⟩

Tactic:
exact Or.inl (Lex.left _ _ hij)

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
⊢ m.dist n ≤ 1

Tactic:
rw [Nat.dist_comm]; exact H.dist_le

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 ↦ x) x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

Goal state after:
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
wrepr,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF ((P F).wMk' ∘ repr) ((P F).wMk a f' f) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) a.dest b.dest

Tactic:
rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$> (TypeVec.id ::: f) <$$> g (f x))
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
l' : List (Computation α)
e' : parallel.aux2 l = Sum.inr l'
⊢ s ∈ l'

Tactic:
induction l generalizing l' with

Goal state after:
case cons
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
m : s.think ∈ c :: l
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
⊢ s ∈ l'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ (s.get? n).Terminates → (s.get? m).Terminates

Tactic:
by
  induction h with
  | refl => exact id
  | step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (Computation.map (fun o ↦ Option.rec nil Prod.snd o) s.destruct)
    (Computation.map (fun o ↦ Option.rec nil Prod.snd o) t.destruct)

Tactic:
rw [← Computation.bind_pure, ← Computation.bind_pure]

Goal state after:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (s.destruct.bind (Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o))
    (t.destruct.bind (Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o))
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 : ℕ
⊢ ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
induction n using Nat.strongRecOn with | _ n IH
   =>  _ 

Goal state after:
case ind
α : 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 β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b
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
c : Computation α
⊢ id c = ((map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c) c

Tactic:
dsimp [id, Function.comp_def]

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
c : Computation α
⊢ c = map (fun c ↦ c.1) (map (fun a ↦ (a, c)) c)
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
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
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T

Tactic:
have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _

Goal state after:
case inr
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
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : μ (I j) ≠ 0
hI₁ : μ (I j) ≠ ∞
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

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

Tactic:
contrapose! h

Goal state after:
case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑s
⊢ ∃ a, addOrderOf a ≠ 0 ∧ s = AddSubgroup.zmultiples a
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s)ᶜ = 0

Tactic:
rw [← mem_ae_iff, ← Filter.eventuallyEq_univ,
      ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]

Goal state after:
case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (μ.singularPart ν) univ
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 ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)

Tactic:
conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
  have hν_ac : ν ≪ ν.withDensity f := withDensity_absolutelyContinuous' hf hf_ne_zero
  refine hν_ac.ae_eq ?_
  have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
  refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm
  exact ((mutuallySingular_singularPart μ ν).symm.withDensity).symm

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s

Tactic:
refine iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩
  rw [← image2_image_left]
  exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s

Tactic:
by
  refine iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩
  rw [← image2_image_left]
  exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
· rintro (hy | hy)
    exacts [omegaLimit_mono_right _ _ subset_union_left hy,
      omegaLimit_mono_right _ _ subset_union_right hy]

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 : ℕ
⊢ IsDynCoverOf T F U n ∅ ↔ F = ∅

Tactic:
by simp [IsDynCoverOf]

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

Goal state before:
pp: 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 : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
y : Y
hy : y ∈ ↑s
hxy : (φ x, y) ∈ dynEntourage T V n
⊢ (y, g y) ∈ dynEntourage T V n

Tactic:
exact g_rel _ hy

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n {x}
⊢ False

Tactic:
rw [← Finset.coe_singleton] at key

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n = 0
x : X
x_F : x ∈ F
key : IsDynNetIn T F U n ↑{x}
⊢ False
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ 0 ∈ range fun s ↦ ⨅ (_ : IsDynCoverOf T ∅ U n ↑s), ↑(#s)

Tactic:
by simp [IsDynCoverOf]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

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
m n : ℕ
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
by
  rcases F.eq_empty_or_nonempty with rfl | F_nonempty
  · simp
  obtain rfl | hn := eq_or_ne n 0
  · rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]
  rcases eq_top_or_lt_top (coverMincard T F U m) with h | h
  · simp [*]
  · obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h
    obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv n
    rw [← s_coverMincard]
    exact t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (V ∩ m • U).Nonempty) ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ i, (U_1 ∩ i • U).Nonempty

Tactic:
exact ⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h h₁ h₂ h₃ h₄, fun h _ _ h₁ h₂ h₃ h₄ ↦ h h₁ h₂ _ h₃ h₄⟩

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
⊢ Group.IsSolvable q.Gal

Tactic:
let ϕ : Gal(L/K) ≃* (q.map (algebraMap F K)).Gal :=
    (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (map (algebraMap F K) q)).autCongr
⊢ Group.IsSolvable q.Gal