mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inl
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ p f

pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f

Tactic:
·

Goal state after:
case intro.a.inl
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ p f
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f

Tactic:
·

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f
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:
·

Goal state after:
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₂
Module: Mathlib.Data.List.Sigma

Goal state before:
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:
·

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.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y

pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.graph.toList.Nodup

Tactic:
·

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.graph.toList.Nodup

Tactic:
·

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.graph.toList.Nodup
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ f.toAList.keys.toFinset = f.support

Tactic:
by
  ext
  simp [toAList, AList.keys, List.keys]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ l.lookupFinsupp a = (lookup a l).getD 0

Tactic:
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
  congr

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a

pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
·

Goal state after:
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬f a = 0
⊢ f.toAList.lookupFinsupp a = f a
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)

pp: case neg
κ : 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⟩ = 0

Tactic:
·

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

Goal state before:
pp: case neg
κ : 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⟩ = 0

Tactic:
·

Goal state after:
case neg
κ : 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⟩ = 0
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
·

Goal state after:
case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
·

Goal state after:
case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩
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:
·

Goal state after:
α : 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
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_1
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ ∅, (f x).slice i hid = (∑ x ∈ ∅, f x).slice i hid

pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
·

Goal state after:
case refine_1
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ ∅, (f x).slice i hid = (∑ x ∈ ∅, f x).slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
·

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
·

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
·

Goal state after:
case h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
·

Goal state after:
case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: case inl
n : ℕ
⊢ fib (↑n + 1) * fib (↑n - 1) - fib ↑n ^ 2 = (-1) ^ (↑n).natAbs

pp: case inr
n : ℕ
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ fib (↑n + 1) * fib (↑n - 1) - fib ↑n ^ 2 = (-1) ^ (↑n).natAbs
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: case inr
n : ℕ
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs

Tactic:
·

Goal state after:
case inr
n : ℕ
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1

pp: case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Tactic:
·

Goal state after:
case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Tactic:
·

Goal state after:
case a
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)
Module: Mathlib.Data.Int.Bitwise

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

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

Tactic:
·

Goal state after:
case false
n : ℕ
⊢ 1 + 2 * -[n.div2+1] = -[0 + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
·

Goal state after:
case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

pp: case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)

Tactic:
·

Goal state after:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)
Module: Mathlib.Data.Int.Bitwise

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

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

Tactic:
·

Goal state after:
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0
Module: Mathlib.Data.Holor

Goal state before:
pp: case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)

Tactic:
·

Goal state after:
case a
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
·

Goal state after:
case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0
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

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

pp: case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n

Tactic:
·

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

Goal state before:
pp: case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

pp: case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
·

Goal state after:
case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
·

Goal state after:
case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
·

Goal state after:
case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

pp: case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
·

Goal state after:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|
Module: Mathlib.Data.Int.Bitwise

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

pp: case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n

Tactic:
·

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

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

Tactic:
·

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
·

Goal state after:
case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r
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)

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

Tactic:
·

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

Goal state before:
pp: case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q

pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Tactic:
·

Goal state after:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
·

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

Goal state before:
pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Tactic:
·

Goal state after:
case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r
Module: Mathlib.Data.Int.Bitwise

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

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

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:
·

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

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

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:
·

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x && !y)) m n = m ||| 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:
·

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !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 : ℕ
⊢ (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))

pp: 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))

pp: 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))

pp: 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))

Tactic:
·

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))