mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
⊢ (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π =
    lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
        (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
      y' ▷ ℕ∪{∞}

Tactic:
apply CartesianMonoidalCategory.hom_ext

Goal state after:
case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      fst S ℕ∪{∞}

case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      snd S ℕ∪{∞}
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1}, Functor.mapConst = Functor.map ∘ Function.const β

Tactic:
intros; ext; simp [Functor.mapConst]

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α β γ : Type u_3
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ a ∈ s >>= fun x ↦ f x >>= g

Tactic:
simp only [bind_def, mem_bind]
    exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,
      fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c

Tactic:
rw [mem_pure] at ab ac
    rwa [← ac] at ab

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

Goal state before:
pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
left
          rw [h'.2]

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

Goal state before:
pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
left
          rw [h'.2]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a l) <+ ⟨a', b'⟩ :: l

Tactic:
exact (lookupAll_sublist a l).cons _

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
by
  by_cases h' : a ∈ s₁
  · rw [lookup_union_left h']
  · rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ l.dedupKeys.NodupKeys

Tactic:
dsimp [dedupKeys]
  generalize hl : nil = l'
  have : NodupKeys l' := by
    rw [← hl]
    apply nodup_nil
  clear hl
  induction l with
  | nil => apply this
  | cons x xs l_ih =>
    cases x
    simp only [foldr_cons, kinsert_def, nodupKeys_cons]
    constructor
    · simp only [keys_kerase]
      apply l_ih.not_mem_erase
    · exact l_ih.kerase _

Goal state after:
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 (kinsert ⟨a', b⟩.fst ⟨a', b⟩.snd tail✝.dedupKeys) = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
dlookup_kinsert_ne h,

Goal state after:
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 tail✝.dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)
Module: Mathlib.Data.List.Sigma

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

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

Tactic:
· subst h₁
      simp

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ ¬a ∈ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ (fib (a - 1) * fib x + fib a * (fib (x - 1) + fib x)) ^ 2 -
      fib x *
        (fib (x - 1) * (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)) +
          fib x * (fib (a - 1) * fib (a - 1) + fib a * fib a + (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)))) =
    (fib x * (fib (a - 1) + fib a) + fib (x - 1) * fib a) ^ 2 -
      fib x *
        (fib x * ((fib (a - 1) + fib a) ^ 2 + fib a ^ 2) +
          fib (x - 1) * (fib a * (fib (a - 1) + fib a) + fib (a - 1) * fib a))

Tactic:
ring

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m

Tactic:
Nat.bitwise_swap,

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Function.swap (Nat.bitwise fun y x ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && y) m n) = -[m+1].land (ofNat n)

Tactic:
Nat.bitwise_swap,

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ ↑(Function.swap (Nat.bitwise fun y x ↦ !x && y) m n) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
Nat.bitwise_swap,

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Function.swap (Nat.bitwise fun y x ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Goal state after:
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true 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 false true then -[Nat.bitwise (fun x y ↦ !f x !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f x !y) m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Goal state after:
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))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Goal state after:
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true 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 true then -[Nat.bitwise (fun x y ↦ !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y ↦ f (!x) !y) m n))
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : dropWhile p tl = hd :: tl
⊢ False

Tactic:
replace h := congrArg length h

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
h : (dropWhile p tl).length = (hd :: tl).length
⊢ False
Module: Mathlib.Data.List.Fold

Goal state before:
pp: α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a l = foldr f a l

Tactic:
by
  induction l <;> simp [*, foldl_assoc]

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ [].rdrop n = []

Tactic:
by simp [rdrop]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.rdrop 0 = l

Tactic:
by simp [rdrop]

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

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Tactic:
| append_singleton xs x IH =>

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

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse

Tactic:
| append_singleton xs x IH =>

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

Goal state before:
pp: α : Type u_1
p : α → Bool
x : α
⊢ (if p x = true then rdropWhile p [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]

Tactic:
rdropWhile_nil

Goal state after:
α : Type u_1
p : α → Bool
x : α
⊢ (if p x = true then [] else [] ++ [x]) = if p x = true then [] else [] ++ [x]
Module: Mathlib.Data.List.DropRight

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

Tactic:
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.Intervals

Goal state before:
pp: n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
by
  rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
  rfl

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

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipLeft bs = (as.zipLeft' bs).fst

Tactic:
rw [zipLeft, zipLeft']

Goal state after:
α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg.inl
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
eq : i % p = i
⊢ w[i % p]? = w[i]?

Tactic:
rw [eq]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ IsNat ⌈r⌉₊ 0

Tactic:
by
  constructor
  simp [h.neg_to_eq, div_nonneg]

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ x ∈ range (n % p + 1),
      ∑ x_1 ∈ range (n / p + 1), if k = x + p * x_1 then 1 * ↑((n % p).choose x * (n / p).choose x_1) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
rw [← sum_product', sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl), sum_ite_eq]

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then
      1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2)
    else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) < n.minFac ^ k

Tactic:
exact Nat.pow_lt_pow_of_lt (Prime.one_lt isPrime) (sub_one_lt_of_lt k_pos)

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

Goal state before:
pp: n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
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.Nat.Nth

Goal state before:
pp: case succ.refine_1
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}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ {x | p x ∧ ∀ k < n + 1, nth p k < x}.Nonempty

pp: case succ.refine_2
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}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ ∀ b ∈ {x | p x ∧ ∀ k < n + 1, nth p k < x}, f (n + 1) ≤ b

Tactic:
· use nth p (n + 1), nth_mem _ hn
      exact fun k hk => nth_lt_nth' hk hn

Goal state after:
case succ.refine_2
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}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ ∀ b ∈ {x | p x ∧ ∀ k < n + 1, nth p k < x}, f (n + 1) ≤ b
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (Set.ofPred p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
⊢ i ∈ f '' {i | p' (f i)} ↔ i ∈ Set.ofPred p'

Tactic:
refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩

Goal state after:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (Set.ofPred p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
he : i ∈ Set.ofPred p'
⊢ i ∈ f '' {i | p' (f i)}
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 (Set.ofPred p)

Tactic:
rw [← hs h0, ← 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)
⊢ {i | p (f i)}.Nonempty
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
· cases id rr
        · exact node 2 nil x r
        · exact node 3 (ι x) rx rr

Goal state after:
case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
constructor
  · rintro ⟨y, hy⟩
    rcases h : y with ⟨a, f⟩
    refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩
    rw [← hy, h, map_eq_map, PFunctor.map_eq]
    congr
  rintro ⟨a, f, xeq, pf⟩
  use ⟨a, fun i => ⟨f i, pf i⟩⟩
  rw [xeq]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0

Tactic:
have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0
Module: Mathlib.Data.PFunctor.Multivariate.Basic

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

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

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual

Tactic:
cases m <;> simp [node4L, node4R, node3L, dual_node3R, add_comm]

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

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ b % pos a ≤ pos a

Tactic:
rw [← le_to_nat, mod_to_nat]
      exact le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ (x.children a).approx n = ch a

Tactic:
dsimp only [children]

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ children' (x.approx n.succ) (cast ⋯ a) = ch a
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

pp: case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

pp: case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y

Tactic:
· rw [← agree_iff_agree']
      apply x.consistent

Goal state after:
case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
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:
simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a

Tactic:
by
  rw [← card_Ico, Fintype.card_ofFinset]

Goal state after: