mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : ¬s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (Sigma.map f g) []) = Option.map (g a) (dlookup a [])

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }

Tactic:
rfl

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

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

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
⊢ dlookup a ([] ++ l₂) = (dlookup a []).or (dlookup a l₂)

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : ¬a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : [].length ≤ 1
⊢ [] = [].head?.toList

Tactic:
rfl

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

Goal state before:
pp: case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

Tactic:
rfl

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

Goal state before:
pp: case nil
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []

Tactic:
rfl

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

Goal state before:
pp: case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList

Tactic:
rfl

Goal state after:
case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a

Tactic:
rfl

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

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

Tactic:
(rw [lookupAll_eq_dlookup a h]; apply Option.toList_nodup)

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬⟨a, b⟩ ∈ l
⊢ ∀ (a_1 : Sigma β), a_1 ∈ l → (if a = a_1.fst then some ⟨a, b⟩ else none) = none

Tactic:
grind

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

Goal state before:
pp: 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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
this : IsIso π'
⊢ (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f =
    ((lightProfiniteToLightCondSet ⋙ free R).map (CategoryTheory.inv π' ≫ g') ≫ g) ≫ p

Tactic:
grind

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.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
h : ¬a ∈ [].keys
⊢ kerase a [] = []

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
tl : List (Sigma β)
fst✝ : α
snd✝ : β fst✝
ih :
  ⟨fst✝, snd✝⟩.fst ∈ tl.keys →
    ∃ b l₁ l₂,
      ¬⟨fst✝, snd✝⟩.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨⟨fst✝, snd✝⟩.fst, b⟩ :: l₂ ∧ kerase ⟨fst✝, snd✝⟩.fst tl = l₁ ++ l₂
h : ⟨fst✝, snd✝⟩.fst ∈ (⟨fst✝, snd✝⟩ :: tl).keys
⊢ ⟨fst✝, snd✝⟩ :: tl = [] ++ ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩ :: tl

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = map Sigma.fst (eraseP ((fun x ↦ a == x) ∘ Sigma.fst) l)

Tactic:
Function.comp_def

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x ↦ a == x.fst) l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)

Tactic:
rfl

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

Goal state before:
pp: case neg.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])

Tactic:
rfl

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

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

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
⊢ dlookup a (kerase a' []) = dlookup a []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
hd : Sigma β
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
⊢ dlookup a (kerase a' (hd :: tl)) = dlookup a (hd :: tl)

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ dlookup a [].dedupKeys = dlookup a []

Tactic:
rfl

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
⊢ dm₁ = dm₂

Tactic:
exact dvd_antisymm
    (hmn.coprime_dvd_left h₁.1.1 |>.coprime_dvd_right h₂.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₁.dvd_mul_right dn₁))
    (hmn.coprime_dvd_left h₂.1.1 |>.coprime_dvd_right h₁.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₂.dvd_mul_right dn₂))

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ image ((fun p ↦ p.1 * p.2) ∘ Subtype.val) (m.divisors ×ˢ n.divisors).attach =
    image (⇑{ toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ }) (m.divisors ×ˢ n.divisors).attach

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ l : List (Sigma β)
⊢ [].kunion l ~ [].kunion l

Tactic:
rfl

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k k' : κ
f : ι k →₀ M
hk : k' ≠ k
i : ι k'
⊢ ⟨k', i⟩ ∉ Set.range ⇑(Embedding.sigmaMk k)

Tactic:
grind

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
i : ι k
m : M
⊢ (single i m).embSigma = single ⟨k, i⟩ m

Tactic:
grind

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

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

Tactic:
simp [split_apply, embSigma_apply_of_ne _ hk]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ : List ℕ
a : Holor α ds₁
⊢ cast ⋯ a = fun t ↦ a (cast ⋯ t)

Tactic:
rfl

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = !n✝.bodd

Tactic:
rfl

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

Goal state before:
pp: case false
n : ℕ
⊢ (bif false then 1 else 0) = ↑(bif false then 1 else 0)

Tactic:
rfl

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

Goal state before:
pp: case true
n : ℕ
⊢ (bif true then 1 else 0) = ↑(bif true then 1 else 0)

Tactic:
rfl

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

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    fib (↑(i + 1) + 1) * fib (↑(i + 1) - 1) - fib ↑(i + 1) ^ 2

Tactic:
grind

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

Goal state before:
pp: case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]

Tactic:
rfl

Goal state after:
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: case false
n : ℕ
⊢ (2 * ↑n + bif false then 1 else 0) = ↑(2 * n + false.toNat)

Tactic:
rfl

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

Goal state before:
pp: case true
n : ℕ
⊢ (2 * ↑n + bif true then 1 else 0) = ↑(2 * n + true.toNat)

Tactic:
rfl

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

Goal state before:
pp: case false
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]

Tactic:
rfl

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

Goal state before:
pp: case true
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]

Tactic:
rfl

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

Goal state before:
pp: n : ℤ
⊢ bodd 2 = false

Tactic:
rfl

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

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

Tactic:
rfl

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

Tactic:
rfl

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
rfl

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (s.card * n) (∑ x ∈ s, f x)

Tactic:
grind

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

Goal state before:
pp: case ofNat.negSucc.e_f.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc.e_f.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc.e_f.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc.e_f.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
rfl

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

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

Tactic:
rfl

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]

Tactic:
rfl

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.ofNat.e_f.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.ofNat.e_f.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.ofNat.e_f.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

Tactic:
rfl

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

Tactic:
rfl

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]

Tactic:
rfl

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.negSucc.e_f.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.negSucc.e_f.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.negSucc.e_f.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

Tactic:
rfl

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

Tactic:
rfl

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]

Tactic:
rfl

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v

Tactic:
sub_lt_sub_iff_right,

Goal state after:
a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x < b) ∧ r ∣ x - v
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
rcases m with m | m <;> rcases n with n | n <;>
  simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
  · by_cases h : f false false <;> simp +decide [h]
  · by_cases h : f false true <;> simp +decide [h]
  · by_cases h : f true false <;> simp +decide [h]
  · by_cases h : f true true <;> simp +decide [h]

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

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v

Tactic:
sub_lt_sub_iff_right,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a < x ∧ x - v ≤ b - v) ∧ r ∣ x - v
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case zero
m : ℕ
⊢ ↑m >>> ↑0 = ↑(m >>> 0)

Tactic:
rfl

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

Goal state before:
pp: case succ
m n✝ : ℕ
⊢ ↑m >>> ↑(n✝ + 1) = ↑(m >>> (n✝ + 1))

Tactic:
rfl

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

Goal state before:
pp: case zero
m : ℕ
⊢ -[m+1] >>> ↑0 = -[m >>> 0+1]

Tactic:
rfl

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

Goal state before:
pp: case succ
m n✝ : ℕ
⊢ -[m+1] >>> ↑(n✝ + 1) = -[m >>> (n✝ + 1)+1]

Tactic:
rfl

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

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
subst c

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

Goal state before:
pp: case negSucc
n a✝ : ℕ
⊢ -↑((a✝ + 1) * 2 ^ n) = -↑(a✝ + 1) * 2 ^ n

Tactic:
grind

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

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
c : ↑y = x
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
subst c

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

Goal state before:
pp: case nil
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left' f [] [] = (map (fun a ↦ f a none) [], [])

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left' f (head✝ :: tail✝) [] = (map (fun a ↦ f a none) (head✝ :: tail✝), [])

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : β
tail✝ : List β
⊢ zipWith f [] (head✝ :: tail✝) = []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head✝ : α
tail✝ : List α
⊢ zipWith f (head✝ :: tail✝) [] = []

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ [].zipLeft' [] = (map (fun a ↦ (a, none)) [], [])

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft' [] = (map (fun a ↦ (a, none)) (head✝ :: tail✝), [])

Tactic:
rfl

Goal state after: