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

Goal state before:
pp: case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x : ↑(toProfinite.obj (F.obj k)).toTop
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map ki)).hom) g } fi) x =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map kj)).hom) g } fj) x

Tactic:
obtain ⟨x, hx⟩ := ((Profinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x

Goal state after:
case refine_2
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
i j : I
fi : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : I
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toProfinite.obj (F.obj k)).toTop
x : ↑(((const I).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map ki)).hom) g } fi) x✝ =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map kj)).hom) g } fj) x✝
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
x✝³ x✝² : CompHausᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ (ConcreteCategory.hom
          (X.obj.map x✝¹ ≫
            ↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ })).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ }) ≫
            X.toTopCat.toCondensedSet.obj.map x✝¹)).toFun
      x✝

Tactic:
simp only [TypeCat.Fun.toFun_apply,
        comp_apply, TopCat.toSheafCompHausLike_obj_map, ConcreteCategory.hom_ofHom,
        TypeCat.Fun.coe_mk, ← Functor.map_comp_apply]

Goal state after:
X✝ X : CondensedSet
x✝³ x✝² : CompHausᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (x✝¹ ≫ (CompHausLike.const (of PUnit.{u + 1}) s).op))) x✝,
      continuous_toFun := ⋯ } =
    (ConcreteCategory.hom (↾fun g ↦ g.comp (TopCat.Hom.hom x✝¹.unop.hom)))
      { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x✝,
        continuous_toFun := ⋯ }
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : 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
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
⊢ ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f (Nat.succ 0) x'

Tactic:
intro x' _

Goal state after:
case zero
α : 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
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = Fix.approx f (Nat.succ 0) 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 + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
⊢ ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'

Tactic:
intro x' _

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 + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ hwf✝.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

Tactic:
rcases le_total i j with H | H <;> [skip; symm]

Goal state after:
case pos.mpr.inr.inl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b

case pos.mpr.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b = y
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun

Tactic:
by
  ext i : 1; cases i

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)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ b ∈ Part.fix (⇑f) a

Tactic:
rw [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.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x

Tactic:
exists equiv x

Goal state after:
α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = ⟨a, b⟩ :: s.entries

Tactic:
entries_insert,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ ⟨a, b⟩ :: kerase a s.entries = ⟨a, b⟩ :: s.entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := c :: l, nodupKeys := ⋯ } ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
cases c

Goal state after:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y

Tactic:
congr 2

Goal state after:
case e_a.e_a
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l ↦ ↑(a :: b :: l)) = fun a b l ↦ ↑(a :: b :: l)
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s

Tactic:
simp_rw [seq_def, fmap_def]

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ u.sup fun f ↦ image f (t.sup fun f ↦ image f s)) ↔
    a ∈ ((image comp u).sup fun f ↦ image f t).sup fun f ↦ image f s
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
ih : tl.NodupKeys → ¬hd.fst ∈ (kerase hd.fst tl).keys
⊢ ¬hd.fst ∈ (kerase hd.fst (hd :: tl)).keys

Tactic:
simp [nd.1]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.support ↔ f x ≠ 0

Tactic:
mem_support_iff

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ f x ≠ 0 ↔ f x ≠ 0
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + -g).support = (f - g).support

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + -g).support = (f + -g).support
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#(Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)) = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0

Tactic:
card_Ico,

Goal state after:
a b r : ℤ
hr : 0 < r
⊢ ↑(⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉).toNat = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a ≤ x_1 ∧ x_1 < b) ∧ x_1 ≡ v [MOD r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
← natCast_modEq_iff

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a ≤ x_1 ∧ x_1 < b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ x_1 ≡ v [MOD r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
← natCast_modEq_iff

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ - ⌈(↑0 - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ = ?m.91

Tactic:
← sub_sub,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r) - ↑r * ↑(v / r)) / ↑r⌉ - ⌈(↑0 - ↑(v % r) - ↑r * ↑(v / r)) / ↑r⌉ = ?m.91
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)

Tactic:
convert! range'_append using 2

Goal state after:
case e'_2.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) ?convert_3

case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + ?convert_3

case convert_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ ℕ
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
apply eq_nil_iff_forall_not_mem.2
  intro a
  simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
  intro _ h₂ h₃
  exfalso
  exact not_lt_of_ge h₃ h₂

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

Goal state before:
pp: n : ℕ
⊢ Ico n (n + 1) = [n]

Tactic:
dsimp [Ico]
  simp [Nat.add_sub_cancel_left]

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

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
· rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

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
this : ∀ j < v.length - p, v[j]? = v[j + p]?
⊢ v.HasPeriod p

Tactic:
by simpa [hasPeriod_iff_getElem?]

Goal state after:
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
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.single j default 1) = 0 (Matrix.single j default 1)
⊢ a i j = 0 i j

Tactic:
simpa using Matrix.ext_iff.2 h i default

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v : n₁ ⊕ n₂ → R
⊢ A₁.fromCols A₂ *ᵥ v = A₁ *ᵥ v ∘ Sum.inl + A₂ *ᵥ v ∘ Sum.inr

Tactic:
by
  simp [← fromCols_mulVec_sumElim]

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

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

Tactic:
Nat.card_Icc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∏ x ∈ (toDFinsupp s).support ∪ (toDFinsupp t).support, ((toDFinsupp t) x + 1 - (toDFinsupp s) x) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
K : Type u_2
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Algebra K A
n : ℕ
this : IsUnit ↑n !
⊢ IsUnit ↑n !

Tactic:
simpa using this.map (algebraMap K A)

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit (↑(n + 1) * ↑n !) ↔ n + 1 < p

Tactic:
Nat.cast_commute _ _ |>.isUnit_mul_iff,

Goal state after:
case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit ↑(n + 1) ∧ IsUnit ↑n ! ↔ n + 1 < p
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l).prod

Tactic:
rw [hlp]

Goal state after:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l').prod
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
rw [Finset.mem_antidiagonal] at hk

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
⊢ p (nth p a)

Tactic:
have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']

Goal state after:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
⊢ p (nth p a)
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ cmpUsing lt a b = Ordering.gt ↔ lt b a

Tactic:
by
  simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left,
    and_iff_right_iff_imp, reduceCtorEq]
  exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

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

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

Tactic:
by rw [ZNum.bit0, cast_pos, cast_pos]; rfl

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

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

Tactic:
rw [ZNum.bit1, cast_neg, cast_neg]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
dsimp only [Num.succ'] at ep

Goal state after:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = a.succ
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
r1,

Goal state after:
case pos
α : 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 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : PosNum
⊢ -(↑a * ↑b) = ↑a * -↑b

Tactic:
neg_mul_eq_mul_neg

Goal state after:
a b : PosNum
⊢ ↑a * -↑b = ↑a * -↑b
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : ↑(const n A) α
⊢ get (f <$$> x) = get x

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)

Tactic:
simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
simp only [liftP_iff]; constructor
  · rintro ⟨_, _, ⟨⟩, _⟩
    assumption
  · intro
    repeat' first | constructor | assumption

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

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

Tactic:
unfold balanceL balanceR
  obtain - | ⟨rs, rl, rx, rr⟩ := r
  · obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
    obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;>
      dsimp only [dual, id] <;> try rfl
    split_ifs with h <;> repeat simp [add_comm]
  · obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
    dsimp only [dual, id]
    split_ifs; swap; · simp [add_comm]
    obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> try rfl
    dsimp only [dual, id]
    split_ifs with h <;> simp [add_comm]

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.Sized

Tactic:
← dual_dual t

Goal state after:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ x ∈ t.toList

Tactic:
unfold Emem; induction t <;> simp [Any, *]

Goal state after:
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
this :
  (r.size = 0 → l.size ≤ 1) →
    (1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size) →
      2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 → Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
exact this H₁ H₂ H₃

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

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

Tactic:
rintro (⟨i, a, hji⟩ | ⟨i, hba⟩)

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hab : ⟨a₂✝, a⟩ < ⟨a₁✝, i⟩
⊢ False

case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : ⟨i, b₂✝⟩ < ⟨i, b₁✝⟩
⊢ False