mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
⊢ (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1})) ⋙
              functor P hs).map
          g ≫
        ObjectProperty.homMk (counitApp Y.obj)).hom =
    (ObjectProperty.homMk (counitApp X.obj) ≫
        (𝟭 (Sheaf (coherentTopology (CompHausLike P)) (Type (max u w)))).map g).hom

Tactic:
simp only [functor, Functor.comp_obj, Functor.flip_obj_obj, ObjectProperty.ι_obj,
      ObjectProperty.lift_obj_obj, Functor.id_obj, Functor.comp_map, Functor.flip_obj_map,
      ObjectProperty.ι_map, ObjectProperty.lift_map, ObjectProperty.FullSubcategory.comp_hom,
      ObjectProperty.homMk_hom, Functor.id_map]

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
⊢ functorToPresheaves.map (g.hom.app (op (of P PUnit.{u + 1}))) ≫ counitApp Y.obj = counitApp X.obj ≫ g.hom
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ Epi f ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
rw [← isLocallySurjective_iff_epi', coherentTopology.isLocallySurjective_iff,
    regularTopology.isLocallySurjective_iff]

Goal state after:
A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.obj.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.hom.app (op X'))) x = (hom (Y.obj.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom ((compHausToCondensed.map f).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((compHausToCondensed.obj Y✝).obj.map (Opposite.op φ))) g

Tactic:
refine ⟨pullback f g.down, pullback.snd _ _, fun y ↦ ?_, ⟨pullback.fst _ _⟩,
      ULift.ext _ _ <| pullback.condition _ _⟩

Goal state after:
X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)
y : (fun X ↦ ↑X.toTop) S
⊢ ∃ a, (ConcreteCategory.hom (pullback.snd f g.down)) a = y
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: ⊢ IsClosedEmbedding ⇑natUnionInftyEmbedding

Tactic:
refine .of_continuous_injective_isClosedMap
    natUnionInftyEmbedding.continuous ?_ ?_

Goal state after:
case refine_1
⊢ Function.Injective ⇑natUnionInftyEmbedding

case refine_2
⊢ IsClosedMap ⇑natUnionInftyEmbedding
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op)

Tactic:
simp only [Nat.succ_eq_add_one, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.ofOpSequence_map_homOfLE_succ]

Goal state after:
n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi (functorMap f n)
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
⊢ ∀ {Y : Type (u + 1)} [tY : TopologicalSpace Y] (f : ↑X.toTopCat → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)) → Continuous f

Tactic:
intro Y

Goal state after:
X✝ X : CondensedSet
Y : Type (u + 1)
⊢ ∀ [tY : TopologicalSpace Y] (f : ↑X.toTopCat → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, ↑X.toTopCat)), Continuous (f ∘ ⇑g)) → Continuous f
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs

Tactic:
have eq₁ : v = Fin2.elim0 := by funext i; contradiction

Goal state after:
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = ↑n
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x

Tactic:
rw [← h, Option.some_injective _ hn'.symm]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ f X

Tactic:
apply f.monotone i_ih

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.rangeIcc g).support ⊆ f.support ∪ g.support

Tactic:
intro x hx
  by_contra h
  refine notMem_support_iff.2 ?_ hx
  rw [rangeIcc_apply, notMem_support_iff.1 (notMem_mono subset_union_left h),
    notMem_support_iff.1 (notMem_mono subset_union_right h)]
  exact Icc_self _

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin 1
⊢ take 1 ⋯ v i = v (castLE ⋯ i)

Tactic:
simp only [take]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ take (n + m) ⋯ (fun i ↦ addCases u v i) i = addCases u (take m h v) i

Tactic:
simp only [take, addCases, val_castLE]

Goal state after:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
⊢ lookup x s₁ = lookup x s₂

Tactic:
· rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
hd : Sigma β
l₁✝ l₂✝ : List (Sigma β)
a✝ : l₁✝ ~ l₂✝
ih : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
l : List (Sigma β)
⊢ (hd :: l₁✝).kunion l ~ (hd :: l₂✝).kunion l

Tactic:
simp [ih (List.kerase _ _)]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
⊢ s.sum.support = (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn with | _ a

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a : List (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a ≤ ↑y ∧ ↑y < ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Tactic:
exact_mod_cast h

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a < ↑y ∧ ↑y ≤ ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Tactic:
exact_mod_cast h

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l <:+ l

Tactic:
by
  rw [← reverse_prefix, rtakeWhile, reverse_reverse]
  exact takeWhile_prefix _

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
rw [rtakeWhile, mem_reverse] at hx
  exact mem_takeWhile_imp hx

Goal state after:
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
x✝ : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)

Tactic:
cases tl with
    | nil =>
      simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append]
      exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }

Goal state after:
Module: Mathlib.Data.List.Sections

Goal state before:
pp: α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L

case refine_2
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (i + 1) (sz.splitLengths l) = (take (i + 1) sz).splitLengths l

Tactic:
cases sz
    · simp
    · simp only [splitLengths_cons, take_succ_cons, hi]

Goal state after:
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : (head :: tail).sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [sum_cons] at h

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
⊢ a = 0

Tactic:
inhabit n
    ext i j
    classical
    replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
    simpa using Matrix.ext_iff.2 h i default

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1

Tactic:
Finset.card_Ioc_eq_card_Icc_sub_one,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) - 1 = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ M → Acc LT.lt x
⊢ Acc OneStep M

Tactic:
induction M using Multiset.induction_on with

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a✝ : ℚ≥0
h : a✝ < 0
⊢ ⌊↑a✝⌋₊ = 0

Tactic:
simpa using h.trans zero_lt_one

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD
    ↑p]

Tactic:
by
    rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]
    gcongr
    apply choose_modEq_choose_mod_mul_choose_div.trans
    simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]

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

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

Tactic:
exact_mod_cast h

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

Goal state before:
pp: n p : ℕ
inst✝ : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), n.choose i ≡ 0 [MOD p]
⊢ ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]

Tactic:
exact_mod_cast h

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

Goal state before:
pp: n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if ↑n < ↑(k.bit1 * k.bit1) then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
simp only [cast_lt, dvd_to_nat]

Goal state after:
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if n < k.bit1 * k.bit1 then ↑n else if k.bit1 ∣ n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (↑q + ↑q + 1) = ↑n

Tactic:
add_comm _ 1,

Goal state after:
case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (1 + (↑q + ↑q)) = ↑n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mk.mk
F : PFunctor.{uA, uB}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }

Tactic:
congr with n

Goal state after:
case mk.mk
F : PFunctor.{uA, uB}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
n : ℕ
⊢ approx✝¹ n = approx✝ n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a, i⟩ :: xs) x → IsPath xs (f i)

Tactic:
rintro (_ | ⟨_, _, _, _, rfl, hp⟩)

Goal state after:
case cons
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f✝ : F.B a → F.M
hp : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f✝⟩
⊢ IsPath xs (f i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := ⋯ } = { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }

Tactic:
congr with n

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.balance' x r).Sized

Tactic:
by
  unfold Ordnode.balance'; split_ifs
  · exact hl.node' hr
  · exact hl.rotateL hr
  · exact hl.rotateR hr
  · exact hl.node' hr

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

Goal state before:
pp: case nil.node.node.nil
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rll.size = 0 ∧ rlr.size = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then nil.node' x ((node rls rll rlx rlr).node' rx nil)
    else nil.rotateL x ((node rls rll rlx rlr).node' rx nil)

Tactic:
cases sr.2.1.2.1.size_eq_zero.1 this.1

Goal state after:
case nil.node.node.nil.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rlx : α
rlr : Ordnode α
hr : ((node rls nil rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls nil rlx rlr) rx nil).Sized
this : nil.size = 0 ∧ rlr.size = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then nil.node' x ((node rls nil rlx rlr).node' rx nil)
    else nil.rotateL x ((node rls nil rlx rlr).node' rx nil)
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ n < PNat.find h₂ + 1 → ¬p n

Tactic:
induction n with
  | one => simp [h1]
  | succ m _ =>
    intro hm
    simp only [add_lt_add_iff_right, lt_find_iff] at hm
    exact hm _ le_rfl

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

Goal state before:
pp: u v : PrimeMultiset
h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := PNat.factorMultiset_le_iff'
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
rw [u.factorMultiset_prod] at h

Goal state after:
u v : PrimeMultiset
h : u ≤ v ↔ u.prod ∣ v.prod
⊢ u.prod ∣ v.prod ↔ u ≤ v
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : (P F).B a' ⟹ α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f' i✝ '' univ

Tactic:
rw [← h _ _ _ _ e.symm]

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : (P F).B a' ⟹ α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f i✝ '' univ
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
suffices H : _ by
        refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
⊢ (∃ l', Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ r', Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := ⋯
x y : Cofix F α
rxy : r x y
⊢ r x y

Tactic:
exact rxy

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map]

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x
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 : F (α ::: Cofix F α)
⊢ (mk x).dest = x

Tactic:
by
  have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
  rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
    appendFun_id_id, MvFunctor.id_map]

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

Goal state before:
pp: case a
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := ⋯
x y : Cofix F
rxy : r x y
⊢ r x y

Tactic:
exact rxy

Goal state after: