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 : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g =
    ((μIso (free R) S'.toCondensed P).hom ≫ (free R).map (lightProfiniteToLightCondSet.map π ▷ P)) ≫
      (μIso (free R) S.toCondensed P).inv ≫ g

Tactic:
← assoc

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ Part.fix ⇑f

Tactic:
intro y

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
⊢ { toFun := approx ⇑f, monotone' := ⋯ } y ≤ Part.fix ⇑f
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) →
    ∃ a ∈ s.pi t, { toFun := fun f ↦ DFinsupp.mk s fun i ↦ f ↑i ⋯, inj' := ⋯ } a = f

Tactic:
· refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
    ext i
    dsimp
    exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case neg.cons
b x : Bool
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
grind [hl.tail.two_mul_count_bool_of_even]

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

Goal state before:
pp: α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
⊢ (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys

Tactic:
by
  simp [keys]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b : β a
s : Multiset (Sigma β)
⊢ (⟨a, b⟩ ::ₘ s).keys = a ::ₘ s.keys

Tactic:
by
  simp [keys]

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
l : List ((_ : α) × β)
nd : l.NodupKeys
⊢ (map (Sigma.map f fun x ↦ id) l).NodupKeys

Tactic:
by
  induction l with
  | nil => exact nodupKeys_nil
  | cons hd tl ih =>
    simp only [map_cons, nodupKeys_cons] at nd ⊢
    exact ⟨mt (fun h => by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩) nd.1, ih nd.2⟩

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

Goal state before:
pp: case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ ∀ (a_1 : Sigma β),
    a_1 ∈ l → (if a = a_1.fst then some ⟨a, b⟩ else none) = Option.guard (fun s ↦ decide (a = s.fst)) a_1

Tactic:
rintro ⟨a', b'⟩ h'

Goal state after:
case refine_1
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
⊢ (if a = ⟨a', b'⟩.fst then some ⟨a, b⟩ else none) = Option.guard (fun s ↦ decide (a = s.fst)) ⟨a', b'⟩
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : 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:
subst a
      rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]

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

Goal state before:
pp: case insert.refine_2
α : 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 ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
this :
  f i (if hji : i = i then cast ⋯ a else g i ⋯) ⊓
      s.attach.inf ((fun i_1 ↦ f (↑i_1) (if hji : ↑i_1 = i then cast ⋯ a else g ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤
    c
⊢ (f i a ⊓ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) ≤ c

Tactic:
simpa only [cast_eq, dif_pos, Function.comp_def, Subtype.coe_mk, dif_neg, aux] using! this

Goal state after:
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ (p ^ 2).divisors = {p ^ 2, p, 1}

Tactic:
simp [divisors_prime_pow hp, range_add_one]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₁ : (s :: l₁).NodupKeys
nd₂ : l₂.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Tactic:
simp only [nodupKeys_cons] at nd₁
    simp [nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ p f

Tactic:
show f = update g i (insert x (g i)) by
      rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k k' : κ
f : ι k →₀ M
hk : k' ≠ k
i : ι k'
⊢ f.embSigma ⟨k', i⟩ = 0

Tactic:
apply embDomain_of_notMem_range
  grind

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

Goal state before:
pp: n : ℕ
⊢ (negOfNat n).bodd = n.bodd

Tactic:
by
  cases n <;> simp +decide
  rfl

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

Goal state before:
pp: a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
simpa only [Int.natAbs_neg, neg_inj] using
    natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)

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

Goal state before:
pp: b : Bool
n : ℤ
⊢ (bit b n).div2 = n

Tactic:
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
  cases b
  · decide
  · change ofNat _ = _
    rw [Nat.div_eq_of_lt] <;> simp
  · decide

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

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

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

Goal state after:
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 [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
intro y

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

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

Tactic:
· intro h; lift x to ℕ using (by omega); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

Goal state after:
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 [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
intro y

Goal state after:
case mp
a b r v : ℕ
x : ℤ
y : ℕ
⊢ ((a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]) ∧ ↑y = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
intro hk
  rw [← length_reverse] at hk
  rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
cases bs

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right' f [] [] = (map (f none) [], [])

case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right' f [] (head✝ :: tail✝) = (map (f none) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight' bs = (map (fun b ↦ (none, b)) bs, [])

Tactic:
cases bs

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipRight' [] = (map (fun b ↦ (none, b)) [], [])

case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight' (head✝ :: tail✝) = (map (fun b ↦ (none, b)) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
cases bs

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right f [] [] = map (f none) []

case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right f [] (head✝ :: tail✝) = map (f none) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = map (fun b ↦ (none, b)) bs

Tactic:
cases bs

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipRight [] = map (fun b ↦ (none, b)) []

case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = map (fun b ↦ (none, b)) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case nil
α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = ([].zipRight' bs).fst

Tactic:
cases bs

Goal state after:
case nil.nil
α : Type u
β : Type v
⊢ [].zipRight [] = ([].zipRight' []).fst

case nil.cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = ([].zipRight' (head✝ :: tail✝)).fst
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
bs : List β
⊢ (head✝ :: tail✝).zipRight bs = ((head✝ :: tail✝).zipRight' bs).fst

Tactic:
cases bs

Goal state after:
case cons.nil
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
⊢ (head✝ :: tail✝).zipRight [] = ((head✝ :: tail✝).zipRight' []).fst

case cons.cons
α : Type u
β : Type v
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), tail✝¹.zipRight bs = (tail✝¹.zipRight' bs).fst
head✝ : β
tail✝ : List β
⊢ (head✝¹ :: tail✝¹).zipRight (head✝ :: tail✝) = ((head✝¹ :: tail✝¹).zipRight' (head✝ :: tail✝)).fst
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: 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]?

Tactic:
rw [p_zero, mod_zero]

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)
⊢ ∀ (x : α), x ∈ l.flatten.head? → r (a.getLast ⋯) x = false

Tactic:
intro y

Goal state after:
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)
y : α
⊢ y ∈ l.flatten.head? → r (a.getLast ⋯) y = false
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
← head_of_mem_head? hy,

Goal state after:
case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ ((splitBy r m).head ⋯).head ⋯ ∈ m.head?
Module: Mathlib.Data.Multiset.Interval

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

Tactic:
Icc_eq,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp s) (toDFinsupp t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: p n : ℕ
hp : Prime p
hn : n < p
⊢ p.Coprime n !

Tactic:
by
  rwa [hp.coprime_iff_not_dvd, hp.dvd_factorial, not_le]

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

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : k ∈ {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
exact prod_dvd_prod_of_subset_of_dvd (support_mono hle) fun p _ ↦ Nat.pow_dvd_pow p <| hle p

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:
rw [nth, dif_neg hf]

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

Goal state before:
pp: fuel : ℕ
n k : PosNum
h : (↑n).sqrt < fuel + ↑k.bit1
⊢ ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1

Tactic:
induction fuel generalizing k <;> rw [minFacAux, Nat.minFacAux]
  case zero =>
    rw [Nat.zero_add, Nat.sqrt_lt] at h
    simp only [h, ite_true]
  case succ fuel ih =>
    simp_rw [← mul_to_nat]
    simp only [cast_lt, dvd_to_nat]
    split_ifs <;> try rfl
    rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1] <;>
      simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

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

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

Tactic:
add_eq_zero

Goal state after:
case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.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: ⊢ (ofNat' 0).toZNum = (ofNat' 0 + 1).toZNumNeg + 1

Tactic:
ofNat'_zero

Goal state after:
⊢ toZNum 0 = (0 + 1).toZNumNeg + 1
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
s₁ s₂ : F.M
ps : Path F
⊢ R s₁ s₂ →
    IsPath ps s₁ ∨ IsPath ps s₂ →
      iselect ps s₁ = iselect ps s₂ ∧
        ∃ a f f', isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
intro h₀ hh

Goal state after:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
s₁ s₂ : F.M
ps : Path F
h₀ : R s₁ s₂
hh : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f', isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case f.f.cons.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
induction h' : f' i using PFunctor.M.casesOn' with | _ a₁ f₁

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size + rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rll.size + rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
this : rll.size = 0 ∧ rlr.size = 0
⊢ rll.size = 0 ∧ rlr.size = 0
Module: Mathlib.Data.PNat.Factors

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

pp: case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset

Tactic:
· intro h
    rw [← prod_factorMultiset m, ← prod_factorMultiset m]
    apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
    rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
      prod_factorMultiset]

Goal state after:
case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset
Module: Mathlib.Data.PNat.Interval

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

Tactic:
by
  rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : lrl.size + lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
add_eq_zero

Goal state after:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : lrl.size = 0 ∧ lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0