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

Goal state before:
pp: case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (Sum.inr x✝) = pure (bimap f✝ f'✝ (Sum.inr x✝))

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Goal state after:
case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α'✝
⊢ pure (Sum.inr (f'✝ x✝)) = pure (bimap f✝ f'✝ (Sum.inr x✝))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (Sum.inl x✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (Sum.inl x✝)

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ (Sum.inr x✝)) =
    bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) (Sum.inr x✝)

Tactic:
simp [bitraverse, Sum.bitraverse, functor_norm]

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ none = Fix.approx f 0 x

pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z

Tactic:
· rfl

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝

Tactic:
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ Function.Surjective (coverToFun (fibreIncl π σ) (π_r π σ))

Tactic:
intro ⟨⟨⟨t, ht⟩, ⟨t', ht'⟩⟩, _⟩

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a

Tactic:
· rfl

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (↑(z % ↑2 ^ (w + 1)).toNat).bmod (2 ^ (w + 1)) = (↑z).toInt

Tactic:
Nat.cast_ofNat,

Goal state after:
z : ℤ
w : ℕ
⊢ (↑(z % 2 ^ (w + 1)).toNat).bmod (2 ^ (w + 1)) = (↑z).toInt
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
h2 : Even [].length
⊢ count (!b) [] = count b []

pp: case cons
b x : Bool
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (x :: l)
h2 : Even (x :: l).length
⊢ count (!b) (x :: l) = count b (x :: l)

Tactic:
· rfl

Goal state after:
case cons
b x : Bool
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (x :: l)
h2 : Even (x :: l).length
⊢ count (!b) (x :: l) = count b (x :: l)
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
card_Ioo_eq_card_Icc_sub_two,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Icc f g) - 2 = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e m'.succ
h : m = m'.succ
ss : m'.size = m.size
⊢ ValidFinite e m'

Tactic:
subst h

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : ValidFinite e m'.succ
ss : m'.size = m'.succ.size
⊢ ValidFinite e m'
Module: Mathlib.Condensed.Light.Sequence

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

Tactic:
Y

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

Goal state before:
pp: case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
let hπ'' : RegularEpi <| lightProfiniteToLightCondSet.map π' :=
      regularEpiOfEpi _

Goal state after:
case pos
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.AList

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
subst h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
subst h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
subst h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll a (⟨a, b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l
Module: Mathlib.Data.List.Sigma

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

Tactic:
subst h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk a) (lookupAll a (⟨a, b'⟩ :: l)) <+ ⟨a, b'⟩ :: l
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂

Tactic:
rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this

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

Goal state before:
pp: case neg
α : 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
h✝¹ : ¬a = a'
h✝ : ¬decide (a = a') = true
⊢ none = none

Tactic:
· rfl

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

Goal state before:
pp: case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ⊥

Tactic:
bot_eq_empty

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ∅
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → ¬a ∈ (kerase a tl).keys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : a = hd.fst
⊢ ¬a ∈ (kerase a (hd :: tl)).keys

Tactic:
subst h

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
ih : tl.NodupKeys → ¬hd.fst ∈ (kerase hd.fst tl).keys
⊢ ¬hd.fst ∈ (kerase hd.fst (hd :: tl)).keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case trans
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
l₁✝ l₂✝ l₃✝ : List (Sigma β)
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁₂ : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
ih₂₃ : ∀ (l : List (Sigma β)), l₂✝.kunion l ~ l₃✝.kunion l
l : List (Sigma β)
⊢ l₁✝.kunion l ~ l₃✝.kunion l

Tactic:
| trans _ _ ih₁₂ ih₂₃ =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
⊢ pimage f s = image (fun x ↦ (f ↑x).get ⋯) {x ∈ s | (f x).Dom}.attach

Tactic:
by
  aesop (add simp Part.mem_eq)

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

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ⟨k, i⟩.fst = k✝
⊢ f.embSigma ⟨k, i⟩ = f (h ▸ ⟨k, i⟩.snd)

Tactic:
subst h

Goal state after:
case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k : κ
i : ι k
f : ι ⟨k, i⟩.fst →₀ M
⊢ f.embSigma ⟨k, i⟩ = f (⋯ ▸ ⟨k, i⟩.snd)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun t ↦ x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

pp: case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Tactic:
· rfl

Goal state after:
case eq
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0

Tactic:
· rfl

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

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

Tactic:
by rw [← shiftLeft_neg, neg_neg]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
rw [rtake]

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse
Module: Mathlib.Data.List.DropRight

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

Tactic:
rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ rtakeWhile p l
⊢ p x = true

Tactic:
rw [rtakeWhile, mem_reverse] at hx

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p l.reverse
⊢ p x = true
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []

Tactic:
by cases l <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []

Tactic:
by cases l <;> rfl

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

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])

Tactic:
simp only [nil_append, modifyLast.go]; simp

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

Goal state before:
pp: case cons.zero.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ 0 = 0

pp: case cons.zero.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1

pp: case cons.succ.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
· rfl

Goal state after:
case cons.zero.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1

case cons.succ.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
by
  rw [List.forall_mem_iff_forall_getElem]
  intro i hi
  have := length_splitLengths_getElem_le l sz (hi := hi)
  have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)
  lia

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ a :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false
⊢ splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m

Tactic:
by
  induction l generalizing a g with
  | nil =>
    rw [nil_append]
    cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]
  | cons b l IH => simp_all [splitBy.loop]

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n.descFactorial k)

Tactic:
by
  rw [Nat.descFactorial_eq_div hk]
  refine (hp.coprime_factorial_of_lt hn).coprime_div_right ?_
  simp [Nat.factorial_dvd_factorial]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑10 ≡ -1 [ZMOD ↑11]

Tactic:
unfold Int.ModEq

Goal state after:
n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case zero
A : Type u_1
inst✝ : Semiring A
m : ℕ
hn_fac : IsUnit ↑(m + 0)!
⊢ IsUnit ↑m !

Tactic:
simpa using hn_fac

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

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

pp: case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)

Tactic:
· rfl

Goal state after:
case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑2 = 2

pp: case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0

Tactic:
· rfl

Goal state after:
case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑(n + 1)).toZNum = ZNum.ofInt' ↑(n + 1)

Tactic:
by
    rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]

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

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

Tactic:
neg_mul_neg

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

Goal state before:
pp: case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
have := this.1 e
    simp only [Num.cast_bit1]
    constructor
    · rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
    · rwa [this, two_mul, add_lt_add_iff_right] at h₂

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

Goal state before:
pp: case zero
⊢ zero.div 0 = 0

pp: case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

Tactic:
· rfl

Goal state after:
case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ zero.mod 0 = zero

pp: case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝

Tactic:
· rfl

Goal state after:
case pos
a✝ : PosNum
⊢ (pos a✝).mod 0 = pos a✝
Module: Mathlib.Data.Num.ZNum

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

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

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

Tactic:
· rfl

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

case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (b % pos a * pos a).natSize ≤ n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑(n.div' d) = ↑(pos n) / ↑(pos d)

Tactic:
rw [← Num.to_nat_to_int]

Goal state after:
n d : PosNum
⊢ ↑↑(n.div' d) = ↑(pos n) / ↑(pos d)