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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1

Tactic:
refine multiplicity_eq_of_dvd_of_not_dvd ?_ (minFac_sq_ndvd_gcd_choose_of_isPrimePow h)

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ n.minFac ^ 1 ∣ (Icc 1 (n - 1)).gcd n.choose
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : ¬IsPrimePow n
⊢ (Icc 1 (n - 1)).gcd n.choose = 1

Tactic:
contrapose! hpn
  obtain ⟨q, hq, h⟩ := Nat.exists_prime_and_dvd hpn
  simp_rw [Finset.dvd_gcd_iff, ← modEq_zero_iff_dvd] at h
  have : Fact (Nat.Prime q) := ⟨hq⟩
  have := eq_pow_multiplicity_of_choose_modEq_zero_nat (zero_lt_of_lt hn) h
  refine (isPrimePow_nat_iff n).mpr ⟨q, _, hq, Dvd.multiplicity_pos ?_, this.symm⟩
  specialize h 1 (by grind)
  rw [choose_one_right, modEq_zero_iff_dvd] at h
  exact h

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

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit0

Tactic:
exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))

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

Goal state before:
pp: n : PosNum
⊢ n.bit0.Prime ↔ n = 1

Tactic:
refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)
        · exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))
        rw [← minFac_to_nat, to_nat_inj]
        exact ⟨bit0.inj, congr_arg _⟩

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

Goal state before:
pp: case hz
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : ∀ (hfi : (Set.ofPred p).Finite), 0 < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) 0) = nth p 0

pp: case hi
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n✝ : ℕ
a✝ : ∀ m ≤ n✝, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n✝ + 1 < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) (n✝ + 1)) = nth p (n✝ + 1)

Tactic:
case _ =>
    simp_rw [nth_zero]
    replace h := nth_mem _ h
    rw [← hs h0, ← hf.monotone.map_csInf]
    rcases h0 _ h with ⟨t, ht⟩
    exact ⟨t, Set.mem_ofPred_eq ▸ ht ▸ h⟩

Goal state after:
case hi
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n✝ : ℕ
a✝ : ∀ m ≤ n✝, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n✝ + 1 < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) (n✝ + 1)) = nth p (n✝ + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(ZNum.bit1 0) = ↑0 + ↑0 + 1

Tactic:
by simp [ZNum.bit1]

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

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
rintro ⟨u, xeq, yeq⟩

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
⊢ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.size = t.size

Tactic:
by cases t <;> rfl

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

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
⊢ LiftR r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
rintro ⟨u, xeq, yeq⟩

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
⊢ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
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✝) = (↑b✝).gcd ↑a✝

Tactic:
exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)

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

Goal state before:
pp: case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
h_a_1 : ⟨x_a, x_f⟩ = ⟨a, x'⟩
⊢ Agree (CofixA.intro x_a fun j ↦ (x_f j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))

Tactic:
cases h_a_1

Goal state after:
case mpr.succ.step.f.f.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
⊢ Agree (CofixA.intro a fun j ↦ (x' j).approx n✝) (CofixA.intro y_a fun j ↦ (y_f j).approx (n✝ + 1))
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 α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)

Tactic:
exact h₁

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

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
· exact hr.rotateL_size

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
replace H₂ : _ ≤ 3 * _ := H₂ l0 r0

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
H₂ : r.size ≤ 3 * l.size
⊢ 2 * r.size ≤ 9 * l.size + 5
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.merge nil = t

Tactic:
by cases t <;> rfl

Goal state after:
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 α
i : P.last.B a
⊢ g <$$> f i = ⟨(f i).fst, g ⊚ (f i).snd⟩

Tactic:
cases f i

Goal state after:
case mk
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 α
i : P.last.B a
fst✝ : P.wp.A
snd✝ : P.wp.B fst✝ ⟹ α
⊢ g <$$> ⟨fst✝, snd✝⟩ = ⟨⟨fst✝, snd✝⟩.fst, g ⊚ ⟨fst✝, snd✝⟩.snd⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.right
m n : ℕ+
⊢ m.gcd n ∣ n

Tactic:
· exact gcd_dvd_right m n

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

Goal state before:
pp: case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      nil.node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else nil.node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

pp: case nil.node.node.node.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ ¬rls + rrs + 1 ≤ 1

Tactic:
· dsimp only [size_node]; split_ifs
          · simp [node3L, node']; abel
          · simp [node4L, node', sr.2.1.1]; abel

Goal state after:
case nil.node.node.node.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ ¬rls + rrs + 1 ≤ 1
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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
⊢ LiftR r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

Tactic:
rintro ⟨u, xeq, yeq⟩

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.balanceL x r = l.balance' x r

Tactic:
rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]

Goal state after:
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.size = 0 → r.size ≤ 1

case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
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
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (corecF g x) = (TypeVec.id ::: corecF g) <$$> repr (g x)

Tactic:
rw [corecF, M.dest_corec]

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

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

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

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
rintro ⟨u, xeq, yeq⟩

Goal state after:
case mp
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x

Tactic:
apply Quot.ind

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : (P F).W α), g₁ (Quot.mk (⇑(wSetoid α)) a) = g₂ (Quot.mk (⇑(wSetoid α)) a)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)) (WType.mk a f)

Tactic:
apply Wequiv.ind

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : (P F).B a), Wequiv ((Wrepr ∘ f) x) (f x)
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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
⊢ ∀ (x : Fix F α), p x

Tactic:
apply Quot.ind

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
⊢ ∀ (a : (P F).W α), p (Quot.mk (⇑(wSetoid α)) a)
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
⊢ ∀ (x : Fix F α), Quot.mk WEquiv (fixToW x) = x

Tactic:
apply Quot.ind

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α : TypeVec.{u} n
⊢ ∀ (a : (P F).W α), Quot.mk WEquiv (fixToW (Quot.mk (⇑(wSetoid α)) a)) = Quot.mk (⇑(wSetoid α)) a
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
⊢ s.drop n ~ʷ t.drop n

Tactic:
by
  induction n <;> simp [*, tail_congr, drop]

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))

Tactic:
obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        exact ⟨h2 r, s, rfl, t, rfl, h⟩

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ d
dl : d ∈ val✝
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩

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

Goal state before:
pp: case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }

Tactic:
simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm

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

Goal state before:
pp: case h2
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α),
    (∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
        s_1.append S.join = s.think → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s

Tactic:
· 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.String.Lemmas

Goal state before:
pp: n : ℕ
c : Char
x✝ : String
s : String := x✝
⊢ (leftpad n c x✝).length = max n x✝.length

Tactic:
simp [leftpad, length_toList, Nat.sub_add_eq_max]

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

Goal state before:
pp: α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t.think)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append t.think).destruct.destruct (nil.destruct.bind (destruct_append.aux t.think)).destruct

Tactic:
exact ⟨nil, t, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = (map (map f) S).join

Tactic:
by
  apply
    Seq.eq_of_bisim fun s1 s2 =>
      ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
  · rintro s1 s2 ⟨s, S, rfl, rfl⟩
    induction s using WSeq.recOn
    · induction S using WSeq.recOn with
      | nil => simp
      | cons s S => simpa using ⟨map f s, S, rfl, rfl⟩
      | think S => simpa using ⟨nil, S, by simp, by simp⟩
    · simpa using ⟨_, _, rfl, rfl⟩
    · simpa using ⟨_, _, rfl, rfl⟩
  · exact ⟨nil, S, by simp, by simp⟩

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

Goal state before:
pp: case nil.nil.think
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ ∃ s S T_1,
    T.join.destruct = (s.append (S.append T_1).join).destruct ∧
      T.join.destruct = (s.append (S.join.append T_1.join)).destruct

Tactic:
refine ⟨nil, nil, T, ?_, ?_⟩

Goal state after:
case nil.nil.think.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.append T).join).destruct

case nil.nil.think.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.join.append T.join)).destruct
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r) =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> (node <$> g v <*> traverse g l <*> traverse g r))

Tactic:
simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]

Goal state after:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ Functor.Comp.mk
      ((fun a x x_1 ↦ node <$> f a <*> traverse f x <*> traverse f x_1) <$> g v <*> traverse g l <*> traverse g r) =
    Functor.Comp.mk ((fun a x x_1 ↦ traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r)
Module: Mathlib.Data.Vector.Zip

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (zipWith f x y).get i = f (x.get i) (y.get i)

Tactic:
dsimp only [Vector.zipWith, Vector.get]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (List.zipWith f ↑x ↑y).get (Fin.cast ⋯ i) = f ((↑x).get (Fin.cast ⋯ i)) ((↑y).get (Fin.cast ⋯ i))
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f xs s = (s, map (fun x ↦ (f x s).2) xs)

Tactic:
by
  induction xs using revInductionOn <;> simp_all

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:
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.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ MeasurePreserving f (μ.restrict s) (μ.restrict s)

Tactic:
convert! hf.restrict_preimage hsm
        exact hfs.symm

Goal state after: