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

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ↑(n.choose (p ^ multiplicity p n)) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False

Tactic:
← mul_one (p ^ _),

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ↑(n.choose (p ^ multiplicity p n * 1)) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k

Tactic:
rcases (Set.ofPred p).finite_or_infinite with hf | hf

Goal state after:
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Finite
⊢ a ≤ nth p k

case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
a : P.A
f : P.B a ⟹ α
xeq : x = ⟨a, f⟩
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ LiftP p x

Tactic:
use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩

Goal state after:
case h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
a : P.A
f : P.B a ⟹ α
xeq : x = ⟨a, f⟩
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ (fun i ↦ Subtype.val) <$$> ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩ = x
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
⊢ ↑n % ↑m = 0 ↔ n % m = 0

Tactic:
← to_int_inj,

Goal state after:
m n : ZNum
⊢ ↑n % ↑m = 0 ↔ ↑(n % m) = ↑0
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
⊢ Valid' o₁ (l.node3L x rl rx rr) o₂

Tactic:
have rr0 : size rr > 0 :=
      (mul_lt_mul_iff_right₀ (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _)

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
⊢ Valid' o₁ (l.node3L x rl rx rr) o₂
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
⊢ (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
rcases M.dest P x with ⟨ax, fx⟩

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
⊢ (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
cases r <;> simp [rotateL, all_node']; split_ifs <;>
    simp [all_node3L, all_node4L, All]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
⊢ s₁ = s₂

Tactic:
apply ext

Goal state after:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
⊢ ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
h : ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α), g <$$> ⟨a, f⟩ = ⟨a, g ⊚ f⟩
⊢ g <$$> ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn f' fun i ↦ (f i).snd⟩ =
    ⟨WType.mk a fun i ↦ (f i).fst, P.wPathCasesOn (g ⊚ f') fun i ↦ g ⊚ (f i).snd⟩

Tactic:
rw [h, comp_wPathCasesOn]

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

Goal state before:
pp: v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Nat.Primes.toPNat v) = Multiset.map Subtype.val v

Tactic:
rw [Multiset.map_map]

Goal state after:
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Nat.Primes.toPNat) v = Multiset.map Subtype.val v
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩

Tactic:
by rw [wDest', wRec_eq]

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨i, a, hji⟩ | ⟨i, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba
      · rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
        · exact Lex.left _ _ hij
        · exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

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

Goal state before:
pp: u : XgcdType
hr : u.r = 0
⊢ u.q = u.qp + 1

Tactic:
by
  by_cases hq : u.q = 0
  · let h := u.rq_eq
    rw [hr, hq, mul_zero, add_zero] at h
    cases h
  · exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ f i '' univ

Tactic:
intro i u

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i✝ : Fin2 n
u✝ : α i✝
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i✝ u✝
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
i : Fin2 n
u : (P F).B a i
⊢ f i u ∈ f i '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
· rintro α ⟨a, f⟩
    simp only [LiftpPreservation] at h
    simp only [supp, h]

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

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

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

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

Goal state before:
pp: case nil.nil
⊢ ltb { s := ofList [], i := 0 } { s := ofList [], i := 0 } = true ↔ [] < []

Tactic:
unfold ltb

Goal state after:
case nil.nil
⊢ (if { s := ofList [], i := 0 }.hasNext = true then
        if { s := ofList [], i := 0 }.hasNext = true then
          if { s := ofList [], i := 0 }.curr = { s := ofList [], i := 0 }.curr then
            ltb { s := ofList [], i := 0 }.next { s := ofList [], i := 0 }.next
          else decide ({ s := ofList [], i := 0 }.curr < { s := ofList [], i := 0 }.curr)
        else true
      else false) =
      true ↔
    [] < []
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true

Tactic:
unfold ltb

Goal state after:
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ (if { s := ofList (c₂ :: cs₂), i := 0 }.hasNext = true then
      if { s := ofList [], i := 0 }.hasNext = true then
        if { s := ofList [], i := 0 }.curr = { s := ofList (c₂ :: cs₂), i := 0 }.curr then
          ltb { s := ofList [], i := 0 }.next { s := ofList (c₂ :: cs₂), i := 0 }.next
        else decide ({ s := ofList [], i := 0 }.curr < { s := ofList (c₂ :: cs₂), i := 0 }.curr)
      else true
    else false) =
    true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 } { s := ofList [], i := 0 } = true

Tactic:
unfold ltb

Goal state after:
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬(if { s := ofList [], i := 0 }.hasNext = true then
        if { s := ofList (c₁ :: cs₁), i := 0 }.hasNext = true then
          if { s := ofList (c₁ :: cs₁), i := 0 }.curr = { s := ofList [], i := 0 }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 }.next { s := ofList [], i := 0 }.next
          else decide ({ s := ofList (c₁ :: cs₁), i := 0 }.curr < { s := ofList [], i := 0 }.curr)
        else true
      else false) =
      true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
unfold ltb

Goal state after:
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if { s := ofList (c₂ :: cs₂), i := 0 }.hasNext = true then
        if { s := ofList (c₁ :: cs₁), i := 0 }.hasNext = true then
          if { s := ofList (c₁ :: cs₁), i := 0 }.curr = { s := ofList (c₂ :: cs₂), i := 0 }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 }.next { s := ofList (c₂ :: cs₂), i := 0 }.next
          else decide ({ s := ofList (c₁ :: cs₁), i := 0 }.curr < { s := ofList (c₂ :: cs₂), i := 0 }.curr)
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: 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 β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
exact
    let ⟨o, m, k, rs1, rs2, en⟩ := of_results_bind ra
    let ⟨p, mT, rop⟩ := Computation.exists_of_liftRel_left (liftRel_destruct ST) rs1.mem
    match o, p, rop, rs1, rs2, mT with
    | none, none, _, _, rs2, mT => by
      simp only [destruct_join]
      exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
    | some (s, S'), some (t, T'), ⟨st, ST'⟩, _, rs2, mT => by
      simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
      exact
        let ⟨k1, rs3, ek⟩ := of_results_think rs2
        let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
        let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
        match o', p', rop', rs4, rs5, mt with
        | none, none, _, _, rs5', mt => by
          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
        | some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt => by
          simp only [destruct_append.aux] at rs5
          refine ⟨some (b, append t' (join T')), ?_, ?_⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem
          rw [eq_of_pure_mem rs5.mem]
          exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    (s.destruct.bind (destruct_append.aux S.join)) (t.destruct.bind (destruct_append.aux T.join))

Tactic:
apply Computation.liftRel_bind _ _ (liftRel_destruct st)

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      Computation.LiftRel
        (LiftRelO R fun s1 s2 ↦
          ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
        (destruct_append.aux S.join a) (destruct_append.aux T.join b)
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
by
  refine funext fun j => j.cases' ?_ ?_ <;> intros <;> rfl

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot

Tactic:
with_reducible_and_instances rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Fintype α
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : OrderBot α
inst✝³ : OrderBot β
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)

Tactic:
by
  intro y
  change IsLUB (e ⁻¹' { x | f x ≤ y }) (e.symm (g y))
  rw [e.isLUB_preimage, e.apply_symm_apply]
  exact h y

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
⊢ ErgodicSMul G G μ

Tactic:
refine ⟨fun {s} hsm hs ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
⊢ ErgodicSMul Gᵐᵒᵖ G μ

Tactic:
refine ⟨fun {s} hsm hs ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| x

pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)

Tactic:
← DivisibleBy.div_cancel x h

Goal state after:
case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| (n - 1) • DivisibleBy.div x (n - 1)

case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: 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 : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) (f ⁻¹' s)

Tactic:
withDensity_absolutelyContinuous _ _ hνs,

Goal state after:
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 : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = 0 + (μ.singularPart ν) (f ⁻¹' s)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: 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
⊢ (ν.withDensity (μ.rnDeriv ν)) s + (μ.singularPart ν) s = (μ.singularPart ν) s

Tactic:
withDensity_absolutelyContinuous _ _ hνs,

Goal state after:
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
⊢ 0 + (μ.singularPart ν) s = (μ.singularPart ν) s
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ ∫⁻ (x : X) in s \ f ⁻¹' s, c ∂ν = ∫⁻ (x : X) in f ⁻¹' s \ s, c ∂ν

Tactic:
simp [hν_sdiff]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x →
    μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
hx_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
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 ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ'.rnDeriv ν x

Tactic:
hx_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x = (f x)⁻¹ * μ'.rnDeriv ν x