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

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ op (flip (List.foldlM f) (FreeMonoid.toList (x✝ * y✝))) =
    op (flip (List.foldlM f) (FreeMonoid.toList x✝)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝))

Tactic:
apply unop_injective

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ unop (op (flip (List.foldlM f) (FreeMonoid.toList (x✝ * y✝)))) =
    unop (op (flip (List.foldlM f) (FreeMonoid.toList x✝)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝)))
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u

Tactic:
· refine ⟨g <$$> u, ?_⟩
    rw [h₁]
    simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) i ⟨x, property✝⟩) = ↑(TypeVec.id i ⟨x, property✝⟩)

Tactic:
cases i

Goal state after:
case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) Fin2.fz ⟨x, property✝⟩) = ↑(TypeVec.id Fin2.fz ⟨x, property✝⟩)

case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) a✝.fs ⟨x, property✝⟩) = ↑(TypeVec.id a✝.fs ⟨x, property✝⟩)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property✝ : ofRepeat (α.PredLast' P i x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α i ⟨x, property✝⟩)

Tactic:
cases i

Goal state after:
case h₁.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (α.PredLast' P Fin2.fz x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α Fin2.fz ⟨x, property✝⟩)

case h₁.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : ofRepeat (α.PredLast' P a✝.fs x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α a✝.fs ⟨x, property✝⟩)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) i ⟨x, property✝⟩ = TypeVec.id i ⟨x, property✝⟩

Tactic:
cases i

Goal state after:
case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) Fin2.fz ⟨x, property✝⟩ = TypeVec.id Fin2.fz ⟨x, property✝⟩

case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) a✝.fs ⟨x, property✝⟩ = TypeVec.id a✝.fs ⟨x, property✝⟩
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α i ⟨x, property✝⟩)).1

Tactic:
cases i

Goal state after:
case h₁.e_a.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).1

case h₁.e_a.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).1
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_b.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α i ⟨x, property✝⟩)).2

Tactic:
cases i

Goal state after:
case h₁.e_b.e_a.e_a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk Fin2.fz x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α Fin2.fz ⟨x, property✝⟩)).2

case h₁.e_b.e_a.e_a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : ofRepeat (α.RelLast' rr a✝.fs (prod.mk a✝.fs x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α a✝.fs ⟨x, property✝⟩)).2
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i

Tactic:
cases i

Goal state after:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ (α.drop ::: α.last) Fin2.fz = α Fin2.fz

case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
a✝ : Fin2 n
⊢ (α.drop ::: α.last) a✝.fs = α a✝.fs
Module: Mathlib.Data.TypeVec

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

Tactic:
cases i

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 ↦ x) i

Tactic:
cases i

Goal state after:
case fz
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) Fin2.fz = (TypeVec.const x α ::: fun x_1 ↦ x) Fin2.fz

case fs
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a✝ : Fin2 n
⊢ TypeVec.const x (α ::: β) a✝.fs = (TypeVec.const x α ::: fun x_1 ↦ x) a✝.fs
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i

Tactic:
cases i

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝

Tactic:
cases i

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
cases i

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

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
Module: Mathlib.Data.TypeVec

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

Tactic:
simp only [toSubtype', comp, subtypeVal, prod.mk] at *

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
simp only [toSubtype', comp, subtypeVal, prod.mk] at *

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.1 x.2)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
Module: Mathlib.Data.BitVec

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

Tactic:
Int.natCast_pow,

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
not_imp_comm

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (¬∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Tactic:
rw [eq_mk_of_mem aq]

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin

Tactic:
exact v

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

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin

Tactic:
exact v

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take m ⋯ fun i ↦ addCases u v i) = take m h u

Tactic:
ext i
  have : i < n := Nat.lt_of_lt_of_le i.isLt h
  simp only [take, addCases, this, val_castLE, ↓reduceDIte]
  congr

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt8.ofFin UInt8.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt8.ofFin UInt8.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt16.ofFin UInt16.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt16.ofFin UInt16.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt32.ofFin UInt32.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt32.ofFin UInt32.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt64.ofFin UInt64.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt64.ofFin UInt64.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int8.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int8.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int16.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int16.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int32.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int32.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse (Int64.ofBitVec ∘ BitVec.ofFin) (BitVec.toFin ∘ Int64.toBitVec)

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ LeftInverse BitVec.ofFin BitVec.toFin

Tactic:
by intro x; simp

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ RightInverse BitVec.ofFin BitVec.toFin

Tactic:
by intro x; simp

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

Goal state before:
pp: case h
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a✝⟧ = Comp.mk (traverse h <$> traverse g ⟦a✝⟧)

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, functor_norm]

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ Prod.mk <$> s <*> t = (fun b a ↦ (a, b)) <$> t <*> s

Tactic:
simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]
      change (s.biUnion fun a => t.image fun b => (a, b))
        = t.biUnion fun b => s.image fun a => (a, b)
      trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]

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:
by
  simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
  congr

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus g = (f - g).support

Tactic:
← neLocus_add_right _ _ (-g),

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + -g).neLocus (g + -g) = (f - g).support
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✝
⊢ (embDomain { toFun := Sigma.mk k✝, inj' := ⋯ } f) ⟨k, i⟩ = 0

Tactic:
rw [embDomain_of_notMem_range]

Goal state after:
case neg.h
κ : 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✝
⊢ ⟨k, i⟩ ∉ Set.range ⇑{ toFun := Sigma.mk k✝, inj' := ⋯ }
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (x + y)

Tactic:
by
    match hx with
    | CPRankMax.zero => simp only [zero_add, hy]

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]; apply Nat.le_add_right

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Tactic:
conv_lhs => rw [← div_add_mod b r, cast_add, cast_mul, ← add_sub, _root_.add_div,
    mul_div_cancel_left₀ _ hr'.ne', add_comm, Int.ceil_add_natCast, add_comm]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]

Tactic:
simp [rtake_eq_reverse_take_reverse]

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

Goal state before:
pp: n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a

Tactic:
intro _ h₂ h₃

Goal state after:
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x < n + 1)) (Ico n m) = [n]

Tactic:
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
  simp [filter_lt n m (n + 1), r]

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

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[i].length ≤ (head :: tail)[i]

Tactic:
cases i

Goal state after:
case zero
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
hi : 0 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[0].length ≤ (head :: tail)[0]

case succ
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
n✝ : ℕ
hi : n✝ + 1 < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[n✝ + 1].length ≤ (head :: tail)[n✝ + 1]
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xs.length < (xa :: xb).length

Tactic:
rw [h2len]; simp

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []

Tactic:
| cons b l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

Tactic:
| cons b l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []

Tactic:
| cons b l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r (b :: l) a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
| cons b l IH =>

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r (b :: l) a g gs)

Tactic:
| cons b l IH =>

Goal state after: