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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.descFactorial a / a !)

Tactic:
exact (hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right
    (Nat.factorial_dvd_descFactorial b a)

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

Tactic:
rw [floorRoot_def]
  split_ifs with h
  · obtain rfl | rfl := h <;> simp
  apply a.factorization_prod_pow_eq_self_of_le_factorization
  exact le_self_nsmul (by simp) (by lia) |>.trans <| smul_floorDiv_le (by lia)

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p

Tactic:
have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp

Goal state after:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b ↦ b + 2 ≤ a) (l ++ [0])
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
⊢ (map fib (a :: l)).sum < fib n

Tactic:
simp only [mem_append, mem_singleton, ← isChain_iff_pairwise, or_imp, forall_and, forall_eq,
      zero_add] at hl

Goal state after:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
← isChain_iff_pairwise

Goal state after:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
Module: Mathlib.Data.Nat.Choose.Lucas

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

Tactic:
simp; grind [IsPrimePow.two_le h]

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
n✝ m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
n_ih : head' (x n.succ) = head' (x 1)
⊢ head' (x (n + 1).succ) = head' (x 1)

Tactic:
grind +splitIndPred [Hconsistent (succ n), head']

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Tactic:
· rw [Nat.gcd_comm]
    exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)

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

Goal state before:
pp: case root.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x 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)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
g₂' : P.last.B a → P.last.M
e₂' : x.dest = ⟨a, g₂'⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)

Tactic:
cases h'.symm.trans e₂'

Goal state after:
case root.refl.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x 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)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₂' : x.dest = ⟨a, f⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case child.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x 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)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
g₂' : P.last.B a → P.last.M
e₂' : x.dest = ⟨a, g₂'⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)

Tactic:
cases h'.symm.trans e₂'

Goal state after:
case child.refl.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x 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)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₂' : x.dest = ⟨a, f⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
⊢ (node ls ll lx lr).rotateL x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      rl

Tactic:
have rd : delta ≤ size rl + size rr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
            rwa [sr.1, Nat.lt_succ_iff] at this
          obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
          · rw [size, zero_add] at rd
            exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
          obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
          · exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
          dsimp [rotateL]; split_ifs
          · simp [node3L, node', sr.1]; abel
          · simp [node4L, node', sr.1, sr.2.1.1]; abel

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

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)) → LiftP p x

Tactic:
· rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use a, fun i j => (f i j).val
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]; rfl
    intro i j
    apply (f i j).property

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)) → LiftP p x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
x : (P F).W
⊢ Wequiv (Wrepr x) x

Tactic:
induction x with | _ a f ih
  apply Wequiv.trans (v := PFunctor.W.mk (q.P.map Wrepr ⟨a, f⟩))
  · apply Wequiv.abs'
    have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl
    rw [this, PFunctor.W.dest_mk, abs_repr]
    rfl
  apply Wequiv.ind; exact ih

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

Tactic:
by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · exact Or.inl <| sign_of_neg hn
  · exact Or.inr <| Or.inl <| sign_zero
  · exact Or.inr <| Or.inr <| sign_of_pos hp

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
⊢ enumerate sel s (m' + 1) = none

Tactic:
simp only [enumerate, hs] at h ⊢

Goal state after:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b

Tactic:
· rintro ⟨i, a, b, h⟩
    exact ⟨rfl, h⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd

pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b

Tactic:
· rintro ⟨i, a, b, h⟩
    exact ⟨rfl, h⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b
Module: Mathlib.Data.String.Basic

Goal state before:
pp: c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos.Raw
⊢ ltb { s := ofList (c :: cs₁), i := i₁ + c } { s := ofList (c :: cs₂), i := i₂ + c } =
    ltb { s := ofList cs₁, i := i₁ } { s := ofList cs₂, i := i₂ }

Tactic:
by
  rw [eq_comm, ← ltb_cons_addChar' c]
  simp

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

Goal state before:
pp: case bisim.nil.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.think.join))) (Seq.destruct (nil.append (map (map f) S.think).join))

Tactic:
simpa using ⟨nil, S, by simp, by simp⟩

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
rcases h with ⟨R, h₀, hR⟩
  exact (mapAccumr_bisim R h₀ hR).2

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
⊢ stabilizer G s ≤ aestabilizer G μ s

Tactic:
by
  intro g hg
  simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x ∈ MulAction.aestabilizer G μ s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᵐ[μ] s

Tactic:
← Subgroup.zpowers_le

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : Subgroup.zpowers x ≤ MulAction.aestabilizer G μ s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᵐ[μ] s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ f 0 + g 0 - 1 < f (g 0) ∧ f (g 0) < f 0 + g 0 + 1

Tactic:
exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x ≤ x + ↑m
n : ℕ
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m

Tactic:
by
  simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n

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

Goal state before:
pp: a p : ℝ
⊢ Dense ↑(AddSubgroup.zmultiples a ⊔ (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)).ker) ↔
    Dense ↑(AddSubgroup.closure {a, p})

Tactic:
QuotientAddGroup.ker_mk',

Goal state after:
a p : ℝ
⊢ Dense ↑(AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples p) ↔ Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense ↑(AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s)
⊢ ∃ a, s = AddSubgroup.zmultiples a

Tactic:
xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∃ a, AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ ∃ a, s = AddSubgroup.zmultiples a
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: 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) ≠ ∞
⊢ n j • ENNReal.ofReal (T / ↑(n j)) = ENNReal.ofReal T

Tactic:
← ENNReal.ofReal_nsmul,

Goal state after:
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) ≠ ∞
⊢ ENNReal.ofReal (n j • (T / ↑(n j))) = ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case hb
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) ≠ ∞
⊢ ↑(n j) ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr hj.ne'

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 μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s

Tactic:
rwa [add_comm, iterate_add_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
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
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ #Finset.univ • ENNReal.ofReal (min T (2 * (T / (2 * ↑n))))

Tactic:
← ENNReal.ofReal_nsmul,

Goal state after:
case refine_4
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
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (#Finset.univ • min T (2 * (T / (2 * ↑n))))
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
· exact fun _ ↦ isClosed_closure

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

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyInfEntourage T F U ≤ coverEntropyInf T F

Tactic:
apply (netEntropyInfEntourage_antitone T F SetRel.symmetrize_subset_self).trans
    apply (le_iSup₂ (SetRel.symmetrize U) (symmetrize_mem_uniformity U_uni)).trans'
    exact netEntropyInfEntourage_le_coverEntropyInfEntourage T F

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

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

Tactic:
ha,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
inst✝ : UniformSpace X
⊢ coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G)

Tactic:
by
  simp only [coverEntropy, ← iSup_sup_eq]
  exact biSup_congr fun _ _ ↦ coverEntropyEntourage_union

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
ha,

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n - C 0).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
⊢ (map i (X ^ n - 1)).Splits

Tactic:
have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp i.injective a) ha

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''

Tactic:
rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (f.apply₂ t₁ t₂) = funMap f ![realize v t₁, realize v t₂]

Tactic:
rw [Functions.apply₂, Term.realize]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim v xs) t

Tactic:
refine _root_.trans ?_ realize_constantsToVars

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs)) t.constantsToVars
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ (liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)

Tactic:
rw [realize_liftAt_one (refl n), iff_eq_eq]
  refine congr rfl (congr rfl (funext fun i => ?_))
  rw [if_pos i.is_lt]

Goal state after: