mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x)).hom

Tactic:
hx,

Goal state after:
R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
          ((coherentTopology LightProfinite).yonedaEquiv
            (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p)))).hom
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
constructor <;> intros <;>
    simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
  · simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]; rfl
  · dsimp only [bicompr]
    simp [naturality, binaturality']

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝

Tactic:
(conv_rhs => rw [← ih])

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = (toList xs).length

Tactic:
unfold length
  rw [foldl_toList]
  generalize toList xs = ys
  rw [← Nat.add_zero ys.length]
  generalize 0 = n
  induction ys generalizing n with
  | nil => simp
  | cons _ _ ih => simp +arith [ih]

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

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
have := S'_compactSpace π (by fun_prop)

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
by
  rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → DecidableEq (α i)
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), IsBotZeroClass (α i)
inst✝¹ : (i : ι) → OrderBot (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
by
  simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x *> y = Function.const α id <$> x <*> y

Tactic:
by intros; ext; simp [Seq.seq, SeqRight.seqRight]

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

Goal state before:
pp: n : ℕ
p : Fin n → Type u
τ : Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih => exact funext (ih <| f ·)

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : ¬k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
· simp_all [lookup_insert_ne h]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → x ∈ f.neLocus g

Tactic:
by simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs

Tactic:
by
  apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
  rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]

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

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ a ^^^ b = b

Tactic:
LawfulXor.xor_self,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ 0 ^^^ b = b
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ (b ^^^ b) = a

Tactic:
LawfulXor.xor_self,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ 0 = a
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ Function.IsFixedPt (fun x ↦ x ^^^ a) b ↔ a = 0

Tactic:
rw [xor_right_eq, isFixedPt_xor_left_iff]

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

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x < b) ∧ r ∣ x - v

Tactic:
sub_le_sub_iff_right

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

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a < x ∧ x - v ≤ b - v) ∧ r ∣ x - v

Tactic:
sub_le_sub_iff_right

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

Goal state before:
pp: a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#({x ∈ Ioc a b | x ≡ v [MOD r]})) = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0

Tactic:
by
  simp_rw [← Ioc_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ioc_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

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

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ↑(v % r) < ↑r + ↑(b % r) ∧ ↑(b % r) ≤ ↑(v % r)

Tactic:
← cast_add,

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ↑(v % r) < ↑(r + b % r) ∧ ↑(b % r) ≤ ↑(v % r)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse

Tactic:
cases n
    · exact drop_length
    · simp [drop_append, IH]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l.reverse = (dropWhile p l).reverse

Tactic:
by
  simp_rw [rdropWhile, reverse_reverse]

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

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

Tactic:
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]

Goal state after:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []

α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
x✝ : hd :: hd' :: tl' ≠ []
⊢ hd' :: tl' ≠ []
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
by
  rcases le_total l m with hlm | hml
  · rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]
  · rw [eq_nil_of_le hml, filter_le_of_top_le hml]

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, cast_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ ∀ a ∈ f.support, a ^ f a ∣ a ^ n.factorization a

Tactic:
exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p

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
⊢ p ^ (multiplicity p n + 1) ∣ n

Tactic:
nth_rw 2 [hm]
    simpa [pow_add] using Nat.mul_dvd_mul_left _ (dvd_iff_mod_eq_zero.mpr (by exact_mod_cast h))

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ n.minFac ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
by
  obtain ⟨k, _, _, hn₁⟩ := (isPrimePow_nat_iff_bounded_log_minFac _).mp h
  exact dvd_gcd_iff.mpr fun i hi => by
    nth_rw 2 [hn₁]
    exact Prime.dvd_choose_pow (minFac_prime_iff.mpr h.ne_one) (by grind) (by grind)

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

Goal state before:
pp: ⊢ ↑(-0) = -↑0

Tactic:
rw [Int.cast_neg]

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

Tactic:
rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]

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

Goal state before:
pp: case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑b % ↑(pos a) ≤ ↑(pos a) * (↑b / ↑(pos a))

Tactic:
Nat.mod_lt,

Goal state after:
case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) ≤ ↑(pos a) * (↑b / ↑(pos a))

case hy
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ 0 < ↑(pos a)
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 α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, fx⟩ ∧
    ⟨ax, fy⟩ = ⟨ax, splitFun (dropFun fx) (lastFun fy)⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)

Tactic:
Hdrop,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ⟨ax, fx⟩ = ⟨ax, fx⟩ ∧
    ⟨ax, fy⟩ = ⟨ax, splitFun (dropFun fy) (lastFun fy)⟩ ∧ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
Valid'.dual_iff,

Goal state after:
α : 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₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₂ (l.balanceR x r).dual o₁
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
Valid'.dual_iff,

Goal state after:
α : 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', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (l.balanceR x r).dual o₁
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : PrimeMultiset
⊢ ↑v.prod = v.toNatMultiset.prod

Tactic:
by
  have h : (v.prod : ℕ) = ((v.map (↑) : Multiset ℕ+).map (↑)).prod :=
    PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
  simpa [Multiset.map_map] using! h

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
⊢ nil.rotateL x ((node rls rll rlx rlr).node' 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:
rotateL

Goal state after:
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))

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.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

Tactic:
exact inf_le_left

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

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

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
obtain ⟨j, h⟩ := exists_gt i

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, ⟨i, a⟩ < b
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioc a b) = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
by
  rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) → ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

Tactic:
intro h a f haf
    have : Liftp (fun u => u ∈ f '' univ) x := by
      rw [liftp_iff]
      exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
    exact h this

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s : WSeq α
⊢ LiftRel R s s

Tactic:
refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
    rw [← h]
    apply Computation.LiftRel.refl _ |>.refl

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (fun x ↦ Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = tail.aux

Tactic:
ext1 (_ | ⟨a, s⟩)

Goal state after:
case none
α : Type u
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd none) >>= destruct = tail.aux none

case some
α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd (some (a, s))) >>= destruct = tail.aux (some (a, s))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a a' : α
s' : WSeq α
⊢ some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
by
  generalize e : destruct s = c
  intro h
  revert s
  apply Computation.memRecOn h <;> [skip; intro c IH] <;> intro s m <;>
    induction s using WSeq.recOn <;>
    have := congr_arg Computation.destruct m
  case h1.nil | h1.think | h2.nil | h2.cons => simp at this
  case h2.think => simp at this; simp [IH this]
  case h1.cons =>
    simp only [destruct_cons, destruct_pure, Sum.inl.injEq, Option.some.injEq,
      Prod.mk.injEq] at this
    obtain ⟨i1, i2⟩ := this
    rw [i1, i2]
    dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]
    have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
    rw [h_a_eq_a']
    refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
    rcases o with e | m
    · rw [e]
      apply Stream'.mem_cons
    · exact Stream'.mem_cons_of_mem _ m

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

Goal state before:
pp: case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think

Tactic:
case succ.think n IH s =>
    simp only [tail_think, mem_think] at m e ⊢
    apply IH m
    rw [e]
    cases tail s
    rfl

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

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

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
obtain ⟨j, h⟩ := exists_gt i

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, ⟨i, a⟩ < b