mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1.true
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)

Tactic:
(try rintro (_ | _))

Goal state after:
case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.false
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))

Tactic:
(try rintro (_ | _))

Goal state after:
case pbb.false.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

case pbb.false.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb.true
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))

Tactic:
(try rintro (_ | _))

Goal state after:
case pbb.true.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

case pbb.true.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ ∅ = ∅

Tactic:
inter_empty

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ ∅ = ∅
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X

Tactic:
· intro h
    let X' : Stonean := ⟨X.toTop, inferInstance⟩
    change Projective X'.compHaus
    apply Stonean.instProjectiveCompHausCompHaus

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
f : Code
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepRet (Cont.comp f k) v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.comp f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.comp f k)) }
        b₂

Tactic:
| comp f k _ =>

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ :
  trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x ↦ false) aux stack (trNormal a✝¹ a✝.cons₂)))) ⊆
      S ∧
    codeSupp a✝¹ a✝.cons₂ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.cons₁ a✝¹ a✝)))

Tactic:
exact fun _ => H₁.1 W

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₂
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝ : Cont'
H₁ : trStmts₁ (head stack (Λ'.ret a✝)) ⊆ S ∧ contSupp a✝ ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret a✝.cons₂))

Tactic:
exact fun _ => H₁.1 W

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMapLE h))

Tactic:
by
  apply Function.Surjective.of_comp (g := S.proj m)
  simpa only [proj_comp_transitionMapLE'] using S.proj_surjective n

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.refine_1
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' : trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧ codeSupp f (Cont'.cons₁ fs k) ⊆ S
h :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x ↦ false) main aux
            (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
⊢ codeSupp fs k.cons₂ ⊆ S

Tactic:
simp only [codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢
      exact ⟨h.2.2.1, h.2.2.2, H.2⟩

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

Goal state before:
pp: ι : 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 ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
by
  refine mem_map.trans ⟨?_, ?_⟩
  · rintro ⟨f, hf, rfl⟩
    rw [Function.Embedding.coeFn_mk]
    refine ⟨support_mk_subset, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact mk_of_mem hi
  · 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: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1

Tactic:
by
  cases l
  · exact zero_le
  grind [hl.count_not_cons]

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

Goal state before:
pp: case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j : ι
⊢ ∃ k, f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_

Goal state after:
case cons
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩

Goal state after:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))
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:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]
  rw [h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ lookup a (insert a b s) = some b

Tactic:
simp only [lookup, insert, dlookup_kinsert]

Goal state after:
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 β)
h : (c :: l).NodupKeys
⊢ C { entries := c :: l, nodupKeys := h }

Tactic:
mk_cons_eq_insert

Goal state after:
α : 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 β)
h : (c :: l).NodupKeys
⊢ C (insert c.fst c.snd { entries := l, nodupKeys := ⋯ })
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), ((s, f).2 i).isSome = true ↔ i ∈ (s, f).1
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩

Tactic:
by
    dsimp only at hf
    ext
    · simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]
    · simp +contextual [lookup_eq_some_iff, ← hf]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧

Tactic:
simp [AList.insert_union]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some ⟨a, b⟩ else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some ⟨a, b⟩ else none
⊢ x = y ∧ z = w

Tactic:
split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂

Goal state after:
case pos.refl.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ ⟨a, b⟩ = ⟨a, b⟩
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₁

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Tactic:
sq,

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b ^ 2
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Tactic:
sq,

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b ^ 2
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2

Tactic:
sq,

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b ^ 2
Module: Mathlib.Data.Int.NatPrime

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

Tactic:
sq,

Goal state after:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs * k.natAbs
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ ([].splitLengths l).length = [].length

Tactic:
simp [splitLengths, *]

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), (tail✝.splitLengths l).length = tail✝.length
l : List α
⊢ ((head✝ :: tail✝).splitLengths l).length = (head✝ :: tail✝).length

Tactic:
simp [splitLengths, *]

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
min : p < w.length
⊢ j + p - (take p w).length = j

Tactic:
simp_all [min_eq_left_of_lt]

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

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ drop p w <+: w

Tactic:
← prefix_append_right_inj (take p w)

Goal state after:
α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ take p w ++ drop p w <+: take p w ++ w
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
A : Matrix (m₁ ⊕ m₂) n R
⊢ A.toRows₁.fromRows A.toRows₂ = A

Tactic:
ext (i | i) j

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j
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
⊢ Function.Injective2 fromCols

Tactic:
intro x1 x2 y1 y2
  simp only [← Matrix.ext_iff]
  simp_all

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
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᵀ = A₁ᵀ.fromRows A₂ᵀ

Tactic:
ext (i | i) j

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j
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✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Tactic:
ext (i | i) j

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inl
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM' : N.OneStep M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)

Tactic:
exact ihM _ hNM'

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 < p ↔ n + 1 < p

Tactic:
← Nat.add_one_le_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) ∧ n + 1 ≤ p ↔ n + 1 < p
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ n.dist m = n - m

Tactic:
by
  unfold Nat.dist; lia

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

Goal state before:
pp: n k m : ℕ
⊢ (n + k).dist (m + k) = n.dist m

Tactic:
by
  unfold Nat.dist; lia

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

Goal state before:
pp: k n m : ℕ
⊢ (k + n).dist (k + m) = n.dist m

Tactic:
by
  unfold Nat.dist; lia

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

Goal state before:
pp: n m k l : ℕ
h : n + m = k + l
⊢ n.dist k = l.dist m

Tactic:
by
  unfold Nat.dist; lia

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

Goal state before:
pp: n m k : ℕ
⊢ n.dist k ≤ n.dist m + m.dist k

Tactic:
by
  unfold Nat.dist; lia

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(choose 0 0) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
choose,

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑1 * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
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
⊢ f (nth (fun i ↦ p (f i)) (n + 1)) = nth p (n + 1)

Tactic:
repeat nth_rw 1 [nth_eq_sInf]

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
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case neg
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : ¬a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
· simp [*]

Goal state after:
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 :
  ∀ (x y : P.M α),
    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)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : PFunctor.M.dest a₂ = ⟨a', g₂'⟩
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩⟩
h' :
  ∀ (i : (P.B a').last),
    R ((fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) ((fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩) i)
⊢ ∃ a f f',
    ⟨a', g₁'⟩ = ⟨a, f⟩ ∧
      PFunctor.M.dest ⟨a₂, f₂⟩.fst = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i

Tactic:
e₂'

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    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)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : PFunctor.M.dest a₂ = ⟨a', g₂'⟩
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩⟩
h' :
  ∀ (i : (P.B a').last),
    R ((fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) ((fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩) i)
⊢ ∃ a f f', ⟨a', g₁'⟩ = ⟨a, f⟩ ∧ ⟨a', g₂'⟩ = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map (fun a ↦ a) v = v

Tactic:
Multiset.map_id'

Goal state after:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ v = v
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
rw [reduce_a h]
        exact u.finish_isSpecial hs

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
n₁ n₂ : ℕ
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂

Tactic:
rcases Nat.le.dest hn with ⟨m, rfl⟩

Goal state after:
α : Type u_1
sel : Set α → Option α
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
n₁ : ℕ
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
hn : n₁ ≤ n₁ + m
⊢ n₁ = n₁ + m
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
apply (@pure_bind Computation _ _ _ _ _ _).trans _

Goal state after:
α : Type u
s : WSeq α
⊢ (Option.rec nil Prod.snd none).destruct = tail.aux none
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd (some (a, s))) >>= destruct = tail.aux (some (a, s))

Tactic:
apply (@pure_bind Computation _ _ _ _ _ _).trans _

Goal state after:
α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ (Option.rec nil Prod.snd (some (a, s))).destruct = tail.aux (some (a, s))
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨j, b⟩ ≤ ⟨i, a⟩

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨i, b⟩ ≤ ⟨i, a⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨j, b⟩ ≤ ⟨i, a⟩