mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := ⋯
next : (n : ℕ) → lifts n → lifts (n + 1) := ⋯
k_seq : (n : ℕ) → lifts n := ⋯
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := ⋯
⊢ ∀ (j : ℕᵒᵖ), g ≫ (lightToProfinite.mapCone S.asLimitCone).π.app j = (k_cone.extend f).π.app j

Tactic:
intro n

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
n : ℕᵒᵖ
⊢ g ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n = (k_cone.extend f).π.app n
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := ⋯
next : (n : ℕ) → lifts n → lifts (n + 1) := ⋯
k_seq : (n : ℕ) → lifts n := ⋯
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := ⋯
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
⊢ ∀ (j : ℕᵒᵖ),
    (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫
        (lightToProfinite.mapCone S.asLimitCone).π.app j =
      (k_cone.extend f).π.app j

Tactic:
intro n

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
n : ℕᵒᵖ
⊢ (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n =
    (k_cone.extend f).π.app n
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = pure (bimap f✝ f'✝ x✝)

pp: case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
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✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
· simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]; rfl

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
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✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Tactic:
simp only [foldMap, traverse_map, Function.comp_def]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Tactic:
by
  simp only [foldMap, traverse_map, Function.comp_def]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
induction n <;> rfl

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
⊢ ∀ (e : X ⟶ Y) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e

Tactic:
p

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
⊢ ∀ [Epi p] (S : LightProfinite) (g : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ p
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s

Tactic:
rcases s with ⟨⟨a⟩, h⟩; exact H ⟨a, h⟩

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
have : x ∉ singleton a b := by rwa [mem_singleton]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
· rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

Goal state after:
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).neLocus (-g) = f.neLocus (-g)

Tactic:
neg_neg

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

Goal state before:
pp: m n : ℤ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
rcases m with m | m <;>
  rcases n with n | n <;>
  simp only [ofNat_eq_natCast, ofNat_add_negSucc, negSucc_add_ofNat,
             negSucc_add_negSucc, bodd_subNatNat, ← Nat.cast_add]

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (↑(m + n)).bodd = ((↑m).bodd ^^ (↑n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (m.bodd ^^ n.succ.bodd) = ((↑m).bodd ^^ -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ (↑n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ -[(m + n).succ+1].bodd = (-[m+1].bodd ^^ -[n+1].bodd)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x

Tactic:
rwa [zero_add, add_zero] at h'

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

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ (↑a - ↑b).natAbs ≤ n

Tactic:
rw [← Nat.cast_le (α := ℤ), natCast_natAbs]

Goal state after:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise (fun x y ↦ f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise (fun x y ↦ !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) y) m n))

Tactic:
by_cases h : f true false <;> simp +decide [h]

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

Goal state before:
pp: m n : ℤ
⊢ m <<< (- -n) = m <<< n

Tactic:
neg_neg

Goal state after:
m n : ℤ
⊢ m <<< n = m <<< n
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true

Tactic:
by
     simp only [decide_eq_true_eq, not_lt]
     apply le_trans hln
     exact (mem.1 hk).1

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k ↦ l.insertIdx k x) {n | n ≤ l.length}

Tactic:
intro n

Goal state after:
α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
⊢ n ∈ {n | n ≤ l.length} →
    ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {n | n ≤ l.length} → (fun k ↦ l.insertIdx k x) n = (fun k ↦ l.insertIdx k x) x₂ → n = x₂
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
exact le_trans hln (mem.1 hk).1

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (take (i + 1) (sz.splitLengths l))[i].length = sz[i]

Tactic:
simp only [take_splitLength]

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ ((take (i + 1) sz).splitLengths l)[i].length = sz[i]
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
⊢ w[i % p]? = w[i]?

Tactic:
by_cases p_zero : p = 0

Goal state after:
case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i % p]? = w[i]?

case neg
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l)

Tactic:
cases l with
  | nil => exact isChain_nil
  | cons _ _ =>
    apply isChain_getLast_head_splitByLoop _ not_mem_nil isChain_nil
    rintro _ ⟨⟩

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬[] ∈ a :: l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l

Tactic:
| cons a l IH =>

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
⊢ fromCols 0 0 = 0

Tactic:
by
  ext _ (_ | _) <;> simp

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

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ

Tactic:
by
  ext _ (_ | _) <;> simp

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

Goal state before:
pp: α : 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₂
⊢ count z Y₂ < count z Z₁

Tactic:
count_eq_zero_of_notMem z_in,

Goal state after:
α : 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₂
⊢ 0 < count z Z₁
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
simpa [hy.2] using hYZ y (by simp_all)

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
n : ℕ
⊢ nth p n = ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)

Tactic:
by rw [nth, dif_neg hf]

Goal state after:
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
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p (nth p a)

Tactic:
ha0

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
hb0 : nth p b = 0
⊢ p 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (f '' {i | p (f i)})

Tactic:
← hf.monotone.map_csInf

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = f (sInf {i | p (f i)})

p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ {i | p (f i)}.Nonempty
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) =
    sInf (f '' {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

Tactic:
← hf.monotone.map_csInf

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) =
    f (sInf {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty
Module: Mathlib.Data.Nat.Nth

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

Tactic:
intro a ha
  simp only [mem_insert, mem_filter, mem_range] at ha ⊢
  exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : a < a
⊢ False

Tactic:
lt_self_iff_false

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : False
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p n = n

Tactic:
← count_of_forall (hp · ·.le),

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p (count p n) = n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]

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

Goal state before:
pp: d n : PosNum
⊢ ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2

Tactic:
rw [Nat.div_mod_unique (PosNum.cast_pos _)]

Goal state after:
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ ∀ (n : ℕ), head' (x n.succ) = head' (x 1)

Tactic:
intro n

Goal state after:
F : PFunctor.{uA, uB}
n✝ m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
⊢ head' (x n.succ) = head' (x 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
⊢ AllAgree fun n ↦ children' (x.approx n.succ) (cast ⋯ i)

Tactic:
intro n

Goal state after:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → ↑F X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (x.approx n.succ) = head' (x.approx (succ 0))
n : ℕ
⊢ Agree ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n) ((fun n ↦ children' (x.approx n.succ) (cast ⋯ i)) n.succ)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
⊢ ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i

Tactic:
intro n

Goal state after:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ (M.mk x.dest).approx n = x.approx n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ ∀ (i_1 : ℕ), ((M.mk ⟨a, x⟩).children i).approx i_1 = (x (cast ⋯ i)).approx i_1

Tactic:
intro n

Goal state after:
F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
n : ℕ
⊢ ((M.mk ⟨a, x⟩).children i).approx n = (x (cast ⋯ i)).approx n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Emem x_1 (node size✝ l x r) ∧ P x_1

Tactic:
by simp only [Emem]; simp [Any, any_iff_exists, or_and_right, exists_or]

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

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

Tactic:
intro hm
    simp only [add_lt_add_iff_right, lt_find_iff] at hm
    exact hm _ le_rfl

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

Goal state before:
pp: a b : ℕ+
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
by
  rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]

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

Goal state before:
pp: case a
m n : ℕ+
⊢ m.lcm n ∣ (m.factorMultiset ⊔ n.factorMultiset).prod

Tactic:
apply lcm_dvd <;> rw [← factorMultiset_le_iff']

Goal state after:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

case a.hn
m n : ℕ+
⊢ n.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset