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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightProfinite
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S' ⊗ P).toCondensed ⟶ A
hh :
  (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
      (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g =
    g' ≫ e
⊢ (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g =
    (free R).map (μIso lightProfiniteToLightCondSet S' P).hom ≫
      (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫
        (free R).map (μIso lightProfiniteToLightCondSet S P).inv ≫ g

Tactic:
simp [-map_comp, ← map_comp_assoc, ← μ_natural_left_assoc]

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

Goal state before:
pp: case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ tsnd (pure ∘ f✝) x✝ = pure (f✝ <$> x✝)

pp: case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ η✝.app (t α β✝) (tsnd f✝ x✝) = tsnd (η✝.app β✝ ∘ f✝) x✝

Tactic:
· simp [tsnd_eq_snd_id, (· <$> ·)]

Goal state after:
case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ η✝.app (t α β✝) (tsnd f✝ x✝) = tsnd (η✝.app β✝ ∘ f✝) x✝
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝

Tactic:
assert_pos hh,

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ hwf✝.fix (fixAux f) (z.succ hh) x✝ = Fix.approx f (n + 1) x✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (⇑f) i ≤ approx (⇑f) j

Tactic:
by
  induction j with
  | zero => cases hij; exact le_rfl
  | succ j ih =>
    cases hij; · exact le_rfl
    exact le_trans (ih ‹_›) (approx_mono' f)

Goal state after:
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'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs

Tactic:
have eq₃ : fs = nilFun := 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
eq₂ : v' = Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ b ∈ Part.fix (⇑f) a

Tactic:
mem_iff f

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ ∃ i, b ∈ approx (⇑f) i a
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 x : Π₀ (i : ι), α i
⊢ x ∈ (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g) ↔ f ≤ x ∧ x ≤ g

Tactic:
refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_
      simp_rw [mem_rangeIcc_apply_iff, forall_and]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toDFinsupp {a} = DFinsupp.single a 1

Tactic:
rw [← replicate_one, toDFinsupp_replicate]

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:
simp [Iic_eq_Icc, card_Icc, bot_eq_zero]

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).toNat = ∑ a ∈ s, (f a).toNat

Tactic:
rw [← natCast_inj, natCast_toNat (sum_ne_top.2 hf), Nat.cast_sum]
  exact sum_congr rfl fun x hx => (natCast_toNat (hf x hx)).symm

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

Goal state before:
pp: C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1

Tactic:
rw [add_sub_assoc]

Goal state after:
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)

Tactic:
apply le_add_of_nonneg_right

Goal state after:
C : FloatCfg
⊢ 0 ≤ ↑prec - 1
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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
⊢ Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop

Tactic:
obtain ⟨x, hx⟩ := (.comp ((fun y ↦ ⟨(Nonempty.some inferInstance, y), rfl⟩))
        ((LightProfinite.epi_iff_surjective _).mp hπ') : ((snd S' ℕ∪{∞}) ∘ π').Surjective) ∞

Goal state after:
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
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
· have : castLE h j ≠ castLE h i := by simp [h']
    simp only [take, update_of_ne h', update_of_ne this]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ List.idxOf x xs < xs.length

Tactic:
rw [List.idxOf_lt_length_iff]; apply h

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

Goal state before:
pp: α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ lookmap f (a :: l) = b :: l

Tactic:
by
  simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]
  rw [h]

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

Goal state before:
pp: α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
    rcases h : g a with - | b
    · simp [h, H₁.trans h, lookmap_congr H₂]
    · simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂

Tactic:
← lookup_isSome,

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ (lookup k s₂).isSome = true
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace a b s ↔ a' ∈ s

Tactic:
by
  rw [mem_keys, keys_replace, ← mem_keys]

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

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise Disjoint (map keys L)

Tactic:
pairwise_map

Goal state after:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ Prod.map id AList.toFinmap (AList.extract a s₁) = Prod.map id AList.toFinmap (AList.extract a s₂)

Tactic:
simp [perm_lookup p, toFinmap_eq, perm_erase p]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i).sup (f i) ⊓ (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert i s).attach.inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)

Tactic:
attach_insert,

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i).sup (f i) ⊓ (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support

Tactic:
simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]
  induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

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

Goal state before:
pp: case e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a)).sup = List.foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ a

Tactic:
simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]

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

Goal state before:
pp: x a : ℤ
⊢ (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a)) =
    (-1) ^ x.natAbs * fib a ^ 2

Tactic:
grind [fib_succ_mul_fib_pred_sub_fib_sq, fib_add_two]

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b a : α
⊢ f (foldl f a []) b = f a (foldr f b [])

Tactic:
simp [*, ha.assoc]

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

Goal state before:
pp: case cons
α : Type u_1
l : List α
f : α → α → α
ha : Std.Associative f
b head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α}, f (foldl f a tail✝) b = f a (foldr f b tail✝)
a : α
⊢ f (foldl f a (head✝ :: tail✝)) b = f a (foldr f b (head✝ :: tail✝))

Tactic:
simp [*, ha.assoc]

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

Goal state before:
pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) []

Tactic:
exact .nil

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ v[j + u.length + p - u.length]? = v[j + p]?

Tactic:
exact congrArg (getElem? v) eq

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

Goal state before:
pp: case h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((a :: g).reverse :: gs)

Tactic:
rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩

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

Goal state before:
pp: case neg
α : 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_in : ¬z ∈ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
⊢ { k // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }

Tactic:
have ih := chineseRemainderOfList l co.of_cons

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
⊢ { k // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ {n ∈ range (nth p (k + 1)) | p n}
⊢ a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n}

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -(↑p + ↑p) = -↑p + -↑p

Tactic:
neg_add_rev

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑p + -↑p = -↑p + -↑p
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
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : R x y
⊢ ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
specialize h _ _ Hr

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 α
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
Hr : R x y
⊢ ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * l.size < r.size
H3 : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.rotateL x r) o₂

Tactic:
by
  obtain - | ⟨rs, rl, rx, rr⟩ := r; · cases H2
  rw [hr.2.size_eq, Nat.lt_succ_iff] at H2
  rw [hr.2.size_eq] at H3
  replace H3 : 2 * (size rl + size rr) ≤ 9 * size l + 3 ∨ size rl + size rr ≤ 2 :=
    H3.imp (@Nat.le_of_add_le_add_right _ 2 _) Nat.le_of_succ_le_succ
  have H3_0 (l0 : size l = 0) : size rl + size rr ≤ 2 := by lia
  have H3p : size l > 0 → 2 * (size rl + size rr) ≤ 9 * size l + 3 := fun l0 : 1 ≤ size l =>
    (or_iff_left_of_imp <| by lia).1 H3
  have ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1 := by lia
  have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb =>
    absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide)
  rw [Ordnode.rotateL_node]; split_ifs with h
  · have rr0 : size rr > 0 :=
      (mul_lt_mul_iff_right₀ (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _)
    suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by
      exact hl.node3L hr.left hr.right this.1 this.2
    rcases Nat.eq_zero_or_pos (size l) with l0 | l0
    · rw [l0]; replace H3 := H3_0 l0
      have := hr.3.1
      rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
      · rw [rl0] at this ⊢
        rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]
        decide
      have rr1 : size rr = 1 := le_antisymm (ablem rl0 H3) rr0
      rw [add_comm] at H3
      rw [rr1, show size rl = 1 from le_antisymm (ablem rr0 H3) rl0]
      decide
    replace H3 := H3p l0
    rcases hr.3.1.resolve_left (hlp l0) with ⟨_, hb₂⟩
    refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
    · exact Valid'.rotateL_lemma₁ H2 hb₂
    · exact Nat.le_of_lt_succ (Valid'.rotateL_lemma₂ H3 h)
    · exact Valid'.rotateL_lemma₃ H2 h
    · exact
        le_trans hb₂
          (Nat.mul_le_mul_left _ <| le_trans (Nat.le_add_left _ _) (Nat.le_add_right _ _))
  · rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
    · rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h
      replace h := h.resolve_left (by decide)
      rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2
      rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1
      cases H1 (by decide)
    refine hl.node4L hr.left hr.right rl0 ?_
    rcases Nat.eq_zero_or_pos (size l) with l0 | l0
    · replace H3 := H3_0 l0
      rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
      · have := hr.3.1
        rw [rr0] at this
        exact Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩
      exact Or.inl ⟨l0, le_antisymm (ablem rr0 <| by rwa [add_comm]) rl0, ablem rl0 H3⟩
    exact
      Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

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

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = (↑l).prod
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Goal state after:
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(ofNatMultiset (↑l) h).prod = l.prod
⊢ ↑(ofNatList l h).prod = l.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l) h).prod = (↑l).prod
⊢ (ofPNatList l h).prod = l.prod

Tactic:
rw [Multiset.prod_coe] at this

Goal state after:
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → p.Prime
this : (ofPNatMultiset (↑l) h).prod = l.prod
⊢ (ofPNatList l h).prod = l.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod ∣ n

Tactic:
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod

Goal state after:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset

Tactic:
exact le_self_add

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

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

Tactic:
· exact dvd_lcm_right m n

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

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m

Tactic:
have : v = m.factorMultiset := v.factorMultiset_prod.symm

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊓ v).prod = n.gcd m