mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : ↑x ∈ ↑b
⊢ ↑↑x ∈ ↑(Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))

Tactic:
simp only [sigmaIncl, ContinuousMap.coe_mk, Fiber.mem_iff_eq_image, comp_apply] at this

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ ↑↑x ∈ ↑(Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by
  let S := f.discreteQuotient
  let ff : S → α := f.lift
  cases isEmpty_or_nonempty S
  · suffices ∃ j, IsEmpty (F.obj j) by
      refine this.imp fun j hj => ?_
      refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
      · convert! isOpen_empty
        ext x
        exact hj.elim x
      · ext x
        exact hj.elim' (C.π.app j x)
    by_contra! h
    have : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
    have : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : T2Space (F.obj j))
    have : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : CompactSpace (F.obj j))
    have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u}
      (F ⋙ Profinite.toTopCat)
    suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)
    let D := Profinite.toTopCat.mapCone C
    have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
    have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
    exact cond.map CD
  · let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩
    obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'
    refine ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩
    ext1 t
    apply_fun fun e => e t at hj
    dsimp at hj ⊢
    rw [← hj]
    rfl

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ map (⇑f) 1 = 1

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x + y) = map (⇑f) x + map (⇑f) y

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (m : R) (x : LocallyConstant X Y), map (⇑f) (m • x) = (RingHom.id R) m • map (⇑f) x

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring Y
inst✝² : Algebra R Y
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : Y →ₐ[R] Z
x✝ : R
⊢ (↑↑(mapRingHom ↑f)).toFun ((algebraMap R (LocallyConstant X Y)) x✝) = (algebraMap R (LocallyConstant X Z)) x✝

Tactic:
by aesop

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
by aesop

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
⊢ ∀ (t : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}) (j : ↑X.toTop),
    (fintypeCatAsCofan X).inj j ≫
        ConcreteCategory.ofHom { toFun := fun x ↦ (ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ } =
      t.inj j

Tactic:
by aesop

Goal state after:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (Opposite.op 0))

Tactic:
apply Functor.epi_of_epi_map (forget R)
  change Epi (((forget R).mapCone c).π.app ⟨0⟩)
  apply coherentTopology.epi_π_app_zero_of_epi
  · simp only [LightProfinite.effectiveEpi_iff_surjective]
    exact fun x h ↦ Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit x) h
  · have := (freeForgetAdjunction R).isRightAdjoint
    exact isLimitOfPreserves _ hc
  · exact fun _ ↦ (forget R).map_epi _

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)

Tactic:
by
  induction x <;> simp! [*, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
by
  induction x <;> simp! [*, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ofFin i.toFin = i

Tactic:
induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv (pure ∘ x✝¹) x✝ = pure (x✝¹ <$> x✝)

Tactic:
Equiv.traverse_eq_map_id,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ pure (Equiv.map eqv x✝¹ x✝) = pure (x✝¹ <$> x✝)
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)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ (f.rangeIcc g) x = 0

Tactic:
rw [rangeIcc_apply, notMem_support_iff.1 (notMem_mono subset_union_left h),
    notMem_support_iff.1 (notMem_mono subset_union_right h)]

Goal state after:
ι : 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)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ Icc 0 0 = 0
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a : α
h : ∃ a_1, (fun x ↦ a_1 = x) = ↑(mk a) := (mk a).property
⊢ Classical.choose h = a

Tactic:
have := Classical.choose_spec h

Goal state after:
α : Sort u_1
a : α
h : ∃ a_1, (fun x ↦ a_1 = x) = ↑(mk a) := (mk a).property
this : (fun x ↦ Classical.choose h = x) = ↑(mk a)
⊢ Classical.choose h = a
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
⊢ ⨅ i, ∑ a ∈ Finset.cons a s ha, f i a = ∑ a ∈ Finset.cons a s ha, ⨅ i, f i a

Tactic:
simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a = ↑(∑ a ∈ s, (f a).toNat)

Tactic:
Nat.cast_sum

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a = ∑ x ∈ s, ↑(f x).toNat
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
exact absurd (‹_› ▸ h) (card α).lt_irrefl

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) → ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ IsMulCommutative (Perm α) → Nat.card α ≤ 2

Tactic:
rintro ⟨⟨h⟩⟩

Goal state after:
α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ Nat.card α ≤ 2
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ∀ (x y : ↑(S' ⊗ ℕ∪{∞}).toTop), h.elim x = h.elim y

Tactic:
by aesop

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ (s :: tail✝).keys
⊢ dlookup a ((s :: tail✝).kunion l₂) = dlookup a (s :: tail✝)

Tactic:
simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑i) * fib (-(↑(i + 1) + 1)) + -fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs

Tactic:
fib_neg,

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    (-1) ^ (-↑(i + 1)).natAbs
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt b ↔ a * a ≤ b

Tactic:
by
  rw [← abs_mul_abs_self, eq_natCast_toNat.mpr hn, eq_natCast_toNat.mpr (abs_nonneg a),
    Int.sqrt_natCast, ← Int.natCast_mul, Nat.cast_le, Nat.cast_le, Nat.le_sqrt]

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

Goal state before:
pp: case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
intro ⟨rfl, rfl⟩
    exact ⟨emod_add_mul_ediv a b, emod_nonneg _ h, emod_lt_abs _ h⟩

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ (match m, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    m.mul ↑(Nat.pow 2 n)

Tactic:
cases m <;> simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]

Goal state after:
case ofNat
n a✝ : ℕ
⊢ ↑a✝ <<< n = ↑a✝ * 2 ^ n

case negSucc
n a✝ : ℕ
⊢ -[Nat.shiftLeft' true a✝ n+1] = -[a✝+1] * 2 ^ n
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_4.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy

Goal state after:
case refine_4.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr.empty
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
hN : ∀ (x : α), x ∈ 0 → x < a
⊢ Acc OneStep (M + 0)

Tactic:
simpa using .intro _ hM

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p * q⁻¹).toNNRat = p.toNNRat * q.toNNRat⁻¹

Tactic:
← toNNRat_inv,

Goal state after:
p q : ℚ
hp : 0 ≤ p
⊢ (p * q⁻¹).toNNRat = p.toNNRat * q⁻¹.toNNRat
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
by
  rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]

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

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iio n.factorization).attach

Tactic:
rw [Finset.map_eq_image]
  change _ = (Finset.Iio n.factorization).attach.image ((·.prod (· ^ ·)) ∘ Subtype.val)
  rw [← Finset.image_image, Finset.attach_image_val]
  exact properDivisors_eq_image_Iio_factorization_prod_pow

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: 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])
⊢ fib a + fib (a - 1) ≤ fib n

Tactic:
by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)

Goal state after:
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) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ fib a + (map fib l).sum < fib n

Tactic:
← List.sum_cons,

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])
ha : 0 < a
n : ℕ
hn : a < n
x✝ : n ≤ (map fib l).sum + (fib a + 1)
⊢ (fib a :: map fib l).sum < fib n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
rcases hn with ⟨hf, hn⟩
    rw [nth_of_card_le _ hn]
    refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm
    rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
    exact (hk.2 _ ((hlt hf).trans_le hn)).false

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

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

Tactic:
rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]

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

Goal state before:
pp: m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
← not_lt

Goal state after:
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
← not_lt

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (↑q + ↑q) = ↑n + ↑n + 1

Tactic:
← two_mul,

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (2 * ↑q) = ↑n + ↑n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (2 * ↑q) = ↑n + ↑n + 1

Tactic:
← two_mul,

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (2 * ↑q) = 2 * ↑n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (↑q + ↑q) = ↑n + ↑n

Tactic:
← two_mul,

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (2 * ↑q) = ↑n + ↑n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (2 * ↑q) = ↑n + ↑n

Tactic:
← two_mul,

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (2 * ↑q) = 2 * ↑n
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
PFunctor.M.dest_corec

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b

Tactic:
PFunctor.M.dest_corec

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : (PFunctor.M.corec (fun b ↦ ⟨g₀ b, g₂ b⟩) b).dest = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
PFunctor.M.dest_corec

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x✝ : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' : P.last.map (PFunctor.M.corec fun b ↦ ⟨g₀ b, g₂ b⟩) ⟨g₀ b, g₂ b⟩ = ⟨a, f⟩
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (y.approx (i + 1))

Tactic:
i_ih

Goal state after:
case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (y.approx i) (y.approx (i + 1))
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
⊢ (node size✝ (node sz l' y r') x r).eraseMin.dual = (node size✝ (node sz l' y r') x r).dual.eraseMax

Tactic:
rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]

Goal state after: