mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } xs).down = (toList xs).length

Tactic:
rw [foldl_toList]

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } (toList xs)).down = (toList xs).length
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : TypeVec.{?u.4} 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec.{?u.4} 0
⊢ β Fin2.elim0 = β v

Tactic:
congr; funext i; cases i

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x

Tactic:
induction i

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ (toSubtype p ⊚ ofSubtype p) Fin2.fz x = id Fin2.fz x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), (toSubtype p ⊚ ofSubtype p) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ (toSubtype p ⊚ ofSubtype p) a✝.fs x = id a✝.fs x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i ↦ { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x

Tactic:
induction i

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p Fin2.fz x) }
⊢ (subtypeVal p ⊚ toSubtype p) Fin2.fz x = ↑x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : (fun i ↦ { x // ofRepeat (p i x) }) a✝),
    (subtypeVal p ⊚ toSubtype p) a✝ x = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ (subtypeVal p ⊚ toSubtype p) a✝.fs x = ↑x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x

Tactic:
induction i

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ (toSubtype' r ⊚ ofSubtype' r) Fin2.fz x = id Fin2.fz x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝),
    (toSubtype' r ⊚ ofSubtype' r) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ (toSubtype' r ⊚ ofSubtype' r) a✝.fs x = id a✝.fs x
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ ⇑(eqv α) <$> pure ((eqv α).symm x) = pure x

Tactic:
map_pure,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ pure ((eqv α) ((eqv α).symm x)) = pure x
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ Equiv.traverse eqv pure x = pure x

Tactic:
by
  rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)

Tactic:
simp only [Equiv.traverse, traverse_eq_map_id]

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ ⇑(eqv β) <$> pure (f <$> (eqv α).symm x) = pure (Equiv.map eqv f x)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
⊢ ∃ a, y π a = s

Tactic:
have hp (s : S) (n : OnePoint X) : π (p s n) = (s, n) := (hπ (s, n)).choose_spec

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × OnePoint X
hπ : Function.Surjective π
s : S
p : S → OnePoint X → T := fun s n ↦ ⋯.choose
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ ∃ a, y π a = s
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i ↦ { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).1 (↑x).2

Tactic:
induction i

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r Fin2.fz (prod.mk Fin2.fz x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) Fin2.fz x = prod.mk Fin2.fz (↑x).1 (↑x).2

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop)
    (x : (fun i ↦ { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) a✝),
    (subtypeVal r ⊚ toSubtype' r) a✝ x = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) a✝.fs x = prod.mk a✝.fs (↑x).1 (↑x).2
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count (!b) l + count b l = l.length

Tactic:
have := length_eq_countP_add_countP (l := l) (· == !b)

Goal state after:
l : List Bool
b : Bool
this : l.length = countP (fun x ↦ x == !b) l + countP (fun a ↦ decide ¬(a == !b) = true) l
⊢ count (!b) l + count b l = l.length
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ (a ∈ if t = ∅ then ∅ else s) ↔ a ∈ (image (const β✝) s).sup fun f ↦ image f t

Tactic:
if_neg ht.ne_empty,

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
· subst h'
        simp

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ b ^^^ a = b

Tactic:
by
  rw [xor_comm a, xor_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ (b ^^^ a) = b

Tactic:
by
  rw [xor_comm a, xor_cancel_right]

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

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ (↑↑1 - 1) * ↑r < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ ↑↑1 * ↑r

Tactic:
cast_one,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ (↑1 - 1) * ↑r < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ ↑1 * ↑r
Module: Mathlib.Data.List.Sections

Goal state before:
pp: case refine_2.nil
α : Type u_1
L : List (List α)
f : List α
⊢ [] ∈ [].sections

Tactic:
simp only [sections, mem_singleton]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
by
  rcases shortlex_def.mp h with h1 | h2
  · apply of_length_lt
    rw [List.length_append]
    lia
  cases t with
  | nil =>
    rw [List.append_nil]
    exact h
  | cons head tail =>
    apply of_length_lt
    rw [List.length_append, List.length_cons]
    lia

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

Goal state before:
pp: case mp
α : 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
⊢ w[j]? = w[j + p]?

Tactic:
have : j + p - (List.take p w).length = j := by
      simp_all [min_eq_left_of_lt]

Goal state after:
case mp
α : 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
this : j + p - (take p w).length = j
⊢ w[j]? = w[j + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w

Tactic:
simp_all [(take_eq_self_iff w).mpr large]

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

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w.HasPeriod p

Tactic:
by
  rw [HasPeriod]; simp_all [(take_eq_self_iff w).mpr large]

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
x1 : Matrix m₁ n R
⊢ ∀ ⦃a₂ : Matrix m₁ n R⦄ ⦃b₁ b₂ : Matrix m₂ n R⦄, x1.fromRows b₁ = a₂.fromRows b₂ → x1 = a₂ ∧ b₁ = b₂

Tactic:
x2

Goal state after:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
x1 x2 : Matrix m₁ n R
⊢ ∀ ⦃b₁ b₂ : Matrix m₂ n R⦄, x1.fromRows b₁ = x2.fromRows b₂ → x1 = x2 ∧ b₁ = b₂
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
x1 : Matrix m n₁ R
⊢ ∀ ⦃a₂ : Matrix m n₁ R⦄ ⦃b₁ b₂ : Matrix m n₂ R⦄, x1.fromCols b₁ = a₂.fromCols b₂ → x1 = a₂ ∧ b₁ = b₂

Tactic:
x2

Goal state after:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
⊢ ∀ ⦃b₁ b₂ : Matrix m n₂ R⦄, x1.fromCols b₁ = x2.fromCols b₂ → x1 = x2 ∧ b₁ = b₂
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr
α : 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 α
hN : ∀ (x : α), x ∈ N → x < a
⊢ Acc OneStep (M + N)

Tactic:
induction N using Multiset.induction with
  | empty =>
    simpa using .intro _ hM
  | @cons b N ihN =>
    simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
    obtain ⟨hba, hN⟩ := hN
    exact ha _ hba <| ihN hN

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: q : ℚ≥0
⊢ ↑⌊q⌋₊ = ↑(q.num / q.den)

Tactic:
NNRat.coe_floor,

Goal state after:
q : ℚ≥0
⊢ ⌊↑q⌋ = ↑(q.num / q.den)
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by
  zify
  convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂ <;> norm_cast

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

Goal state before:
pp: m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ ¬m.minFac ≤ n

Tactic:
iff_not_comm,

Goal state after:
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n ↔ ¬m.Coprime n !
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons.mp
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i : Fin (l.length + 1)
⊢ a ≡ b [MOD (m :: l).get i]

Tactic:
cases i using Fin.cases <;> simp_all

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
⊢ {x | x ∈ l}.Pairwise (Coprime on s)

Tactic:
simpa [List.Perm.mem_iff pp] using co'

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

Goal state before:
pp: case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization ≤ n • b.factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization

Tactic:
factorization_ceilRoot,

Goal state after:
case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization ≤ n • b.factorization ↔ a.factorization ⌈/⌉ n ≤ b.factorization
Module: Mathlib.Data.Nat.Choose.Lucas

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

Tactic:
mul_right_comm

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) *
      ↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) [ZMOD
    ↑p]
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
⊢ ↑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]

Tactic:
cast_one,

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
hf : (Set.ofPred p).Infinite
n : ℕ
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) =
    ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)

Tactic:
dif_neg hf

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Infinite
n : ℕ
⊢ ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n) = ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
hf : (Set.ofPred p).Finite
⊢ n < #hf.toFinset

Tactic:
simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h
  exact h.2 hf

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

Goal state before:
pp: case zero
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ nth p 0

Tactic:
rw [Nat.nth_zero]
    refine le_csInf ⟨_, nth_mem _ hn⟩ fun b hb => ?_
    rcases hsurj hb with ⟨k, hk, rfl⟩
    exact hmono hn hk (Nat.zero_le _)

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

Goal state before:
pp: case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
· refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
      rcases id ll with _ | lls
      · exact nil
      --should not happen
      rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
      · exact nil
      --should not happen
      exact
        if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
        else
          node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
            (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩
  · rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact ι x
    · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · cases id rr
        · exact node 2 nil x r
        · exact node 3 (ι x) rx rr
      · rcases id rr with _ | rrs
        · exact node 3 (ι x) rlx ι rx
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)
  · rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)
    · refine
        if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact nil
        --should not happen
        rcases id rr with _ | rrs
        · exact nil
        --should not happen
        exact
          if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
          else
            node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
              (node (size rlr + rrs + 1) rlr rx rr)
      · rcases id ll with _ | lls
        · exact nil
        --should not happen
        rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact nil
        --should not happen
        exact
          if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (lrs + rs + 1) lr x r)
          else
            node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
              (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: p : PosNum
⊢ (pos p.pred'.succ').toZNum = ZNum.pos p

Tactic:
PosNum.succ'_pred',

Goal state after:
p : PosNum
⊢ (pos p).toZNum = ZNum.pos p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero.mp
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

Tactic:
cases h <;> rfl

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

Goal state before:
pp: case zero.mpr
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

Tactic:
cases h <;> rfl

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

Goal state before:
pp: case pos.mp
p a✝ : PosNum
h : pos p = pos a✝
⊢ ZNum.pos p = (pos a✝).toZNum

Tactic:
cases h <;> rfl

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

Goal state before:
pp: case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝

Tactic:
cases h <;> rfl

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

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

Tactic:
PosNum.cast_mul,

Goal state after:
a b : PosNum
⊢ -(↑a * ↑b) = ↑a * -↑b
Module: Mathlib.Data.Num.ZNum

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

Tactic:
PosNum.cast_mul,

Goal state after:
a b : PosNum
⊢ -(↑a * ↑b) = -↑a * ↑b
Module: Mathlib.Data.Num.ZNum

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

Tactic:
PosNum.cast_mul,

Goal state after:
a b : PosNum
⊢ ↑a * ↑b = -↑a * -↑b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(pos a) = pos a

Tactic:
rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
← cast_to_int m,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m < ↑n ↔ m < n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
← cast_to_int m,

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑↑m = ↑n ↔ m = n
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left

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
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
by
  rw [Valid'.dual_iff, dual_balanceR]
  have := hr.dual.balanceL_aux hl.dual
  rw [size_dual, size_dual] at this
  exact this H₁ H₂ H₃

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m

Tactic:
by
  simp only [← not_lt, find_lt_iff, not_exists, not_and]

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

Goal state before:
pp: m : ℕ+
v : PrimeMultiset
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
let h := @factorMultiset_le_iff m v.prod
  rw [v.factorMultiset_prod] at h
  exact h

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

Goal state before:
pp: case nil.node.node.node.hnc
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ ¬rls + rrs + 1 ≤ 1

Tactic:
· exact not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))

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

Goal state before:
pp: case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ (node ls ll lx lr).balanceL x (node rs rl rx rr) = (node ls ll lx lr).balance x (node rs rl rx rr)

Tactic:
· replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)
      simp [balanceL, balance, H2]; split_ifs <;> simp [add_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ ↑y
xr : r.Bounded (↑y) o₂
xf : x ≤ f y
fx : f y ≤ x
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size

Tactic:
refine
        ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩

Goal state after: